A Model of Type Theory in Cubical Sets

Bezem, Marcus Aloysius; Coquand, Thierry; Huber, Simon
Peer reviewed, Journal article
Published version
Thumbnail
View/Open
URI
https://hdl.handle.net/1956/10215
Date
2014
Metadata
Show full item record
Collections
Original version
https://doi.org/10.4230/lipics.types.2013.107
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.
Publisher
Schloss Dagstuhl - Leibniz-Zentrum für Informatik
Journal
Leibniz International Proceedings in Informatics
Copyright
Copyright 2014 The Authors
Attribution CC BY
Except where otherwise noted, this item's license is described as Attribution CC BY