Skip to main content

Research Repository

Advanced Search

Towards a cubical type theory without an interval

Altenkirch, Thorsten; Kaposi, Ambrus

Towards a cubical type theory without an interval Thumbnail


Authors

Ambrus Kaposi



Abstract

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.

Citation

Altenkirch, T., & Kaposi, A. (2018). Towards a cubical type theory without an interval. LIPIcs, 3:1-3:27. https://doi.org/10.4230/LIPIcs.TYPES.2015.3

Journal Article Type Article
Acceptance Date Apr 20, 2017
Online Publication Date Mar 15, 2018
Publication Date 2018
Deposit Date Jul 7, 2017
Publicly Available Date Mar 15, 2018
Journal Leibniz International Proceedings in Informatics
Electronic ISSN 1868-8969
Publisher Schloss Dagstuhl - Leibniz-Zentrum für Informatik
Peer Reviewed Peer Reviewed
Article Number 3
Pages 3:1-3:27
DOI https://doi.org/10.4230/LIPIcs.TYPES.2015.3
Keywords homotopy type theory, parametricity, univalence
Public URL https://nottingham-repository.worktribe.com/output/856486
Publisher URL https://drops.dagstuhl.de/opus/volltexte/2018/8473/
Additional Information 21st International Conference on Types for Proofs and Programs (TYPES 2015)
Contract Date Jul 7, 2017

Files





You might also like



Downloadable Citations