Sidansvarig: Webbredaktion
Sidan uppdaterades: 2012-09-11 15:12
| Författare |
M. Bezem Thierry Coquand Simon Huber |
|---|---|
| Publicerad i | Journal of Automated Reasoning |
| Volym | 63 |
| Nummer/häfte | 2 |
| Sidor | 159-171 |
| ISSN | 0168-7433 |
| Publiceringsår | 2019 |
| Publicerad vid |
Institutionen för data- och informationsteknik, datavetenskap, programmeringslogik (GU) Institutionen för data- och informationsteknik (GU) |
| Sidor | 159-171 |
| Språk | en |
| Länkar |
dx.doi.org/10.1007/s10817-018-9472-... |
| Ämnesord | Dependent type theory, Univalence axiom, Cubical sets, Computer Science |
| Ämneskategorier | Data- och informationsvetenskap |
In this note we show that Voevodsky's univalence axiom holds in the model of type theory based on cubical sets as described inBezem et al. (in: Matthes and Schubert (eds.) 19th international conference on types for proofs and programs (TYPES 2013), Leibniz international proceedings in informatics (LIPIcs), Schloss Dagstuhl-Leibniz-Zentrum fur Informatik, Dagstuhl, Germany, vol26, pp 107-128, 2014. 10.4230/LIPIcs.TYPES.2013.107. http://drops.dagstuhl.de/opus/volltexte/2014/4628) and Huber (A model of type theory in cubical sets. Licentiate thesis, University of Gothenburg, 2015). We will also discuss Swan's construction of the identity type in this variation of cubical sets. This proves that we have a model of type theory supporting dependent products, dependent sums, univalent universes, and identity types with the usual judgmental equality, and this model is formulated in a constructive metatheory.
GÖTEBORGS UNIVERSITET • Box 100 • 405 30 Göteborg • Telefon: 031 786 0000
Kontakt • Organisationsnummer: 202100-3153 • Om webbplatsen
Facebook
Twitter
Instagram
Youtube