Extension Types for Free

Technical Summary: Extension Types for Free: Cofibrations, Gluing, and Univalence in Two-Level Type Theory

Problem Statement
Extension types are a fundamental concept in dependent type theory, appearing in various contexts such as cubical type theories (paths with fixed endpoints), Riehl and Shulman's simplicial type theory (terms fixed on subshapes), and controlled-unfolding mechanisms. In existing frameworks, these types are typically postulated as new primitives, governed by a meta-theoretic "face calculus" or shape layer that dictates their formation and rules. This approach often requires specific model constructions or axiomatic additions to validate the rules (such as strict boundary conditions, relative function extensionality, and the homotopy extension property). A central open problem in homotopy type theory (HoTT) is determining the precise relationship between "book HoTT" (the axiomatic formulation in the HoTT book) and cubical type theories, particularly regarding whether they are conservative extensions of one another.

Methodology
The paper utilizes Two-Level Type Theory (2LTT) as a unifying framework. 2LTT enriches HoTT with a "strict" (outer) level of equality that satisfies Uniqueness of Identity Proofs (UIP) and function extensionality, while the "inner" (fibrant) level retains the standard homotopical structure.

• Semantics: The framework is semantically "free"; standard models of HoTT (e.g., simplicial sets, cubical sets) automatically yield models of 2LTT via presheaf constructions. The theory is conservative over its inner level, meaning no new theorems are provable in the inner language that were not already provable in HoTT.
• Definition of Extension Types: Instead of postulating extension types, the paper defines them internally within 2LTT. Given a cofibration $i: \Phi \hookrightarrow \Psi$ (a map in the outer level), a fibrant family $A$ over $\Psi$, and a partial section $a$, the extension type is defined as the strict fiber of the restriction map over $a$:
  $$\Pi_\Psi A \mid_i^a \coloneqq \Sigma_{f : \Pi_\Psi A} (f \circ i =_s a)$$
  Here, $=_s$ denotes the strict equality of the outer level.
• Cofibrations: The "face calculus" is replaced by the class of cofibrations in the outer level. The paper treats the specific choice of which maps are cofibrations as a parameter, allowing the framework to adapt to different settings (simplicial, cubical, etc.) without changing the core definition.

Key Contributions and Results

1. Extension Types "For Free":
   The paper demonstrates that in 2LTT, the entire calculus of extension types proposed by Riehl and Shulman is definable rather than axiomatic.

   • Strict Rules: The introduction, elimination, $\beta$, $\eta$, and boundary rules hold strictly by construction.
   • Provable Axioms: Axioms that are postulated in other settings, such as relative function extensionality and the homotopy extension property (realignment), become theorems derived from the properties of cofibrations and fibrations in 2LTT.
   • Unification: This single definition subsumes various existing instances, including cubical paths, Riehl-Shulman extension types, and proposition-indexed types (controlled unfolding).

2. Equivalence of Gluing and Univalence:
   The paper establishes a precise cycle of implications connecting cubical gluing and the univalence axiom within the 2LTT framework:

   • Univalence $\implies$ Gluing: If the inner universe is univalent, then for any cofibration, the type of "Glue data" (structures required to form a Glue type) is contractible. This implies the existence of a Glue structure satisfying the rules in homotopy form.
   • Gluing $\implies$ Univalence: Conversely, the existence of a "weak Glue structure" (requiring only inner equalities for boundary agreement and a path interval structure) implies that the universe is univalent.
   • Result: In the presence of a path interval, univalence and the existence of contractible Glue data are equivalent. This reverses the standard direction of implication (that Glue types imply Univalence) and establishes a two-way equivalence.

3. Formalization:
   All results from Section 2 through Section 5 are auto-formalized in Agda using the --two-level flag. The formalization combines internal HoTT arguments with external reasoning about the strict level, verifying the consistency and correctness of the theoretical claims.

4. Approach to Conservativity:
   The paper proposes a strategy to address the open problem of whether cubical type theories are conservative over book HoTT. By representing both theories within 2LTT:

   • Book HoTT is represented as MLTT + Univalence (inner level).
   • Cubical Type Theory is represented as MLTT + Glue + Path Interval (outer/structural assumptions).
   • The paper proves that over a base theory with a path interval, the Univalence axiom and the Glue axiom are inter-derivable. This suggests that the core difference between the theories may be structural rather than logical, offering a route to proving conservativity.

Significance and Claims
The paper claims that the framework of 2LTT provides a "free" and uniform foundation for extension types, removing the need for ad-hoc axioms or specific model constructions to validate their rules. By internalizing the face calculus as cofibrations, the theory unifies disparate occurrences of extension types found in the literature.

Regarding the connection between cubical type theories and book HoTT, the paper is modest. It does not claim to have solved the conservativity conjecture. Instead, it offers a proof of concept: it demonstrates that the core mechanism of cubical type theory (gluing) is logically equivalent to the core axiom of HoTT (univalence) when viewed through the lens of 2LTT. This equivalence allows researchers to translate structural extensions (like Glue types) into axiomatic extensions within a single framework, facilitating comparison and potentially paving the way for future conservativity proofs. The paper explicitly notes that the assumption of a "path interval" on the HoTT side remains an open challenge to discharge for a full equivalence.