Show simple item record

A Model of Type Theory in Cubical Sets

dc.contributor.authorBezem, Marcus Aloysiuseng
dc.contributor.authorCoquand, Thierryeng
dc.contributor.authorHuber, Simoneng
dc.date.accessioned2015-08-05T11:33:22Z
dc.date.available2015-08-05T11:33:22Z
dc.date.issued2014
dc.identifier.issn1868-8969en_US
dc.identifier.urihttps://hdl.handle.net/1956/10215
dc.description.abstractWe 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.isoengeng
dc.publisherSchloss Dagstuhl - Leibniz-Zentrum für Informatiken_US
dc.rightsAttribution CC BYeng
dc.rights.urihttp://creativecommons.org/licenses/by/3.0/eng
dc.subjectmodels of dependent type theoryeng
dc.subjectcubical setseng
dc.subjectunivalent foundationseng
dc.titleA Model of Type Theory in Cubical Setsen_US
dc.typePeer reviewed
dc.typeJournal article
dc.date.updated2015-08-05T11:23:00Z
dc.description.versionpublishedVersionen_US
dc.rights.holderCopyright 2014 The Authorsen_US
dc.identifier.doihttps://doi.org/10.4230/lipics.types.2013.107
dc.identifier.cristin1199877
dc.source.journalLeibniz International Proceedings in Informatics
dc.source.4026
dc.source.pagenumber107-128
dc.subject.nsiVDP::Matematikk og Naturvitenskap: 400::Matematikk: 410::Logikk: 416en_US


Files in this item

Thumbnail
Name:
7.pdf
Size:
587.5Kb
Format:
PDF
View/Open

This item appears in the following Collection(s)

Show simple item record

Attribution CC BY
Except where otherwise noted, this item's license is described as Attribution CC BY