The univalence axiom in cubical sets
Logic
2017-10-31 v1 Logic in Computer Science
Abstract
In this note we show that Voevodsky's univalence axiom holds in the model of type theory based on symmetric cubical sets. 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.
Cite
@article{arxiv.1710.10941,
title = {The univalence axiom in cubical sets},
author = {Marc Bezem and Thierry Coquand and Simon Huber},
journal= {arXiv preprint arXiv:1710.10941},
year = {2017}
}
Comments
12 pages