Formalizing two-level type theory with cofibrant exo-nat

TL;DR

This paper formalizes two-level type theory in proof assistants like Agda, introducing new notions such as function extensionality for cofibrant types and providing novel results on inductive types using cofibrant exo-nat.

Contribution

It offers fully formalized proofs without notation abuse, introduces new concepts like function extensionality for cofibrant types, and explores models satisfying these axioms.

Findings

Formalization of two-level type theory in Agda.

Introduction of function extensionality for cofibrant types.

New results on inductive types using cofibrant exo-nat.

Abstract

This study provides some results about two-level type-theoretic notions in a way that the proofs are fully formalizable in a proof assistant implementing two-level type theory such as Agda. The difference from prior works is that these proofs do not assume any abuse of notation, providing us with more direct formalization. Moreover, some new notions, such as function extensionality for cofibrant types, are introduced. The necessity of such notions arises during the task of formalization. In addition, we provide some novel results about inductive types using cofibrant exo-nat, the natural number type at the non-fibrant level. While emphasizing the necessity of this axiom by citing new applications as justifications, we also touch upon the semantic aspect of the theory by presenting various models that satisfy this axiom.