License: Creative Commons Attribution 3.0 Unported license (CC BY 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.TYPES.2015.3
URN: urn:nbn:de:0030-drops-84739
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2018/8473/
Go to the corresponding LIPIcs Volume Portal

Altenkirch, Thorsten ; Kaposi, Ambrus

Towards a Cubical Type Theory without an Interval

pdf-format:
LIPIcs-TYPES-2015-3.pdf (0.6 MB)

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 do not 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.

BibTeX - Entry

@InProceedings{altenkirch_et_al:LIPIcs:2018:8473,
  author =	{Thorsten Altenkirch and Ambrus Kaposi},
  title =	{{Towards a Cubical Type Theory without an Interval}},
  booktitle =	{21st International Conference on Types for Proofs and Programs (TYPES 2015)},
  pages =	{3:1--3:27},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-030-9},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{69},
  editor =	{Tarmo Uustalu},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2018/8473},
  URN =		{urn:nbn:de:0030-drops-84739},
  doi =		{10.4230/LIPIcs.TYPES.2015.3},
  annote =	{Keywords: homotopy type theory, parametricity, univalence}
}

Keywords: homotopy type theory, parametricity, univalence
Collection: 21st International Conference on Types for Proofs and Programs (TYPES 2015)
Issue Date: 2018
Date of publication: 15.03.2018

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI