Vis enkel innførsel

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


Tilhørende fil(er)

Thumbnail
Filnavn:
7.pdf
Størrelse:
587.5Kb
Format:
PDF
Åpne

Denne innførselen finnes i følgende samling(er)

Vis enkel innførsel

Attribution CC BY
Med mindre annet er angitt, så er denne innførselen lisensiert som Attribution CC BY