The internal languages of univalent categories
Niels van der Weide
TL;DR
The paper extends Clairambault–Dybjer’s internal-language correspondence to univalent foundations by developing a biequivalence between bicategories of univalent categories (and topoi) and bicategories of comprehension categories enriched with type formers. It builds a modular framework using displayed bicategories to realize FullComprehensionCat and DFLComprehensionCat, then proves biequivalences with FinLim, LCCC, Toposes, and universes, leveraging local properties and universe semantics. It also formalizes the results in the Rocq/UniMath ecosystem, and generalizes the internal language to include universe-level type formers in elementary toposes, such as NNO, subobject classifiers, and propositional resizing. The work broadens the semantic reach of dependent type theory in univalent contexts and provides a robust, scalable approach to internal languages across several categorical landscapes, with potential extensions to predicative settings and higher-dimensional types.
Abstract
Internal language theorems are fundamental in categorical logic, since they express an equivalence between syntax and semantics. One of such theorems was proven by Clairambault and Dybjer, who corrected the result originally by Seely. More specifically, they constructed a biequivalence between the bicategory of locally Cartesian closed categories and the bicategory of democratic categories with families with extensional identity types, $\sum$-types, and $\prod$-types. This theorem expresses that the internal language of locally Cartesian closed categories is extensional Martin-Löf type theory with dependent sums and products. In this paper, we study the theorem by Clairambault and Dybjer for univalent categories, and we extend it to various classes of toposes, among which are $\prod$-pretoposes, elementary toposes, and elementary toposes with a universe. The results in this paper have been formalized using the proof assistant Rocq and the UniMath library.