dc.contributor.author | Bezem, Marcus Aloysius | eng |
dc.contributor.author | Coquand, Thierry | eng |
dc.contributor.author | Huber, Simon | eng |
dc.date.accessioned | 2015-08-05T11:33:22Z | |
dc.date.available | 2015-08-05T11:33:22Z | |
dc.date.issued | 2014 | |
dc.identifier.issn | 1868-8969 | en_US |
dc.identifier.uri | https://hdl.handle.net/1956/10215 | |
dc.description.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. | en_US |
dc.language.iso | eng | eng |
dc.publisher | Schloss Dagstuhl - Leibniz-Zentrum für Informatik | en_US |
dc.rights | Attribution CC BY | eng |
dc.rights.uri | http://creativecommons.org/licenses/by/3.0/ | eng |
dc.subject | models of dependent type theory | eng |
dc.subject | cubical sets | eng |
dc.subject | univalent foundations | eng |
dc.title | A Model of Type Theory in Cubical Sets | en_US |
dc.type | Peer reviewed | |
dc.type | Journal article | |
dc.date.updated | 2015-08-05T11:23:00Z | |
dc.description.version | publishedVersion | en_US |
dc.rights.holder | Copyright 2014 The Authors | en_US |
dc.identifier.doi | https://doi.org/10.4230/lipics.types.2013.107 | |
dc.identifier.cristin | 1199877 | |
dc.source.journal | Leibniz International Proceedings in Informatics | |
dc.source.40 | 26 | |
dc.source.pagenumber | 107-128 | |
dc.subject.nsi | VDP::Matematikk og Naturvitenskap: 400::Matematikk: 410::Logikk: 416 | en_US |