Repository logo
 

Axioms for modelling cubical type theory in a topos

Published version
Peer-reviewed

Change log

Authors

Orton, I 
Pitts, AM 

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.)

Description

Keywords

models of dependent type theory, homotopy type theory, cubical sets, cubical type theory, topos, univalence

Journal Title

Logical Methods in Computer Science

Conference Name

Journal ISSN

1860-5974
1860-5974

Volume Title

14

Publisher

Logical Methods in Computer Science e.V.
Sponsorship
EPSRC (1641673)
Relationships
Is derived from: