Change search
ReferencesLink to record
Permanent link

Direct link
The local universes model: An overlooked coherence construction for dependent type theories
Stockholm University, Faculty of Science, Department of Mathematics.ORCID iD: 0000-0003-1390-2970
(English)Manuscript (preprint) (Other academic)
Abstract [en]

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.

Keyword [en]
dependent type theory, semantics, categorical logic
National Category
Research subject
Mathematical Logic
URN: urn:nbn:se:su:diva-112196OAI: diva2:778402
Available from: 2015-01-09 Created: 2015-01-09 Last updated: 2016-01-29Bibliographically approved

Open Access in DiVA

No full text

Other links


Search in DiVA

By author/editor
Lumsdaine, Peter LeFanu
By organisation
Department of Mathematics

Search outside of DiVA

GoogleGoogle Scholar
The number of downloads is the sum of all downloads of full texts. It may include eg previous versions that are now no longer available

Total: 9 hits
ReferencesLink to record
Permanent link

Direct link