Show simple item record

dc.contributor.authorOrton, I
dc.contributor.authorPitts, AM
dc.date.accessioned2019-01-04T08:57:02Z
dc.date.available2019-01-04T08:57:02Z
dc.date.issued2018
dc.identifier.issn1860-5974
dc.identifier.urihttps://www.repository.cam.ac.uk/handle/1810/287526
dc.description.abstractThe homotopical approach to intensional type theory views proofs of equality as paths. We explore what is required of an object $I$ in a topos to give such a path-based model of type theory in which paths are just functions with domain $I$. Cohen, Coquand, Huber and M\"ortberg give such a model using a particular category of presheaves. We investigate the extent to which their model construction can be expressed in the internal type theory of any topos and identify a collection of quite weak axioms for this purpose. This clarifies the definition and properties of the notion of uniform Kan filling that lies at the heart of their constructive interpretation of Voevodsky's univalence axiom. (This paper is a revised and expanded version of a paper of the same name that appeared in the proceedings of the 25th EACSL Annual Conference on Computer Science Logic, CSL 2016.)
dc.language.isoen
dc.publisherLogical Methods in Computer Science e.V.
dc.rightsAttribution 4.0 International
dc.rights.urihttp://creativecommons.org/licenses/by/4.0/
dc.titleAxioms for modelling cubical type theory in a topos
dc.typeArticle
prism.issueIdentifier4
prism.publicationDate2018
prism.publicationNameLogical Methods in Computer Science
prism.volume14
dc.identifier.doi10.17863/CAM.34826
dcterms.dateAccepted2018-09-22
rioxxterms.versionofrecord10.23638/LMCS-14(4:23)2018
rioxxterms.versionVoR
rioxxterms.licenseref.urihttp://www.rioxx.net/licenses/all-rights-reserved
rioxxterms.licenseref.startdate2018-01-01
dc.contributor.orcidPitts, Andrew [0000-0001-7775-3471]
dc.identifier.eissn1860-5974
rioxxterms.typeJournal Article/Review
pubs.funder-project-idEPSRC (1641673)
cam.issuedOnline2018-12-11
cam.orpheus.successThu Jan 30 10:52:50 GMT 2020 - The item has an open VoR version.
datacite.isderivedfrom.doi10.4230/LIPIcs.CSL.2016.24
rioxxterms.freetoread.startdate2100-01-01


Files in this item

Thumbnail
Thumbnail

This item appears in the following Collection(s)

Show simple item record

Attribution 4.0 International
Except where otherwise noted, this item's licence is described as Attribution 4.0 International