Creative Commons Attribution 3.0 Unported license (CC-BY 3.0)when quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.FSCD.2018.22
URN: urn:nbn:de:0030-drops-91929
URL: https://drops.dagstuhl.de/opus/volltexte/2018/9192/
Licata, Daniel R. ; Orton, Ian ; Pitts, Andrew M. ; Spitters, Bas
Internal Universes in Models of Homotopy Type Theory
| pdf-format: |
|
Abstract
We begin by recalling the essentially global character of universes in various models of homotopy type theory, which prevents a straightforward axiomatization of their properties using the internal language of the presheaf toposes from which these model are constructed. We get around this problem by extending the internal language with a modal operator for expressing properties of global elements. In this setting we show how to construct a universe that classifies the Cohen-Coquand-Huber-Mörtberg (CCHM) notion of fibration from their cubical sets model, starting from the assumption that the interval is tiny - a property that the interval in cubical sets does indeed have. This leads to an elementary axiomatization of that and related models of homotopy type theory within what we call crisp type theory.
BibTeX - Entry
@InProceedings{licata_et_al:LIPIcs:2018:9192,
author = {Daniel R. Licata and Ian Orton and Andrew M. Pitts and Bas Spitters},
title = {{Internal Universes in Models of Homotopy Type Theory}},
booktitle = {3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018)},
pages = {22:1--22:17},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-077-4},
ISSN = {1868-8969},
year = {2018},
volume = {108},
editor = {H{\'e}l{\`e}ne Kirchner},
publisher = {Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
address = {Dagstuhl, Germany},
URL = {http://drops.dagstuhl.de/opus/volltexte/2018/9192},
URN = {urn:nbn:de:0030-drops-91929},
doi = {10.4230/LIPIcs.FSCD.2018.22},
annote = {Keywords: cubical sets, dependent type theory, homotopy type theory, internal language, modalities, univalent foundations, universes}
}
| Keywords: | cubical sets, dependent type theory, homotopy type theory, internal language, modalities, univalent foundations, universes | |
| Seminar: | 3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018) | |
| Issue date: | 2018 | |
| Date of publication: | 04.07.2018 | |
| Supplementary Material: | https://doi.org/10.17863/CAM.22369 (Agda-flat source code) |
