Strict stability of extension types

Technical Summary: Strict Stability of Extension Types

Problem Statement
The paper addresses a foundational gap in the synthetic development of $(\infty, 1)$-categories within Homotopy Type Theory (HoTT), specifically the system introduced by Riehl and Shulman. While the semantics of this system were sketched using simplicial homotopy theory and the Segal space model, the original formulation left open the demonstration of strict stability for extension types under substitution. In type-theoretic models, "strict stability" requires that the interpretation of type formers (like extension types) commutes strictly with pullbacks (substitution), rather than merely up to isomorphism or homotopy. Without this property, the system cannot be fully interpreted in the internal language of an $\infty$-topos in a way that supports the strict equality required for certain internal category theories (e.g., those of Martini–Wolf).

Methodology
The author employs the splitting method originally described by Voevodsky and later generalized by Lumsdaine and Warren for local universes. The approach involves the following technical steps:

1. Universe Categories: The work is situated within a universe category (a category $\mathcal{C}$ equipped with a universe object $U$ and a universal fibration $\pi: \tilde{U} \to U$). The author assumes the existence of a "splitting," which is a global choice of pullback squares for the universal fibration. This ensures that reindexing (substitution) is modeled by strict equality of objects and morphisms, not just isomorphism.
2. Generic Contexts: Following the style of Awodey's work on natural models, the paper defines generic contexts (classifying objects) for extension type formation and introduction.
   • $U_{\text{Ext}@j}$ is defined as the object classifying pairs of a type family $A$ and a partial section $a$ over a shape inclusion $j: \phi \hookrightarrow \psi$.
   • $U_{\lambda@j}$ is defined as the object classifying triples $\langle A, a, b \rangle$ where $b$ is a total extension of $a$.
3. Strict Pullback Construction: The author constructs the extension type former $\text{Ext}@j$ and the introduction map $\lambda@j$ as morphisms between these generic contexts and the universe. By utilizing the splitting of the universal fibration, the paper demonstrates that the square formed by these maps is a strict pullback (not just a weak pullback).
4. Fibrancy Assumptions: To simplify the technical setting while retaining applicability to standard models (simplicial objects in an $\infty$-topos), the author assumes that the "shapes" (the simplicial contexts) are fibrant. This ensures that Leibniz cotensors are fibrations, allowing extension types to be modeled as ordinary 1-categorical pullbacks.

Key Contributions and Results
The primary contribution is Theorem 3.8, which establishes the strict stability of extension types. The theorem proves that for a type-theoretic model topos $\mathcal{E}$ and its associated simplicial model $s\mathcal{E}$, a fixed splitting of the standard type formers yields an interpretation of extension types that satisfies the following strict equalities for any context morphism $\sigma: \Delta \to \Gamma$:

1. Formation Stability: $\sigma^*(\text{Ext}@j(A, a)) = \text{Ext}@j(\sigma^*A, \sigma^*a)$
2. Introduction Stability: $\sigma^*(\lambda@j_{A,a}(b)) = \lambda@j_{\sigma^*A, \sigma^*a}(\sigma^*b)$
3. Elimination Stability: $\sigma^*(\text{app}@j_{A,a}(f, s)) = \text{app}@j_{\sigma^*A, \sigma^*a}(\sigma^*f, \sigma^*s)$

The paper further details how the $\beta$- and $\eta$-computation rules are satisfied within this strictly stable framework, relying on the universal property of the pullback squares defined by the splitting.

Significance and Claims
The paper claims that this result resolves the open problem regarding the strict stability of extension types in Riehl–Shulman's system. The practical upshot is that the system now possesses a robust semantics in the simplicial objects of an $\infty$-topos. This enables the use of the system to prove theorems about internal $\infty$-categories in the sense of Martini–Wolf, as the strict stability ensures that the type-theoretic operations align perfectly with the categorical pullbacks required for internal category theory.

The author notes that while the work assumes a single universe and fibrant shapes for technical simplicity, the reasoning is believed to generalize to hierarchies of universes and more complex fibered structures without essential obstruction. The work serves as a bridge between the synthetic syntax of simplicial HoTT and the rigorous semantics of $\infty$-topoi.