Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Formalizing two-level type theory with cofibrant exo-nat

Elif Uskuplu

TL;DR

The paper advances formalization of two-level type theory (2LTT) with a cofibrant exo-natural number type $\mathbb{N}^e$ in Agda, emphasizing rigorous, notation-abide proofs. It introduces function extensionality tailored for cofibrant types, and develops results on cofibrant exo-types, sharp exo-types, and the lifting of cofibrancy from $\mathbb{N}^e$ to inductive types like $\mathsf{List}^e(A)$ and $\mathsf{BinTree}^e(N,L)$, including a novel equivalence $\mathsf{UnLBinTree}}^e \cong \mathsf{Balanced}(0^e)$. Semantically, the work constructs two-level CwFs and demonstrates models where cofibrant exo-nat holds, using presheaf models and exo-nat products to capture the required funext and UIP-like behaviors; it also discusses the interplay with fibrant replacements and potential infinities-toposes. The results provide a concrete path from formalization in proof assistants to robust semantic models for 2LTT, with implications for semisimplicial-type constructions and broader mathematical verification. The paper concludes with future directions toward W-types, extended Agda tooling, and richer model-theoretic explorations of cofibrancy across diverse categories.

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.

Formalizing two-level type theory with cofibrant exo-nat

TL;DR

The paper advances formalization of two-level type theory (2LTT) with a cofibrant exo-natural number type in Agda, emphasizing rigorous, notation-abide proofs. It introduces function extensionality tailored for cofibrant types, and develops results on cofibrant exo-types, sharp exo-types, and the lifting of cofibrancy from to inductive types like and , including a novel equivalence . Semantically, the work constructs two-level CwFs and demonstrates models where cofibrant exo-nat holds, using presheaf models and exo-nat products to capture the required funext and UIP-like behaviors; it also discusses the interplay with fibrant replacements and potential infinities-toposes. The results provide a concrete path from formalization in proof assistants to robust semantic models for 2LTT, with implications for semisimplicial-type constructions and broader mathematical verification. The paper concludes with future directions toward W-types, extended Agda tooling, and richer model-theoretic explorations of cofibrancy across diverse categories.

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.
Paper Structure (16 sections, 23 theorems, 83 equations, 7 figures)

This paper contains 16 sections, 23 theorems, 83 equations, 7 figures.

Table of Contents

  1. Introduction
  2. Review about two-level type theory
  3. Types & exo-types
  4. Isomorphisms & Equivalences
  5. Fibrant exo-types
  6. Cofibrant exo-types
  7. Sharp exo-types
  8. Lifting cofibrancy from exo-nat to other types
  9. List exo-types
  10. Exo-type of binary trees
  11. Semantics of two-level type theory
  12. Category with families
  13. Type formers in CwFs
  14. Two-level CwFs
  15. Models with cofibrant exo-nat
  16. ...and 1 more sections

Key Result

Theorem 2.6

If $A, C: \mathcal{U}$ are types and $B : A \rightarrow \mathcal{U}$ is a type family, we have the following maps. The first three maps are exo-isomorphisms.

Figures (7)

  • Figure 1: Agda code for two kinds of universes.
  • Figure 2: An example of the interaction between the flags --two-level and --cumulativity.
  • Figure 3: The diagram about sharpness of exo-coproduct.
  • Figure 4: The diagram about sharpness of $\sum$-exo-type.
  • Figure 5: Examples of the conversion between binary trees and parenthesization.
  • ...and 2 more figures

Theorems & Definitions (74)

  • Definition 2.1
  • Remark 2.2
  • Remark 2.3
  • Definition 2.4
  • Remark 2.5
  • Theorem 2.6
  • proof
  • Remark 2.7
  • Lemma 2.8
  • proof
  • ...and 64 more