Change search
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf
The Local Universes Model: An Overlooked Coherence Construction for Dependent Type Theories
Institute for Advanced Study, Princeton, New Jersey, U.S.A..ORCID iD: 0000-0003-1390-2970
Institute for Advanced Study, Princeton, New Jersey, U.S.A..ORCID iD: 0000-0002-3221-4797
2015 (English)In: ACM Transactions on Computational Logic, ISSN 1529-3785, E-ISSN 1557-945X, Vol. 16, no 3, article id 23Article in journal (Refereed) Published
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. 

Place, publisher, year, edition, pages
2015. Vol. 16, no 3, article id 23
Keywords [en]
dependent type theory, categorical semantics, comprehension categories, coherence theorems
National Category
Algebra and Logic
Research subject
Mathematical Logic
Identifiers
URN: urn:nbn:se:su:diva-128393DOI: 10.1145/2754931OAI: oai:DiVA.org:su-128393DiVA, id: diva2:914762
Available from: 2016-03-25 Created: 2016-03-25 Last updated: 2018-05-08Bibliographically approved

Open Access in DiVA

fulltext(753 kB)1 downloads
File information
File name FULLTEXT01.pdfFile size 753 kBChecksum SHA-512
6f5fefe88a17ddec063ec4b2b3c2e860354a996cb4746b54792b862c7a6961ee28dfdafc6bb1a60253609acdc4475f14ae2e88a06120251d5621e2aba9da0f41
Type fulltextMimetype application/pdf

Other links

Publisher's full textarXiv:1411.1736

Search in DiVA

By author/editor
Lumsdaine, Peter LeFanuWarren, Michael A.
In the same journal
ACM Transactions on Computational Logic
Algebra and Logic

Search outside of DiVA

GoogleGoogle Scholar
Total: 1 downloads
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

doi
urn-nbn

Altmetric score

doi
urn-nbn
Total: 25 hits
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf