dc.contributor.author Orton, I dc.contributor.author Pitts, AM dc.date.accessioned 2019-01-04T08:57:02Z dc.date.available 2019-01-04T08:57:02Z dc.date.issued 2018 dc.identifier.issn 1860-5974 dc.identifier.uri https://www.repository.cam.ac.uk/handle/1810/287526 dc.description.abstract The 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.iso en dc.publisher Logical Methods in Computer Science e.V. dc.rights Attribution 4.0 International dc.rights.uri http://creativecommons.org/licenses/by/4.0/ dc.title Axioms for modelling cubical type theory in a topos dc.type Article prism.issueIdentifier 4 prism.publicationDate 2018 prism.publicationName Logical Methods in Computer Science prism.volume 14 dc.identifier.doi 10.17863/CAM.34826 dcterms.dateAccepted 2018-09-22 rioxxterms.versionofrecord 10.23638/LMCS-14(4:23)2018 rioxxterms.version VoR rioxxterms.licenseref.uri http://www.rioxx.net/licenses/all-rights-reserved rioxxterms.licenseref.startdate 2018-01-01 dc.contributor.orcid Pitts, Andrew [0000-0001-7775-3471] dc.identifier.eissn 1860-5974 rioxxterms.type Journal Article/Review pubs.funder-project-id EPSRC (1641673) cam.issuedOnline 2018-12-11 cam.orpheus.success Thu Jan 30 10:52:50 GMT 2020 - The item has an open VoR version. datacite.isderivedfrom.doi 10.4230/LIPIcs.CSL.2016.24 rioxxterms.freetoread.startdate 2100-01-01
﻿

### This item appears in the following Collection(s)

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