Towards a cubical type theory without an interval
Following the cubical set model of type theory which validates the univalence axiom, cubical type theories have been developed that interpret the identity type using an interval pretype. These theories start from a geometric view of equality. A proof of equality is encoded as a term in a context ext...
| Main Authors: | , |
|---|---|
| Format: | Article |
| Published: |
Dagstuhl Publishing
2017
|
| Subjects: | |
| Online Access: | https://eprints.nottingham.ac.uk/44008/ |
| _version_ | 1848796815859646464 |
|---|---|
| author | Altenkirch, Thorsten Kaposi, Ambrus |
| author_facet | Altenkirch, Thorsten Kaposi, Ambrus |
| author_sort | Altenkirch, Thorsten |
| building | Nottingham Research Data Repository |
| collection | Online Access |
| description | Following the cubical set model of type theory which validates the univalence axiom, cubical type theories have been developed that interpret the identity type using an interval pretype. These theories start from a geometric view of equality. A proof of equality is encoded as a term in a context extended by the interval pretype. Our goal is to develop a cubical theory where the identity type is defined recursively over the type structure, and the geometry arises from these definitions. In this theory, cubes are present explicitly, e.g. a line is a telescope with 3 elements: two endpoints and the connecting equality. This is in line with Bernardy and Moulin's earlier work on internal parametricity. In this paper we present a naive syntax for internal parametricity and by replacing the parametric interpretation of the universe, we extend it to univalence. However, we don't know how to compute in this theory. As a second step, we present a version of the theory for parametricity with named dimensions which has an operational semantics. Extending this syntax to univalence is left as further work. |
| first_indexed | 2025-11-14T19:53:59Z |
| format | Article |
| id | nottingham-44008 |
| institution | University of Nottingham Malaysia Campus |
| institution_category | Local University |
| last_indexed | 2025-11-14T19:53:59Z |
| publishDate | 2017 |
| publisher | Dagstuhl Publishing |
| recordtype | eprints |
| repository_type | Digital Repository |
| spelling | nottingham-440082020-05-04T18:42:16Z https://eprints.nottingham.ac.uk/44008/ Towards a cubical type theory without an interval Altenkirch, Thorsten Kaposi, Ambrus Following the cubical set model of type theory which validates the univalence axiom, cubical type theories have been developed that interpret the identity type using an interval pretype. These theories start from a geometric view of equality. A proof of equality is encoded as a term in a context extended by the interval pretype. Our goal is to develop a cubical theory where the identity type is defined recursively over the type structure, and the geometry arises from these definitions. In this theory, cubes are present explicitly, e.g. a line is a telescope with 3 elements: two endpoints and the connecting equality. This is in line with Bernardy and Moulin's earlier work on internal parametricity. In this paper we present a naive syntax for internal parametricity and by replacing the parametric interpretation of the universe, we extend it to univalence. However, we don't know how to compute in this theory. As a second step, we present a version of the theory for parametricity with named dimensions which has an operational semantics. Extending this syntax to univalence is left as further work. Dagstuhl Publishing 2017-04-20 Article PeerReviewed Altenkirch, Thorsten and Kaposi, Ambrus (2017) Towards a cubical type theory without an interval. Leibniz International Proceedings in Informatics . ISSN 1868-8969 (In Press) homotopy type theory parametricity univalence |
| spellingShingle | homotopy type theory parametricity univalence Altenkirch, Thorsten Kaposi, Ambrus Towards a cubical type theory without an interval |
| title | Towards a cubical type theory without an interval |
| title_full | Towards a cubical type theory without an interval |
| title_fullStr | Towards a cubical type theory without an interval |
| title_full_unstemmed | Towards a cubical type theory without an interval |
| title_short | Towards a cubical type theory without an interval |
| title_sort | towards a cubical type theory without an interval |
| topic | homotopy type theory parametricity univalence |
| url | https://eprints.nottingham.ac.uk/44008/ |