Axioms for Modelling Cubical Type Theory in a Topos
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...
| Main Authors: | , |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
Logical Methods in Computer Science e.V.
2018-12-01
|
| Series: | Logical Methods in Computer Science |
| Subjects: | |
| Online Access: | https://lmcs.episciences.org/4491/pdf |
| _version_ | 1797268583167819776 |
|---|---|
| author | Ian Orton Andrew M. Pitts |
| author_facet | Ian Orton Andrew M. Pitts |
| author_sort | Ian Orton |
| collection | DOAJ |
| description | 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.) |
| first_indexed | 2024-04-25T01:34:47Z |
| format | Article |
| id | doaj.art-b389b69bda97409c912297d69e08e367 |
| institution | Directory Open Access Journal |
| issn | 1860-5974 |
| language | English |
| last_indexed | 2024-04-25T01:34:47Z |
| publishDate | 2018-12-01 |
| publisher | Logical Methods in Computer Science e.V. |
| record_format | Article |
| series | Logical Methods in Computer Science |
| spelling | doaj.art-b389b69bda97409c912297d69e08e3672024-03-08T10:27:52ZengLogical Methods in Computer Science e.V.Logical Methods in Computer Science1860-59742018-12-01Volume 14, Issue 410.23638/LMCS-14(4:23)20184491Axioms for Modelling Cubical Type Theory in a ToposIan OrtonAndrew M. PittsThe 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.)https://lmcs.episciences.org/4491/pdfcomputer science - logic in computer sciencef.4.1 |
| spellingShingle | Ian Orton Andrew M. Pitts Axioms for Modelling Cubical Type Theory in a Topos Logical Methods in Computer Science computer science - logic in computer science f.4.1 |
| title | Axioms for Modelling Cubical Type Theory in a Topos |
| title_full | Axioms for Modelling Cubical Type Theory in a Topos |
| title_fullStr | Axioms for Modelling Cubical Type Theory in a Topos |
| title_full_unstemmed | Axioms for Modelling Cubical Type Theory in a Topos |
| title_short | Axioms for Modelling Cubical Type Theory in a Topos |
| title_sort | axioms for modelling cubical type theory in a topos |
| topic | computer science - logic in computer science f.4.1 |
| url | https://lmcs.episciences.org/4491/pdf |
| work_keys_str_mv | AT ianorton axiomsformodellingcubicaltypetheoryinatopos AT andrewmpitts axiomsformodellingcubicaltypetheoryinatopos |