The internal languages of univalent categories

Technical Summary: The Internal Languages of Univalent Categories

Problem Statement
Internal language theorems in categorical logic establish an equivalence between syntax (type theories) and semantics (categorical models). A seminal result by Clairambault and Dybjer [CD14] corrected Seely's original theorem [See84], establishing a biequivalence between the bicategory of locally Cartesian closed categories (LCCCs) and the bicategory of democratic categories with families (CwFs) supporting extensional identity types, $\Sigma$-types, and $\Pi$-types.

However, this result was formulated within set-theoretic foundations. In univalent foundations (Homotopy Type Theory), the standard notion of CwF encounters a fundamental obstacle: the univalence axiom implies that the type of sets is not a set itself (it is a 1-type). Consequently, the requirement in CwFs that the collection of types in a context forms a set is violated by the univalent category of sets. Furthermore, the distinction between "chosen" structure (e.g., split fibrations) and "existing" structure (e.g., limits up to isomorphism) creates coherence issues in set-theoretic foundations that necessitate the axiom of choice or strictification procedures. In univalent foundations, where isomorphism implies identity, these distinctions evaporate, but the existing framework of CwFs is not directly applicable.

Methodology
The paper develops a new framework for categorical semantics within univalent foundations, utilizing univalent categories and comprehension categories instead of CwFs.

1. Univalent Categories: The author works with categories where the identity type of objects is equivalent to the type of isomorphisms (adjoint equivalences). This allows for the treatment of adjoint equivalences as identities, simplifying proofs regarding the preservation of structure (e.g., exponentials) and eliminating the need for the axiom of choice to select limits.
2. Comprehension Categories: To model dependent types without requiring types to form a set, the paper adopts comprehension categories (based on fibrations and displayed categories). A comprehension category consists of a base category of contexts, a displayed category of types, a cleaving (providing substitution), and a comprehension functor. The author restricts their attention to univalent full comprehension categories, where both the base and the displayed category are univalent.
3. Displayed Bicategories: The construction of the bicategories of models relies heavily on displayed bicategories [AFM+21]. This modular approach allows the author to build complex bicategories (like those of LCCCs or toposes with universes) by layering properties (e.g., finite limits, $\Pi$-types, universes) over simpler base bicategories. This modularity facilitates the proof that the resulting bicategories are themselves univalent.
4. Local Properties: To extend results from categories with finite limits to more complex structures like toposes, the paper adapts Maietti's notion of local properties [Mai05]. A local property is a condition on categories closed under slicing. The author formalizes this within the displayed bicategory framework to extend biequivalences from the base case (finite limits) to various classes of toposes.
5. Reindexing and Universes: For the treatment of universes, the paper employs reindexing of displayed bicategories. This technique allows the transfer of a biequivalence from a base category to a displayed category over it, enabling the definition of universes closed under specific type formers (e.g., $\Sigma$, $\Pi$, natural numbers) without requiring strict stability laws, but rather stability up to isomorphism (which becomes identity in univalent categories).

Key Contributions
The paper makes four primary contributions:

1. Univalent Analogue of Clairambault-Dybjer: The author constructs a biequivalence between the bicategory of univalent categories with finite limits and the bicategory of univalent full democratic finite limit (DFL) comprehension categories. This establishes that the internal language of univalent categories with finite limits is extensional Martin-Löf type theory with unit, binary product, and $\Sigma$-types.
2. Extension to Locally Cartesian Closed Categories: The biequivalence is extended to univalent locally Cartesian closed categories and DFL comprehension categories supporting $\Pi$-types. This confirms that the internal language of univalent LCCCs is extensional Martin-Löf type theory with $\Pi$-types.
3. Extension to Toposes and Universes: The method is generalized to various classes of toposes (pretoposes, $\Pi$-pretoposes, elementary toposes, and toposes with a natural numbers object) using local properties. Furthermore, the author defines universes in these categories that are closed under type formers (natural numbers, subobject classifier, propositional resizing, $\Sigma$-types, and $\Pi$-types), establishing a biequivalence for elementary toposes with a universe.
4. Formalization: All constructions and proofs are formalized in the Rocq proof assistant using the UniMath library, ensuring correctness and providing a machine-checked reference for the theory.

Results
The paper proves that for various classes of univalent categories, there exists a biequivalence with corresponding classes of univalent comprehension categories. Specifically:

• Finite Limits: Univalent categories with finite limits $\simeq$ DFL comprehension categories (Unit, Product, Equalizer, $\Sigma$).
• LCCC: Univalent LCCCs $\simeq$ DFL comprehension categories with $\Pi$-types.
• Toposes: Univalent elementary toposes (with/without NNO) $\simeq$ DFL comprehension categories with corresponding local properties (e.g., subobject classifiers, disjoint sums, quotients).
• Universes: Univalent elementary toposes with a universe closed under specific type formers $\simeq$ DFL comprehension categories with a universe object satisfying corresponding closure conditions.

The paper demonstrates that in univalent foundations, the internal language of these categorical structures is extensional Martin-Löf type theory. The use of univalent categories simplifies the theory by removing the need for split fibrations; the coherence issues that plague set-theoretic models (where substitution must hold strictly) are resolved because isomorphisms are identities.

Significance and Claims
The paper claims that its development provides a new perspective on the semantics of dependent type theory. By utilizing univalent categories, the author avoids the technical overhead of split fibrations and the axiom of choice, which are necessary in set-theoretic foundations to ensure soundness. The structure identity principles inherent in univalent foundations allow for a more natural treatment of categorical structures where objects are identified up to equivalence rather than strict equality.

The author explicitly states that they do not construct the syntax or the initial model in this work; rather, they focus on the categorical side of the internal language theorem (the equivalence between models). They note that while comprehension categories are suitable for univalent foundations, other structures like CwFs are not, due to the set-restriction on types. The paper positions itself as a foundational step, leaving the development of suitable syntax (such as groupoid syntax) and its interpretation as future work. The significance lies in establishing a robust, machine-checked correspondence between univalent categorical structures and type theories, demonstrating that univalent foundations naturally support these internal language theorems without the defects found in earlier set-theoretic formulations.