Creative Commons Attribution 3.0 Unported license (CC-BY 3.0)when quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.TYPES.2013.107
URN: urn:nbn:de:0030-drops-46284
URL: https://drops.dagstuhl.de/opus/volltexte/2014/4628/
Bezem, Marc ; Coquand, Thierry ; Huber, Simon
A Model of Type Theory in Cubical Sets
| pdf-format: |
|
Abstract
We present a model of type theory with dependent product, sum, and identity, in cubical sets. We describe a universe and explain how to transform an equivalence between two types into an equality. We also explain how to model propositional truncation and the circle. While not expressed internally in type theory, the model is expressed in a constructive metalogic. Thus it is a step towards a computational interpretation of Voevodsky's Univalence Axiom.
BibTeX - Entry
@InProceedings{bezem_et_al:LIPIcs:2014:4628,
author = {Marc Bezem and Thierry Coquand and Simon Huber},
title = {{A Model of Type Theory in Cubical Sets}},
booktitle = {19th International Conference on Types for Proofs and Programs (TYPES 2013)},
pages = {107--128},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-72-9},
ISSN = {1868-8969},
year = {2014},
volume = {26},
editor = {Ralph Matthes and Aleksy Schubert},
publisher = {Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
address = {Dagstuhl, Germany},
URL = {http://drops.dagstuhl.de/opus/volltexte/2014/4628},
URN = {urn:nbn:de:0030-drops-46284},
doi = {10.4230/LIPIcs.TYPES.2013.107},
annote = {Keywords: Models of dependent type theory, cubical sets, Univalent Foundations}
}
| Keywords: | Models of dependent type theory, cubical sets, Univalent Foundations | |
| Seminar: | 19th International Conference on Types for Proofs and Programs (TYPES 2013) | |
| Issue date: | 2014 | |
| Date of publication: | 25.07.2014 |
