The local universes model: an overlooked coherence construction for dependent type theories

Abstract

We present a new coherence theorem for comprehension categories, providing strict models of dependent type theory with all standard constructors, including dependent products, dependent sums, identity types, and other inductive types. Precisely, we take as input a "weak model": a comprehension category, equipped with structure corresponding to the desired logical constructions. We assume throughout that the base category is close to locally Cartesian closed: specifically, that products and certain exponentials exist. Beyond this, we require only that the logical structure should be *weakly stable* --- a pure existence statement, not involving any specific choice of structure, weaker than standard categorical Beck--Chevalley conditions, and holding in the now standard homotopy-theoretic models of type theory. Given such a comprehension category, we construct an equivalent split one, whose logical structure is strictly stable under reindexing. This yields an interpretation of type theory with the chosen constructors. The model is adapted from Voevodsky's use of universes for coherence, and at the level of fibrations is a classical construction of Giraud. It may be viewed in terms of local universes or delayed substitutions.

36 pages. Definition of "pseudo-stable" corrected from earlier version. To appear in ACM Transactions on Computational Logic

References in corpus (2)

• Homotopy theoretic models of identity types
• The identity type weak factorisation system

Cited by in corpus (17)

• Modalities in homotopy type theory
• Semantics of higher inductive types
• Dialectica models of type theory
• Models of Martin-Löf type theory from algebraic weak factorisation systems
• Affine logic for constructive mathematics
• Univalence and completeness of Segal objects
• Displayed Categories
• A homotopy-theoretic model of function extensionality in the effective topos
• A type theory for synthetic $\infty$-categories
• Locally Cartesian Closed Quasicategories from Type Theory
• Exact completion of path categories and algebraic set theory -- Part I: Exact completion of path categories
• Homotopical inverse diagrams in categories with attributes
• On the $\infty$-topos semantics of homotopy type theory
• Identity types and weak factorization systems in Cauchy complete categories
• Models of Type Theory Based on Moore Paths
• Formalizing two-level type theory with cofibrant exo-nat
• Relative elegance and cartesian cubes with one connection