To the top

Page Manager: Webmaster
Last update: 9/11/2012 3:13 PM

Tell a friend about this page
Print version

The Univalence Axiom in C… - University of Gothenburg, Sweden Till startsida
Sitemap
To content Read more about how we use cookies on gu.se

Contact form








 


Note! If you want an answer on a question you must specify your email address




The Univalence Axiom in Cubical Sets

Journal article
Authors M. Bezem
Thierry Coquand
Simon Huber
Published in Journal of Automated Reasoning
Volume 63
Issue 2
Pages 159-171
ISSN 0168-7433
Publication year 2019
Published at Department of Computer Science and Engineering, Computing Science, Programming Logic
Department of Computer Science and Engineering (GU)
Pages 159-171
Language en
Links dx.doi.org/10.1007/s10817-018-9472-...
Keywords Dependent type theory, Univalence axiom, Cubical sets, Computer Science
Subject categories Computer and Information Science

Abstract

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.

Page Manager: Webmaster|Last update: 9/11/2012
Share:

The University of Gothenburg uses cookies to provide you with the best possible user experience. By continuing on this website, you approve of our use of cookies.  What are cookies?