Publication date
January 2014
DOI Publisher
LIPIcs - Leibniz International Proceedings in Informatics. 19th International Conference on Types for Proofs and Programs (TYPES 2013)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\u27s Univalence Axiom
Add to ORKG