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.2019.10
URN: urn:nbn:de:0030-drops-130749
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2020/13074/
Go to the corresponding LIPIcs Volume Portal

Danielsson, Nils Anders

Higher Inductive Type Eliminators Without Paths

pdf-format:
LIPIcs-TYPES-2019-10.pdf (0.4 MB)

Abstract

Cubical Agda has support for higher inductive types. Paths are integral to the working of this feature. However, there are other notions of equality. For instance, Cubical Agda comes with an identity type family for which the J rule computes in the usual way when applied to the canonical proof of reflexivity, whereas typical implementations of the J rule for paths do not.
This text shows how one can use some of the higher inductive types definable in Cubical Agda with arbitrary notions of equality satisfying certain axioms. The method works for several examples taken from the HoTT book, including the interval, the circle, suspensions, pushouts, the propositional truncation, a general truncation operator, and set quotients.

BibTeX - Entry

@InProceedings{danielsson:LIPIcs:2020:13074,
  author =	{Nils Anders Danielsson},
  title =	{{Higher Inductive Type Eliminators Without Paths}},
  booktitle =	{25th International Conference on Types for Proofs and Programs (TYPES 2019)},
  pages =	{10:1--10:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-158-0},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{175},
  editor =	{Marc Bezem and Assia Mahboubi},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/opus/volltexte/2020/13074},
  URN =		{urn:nbn:de:0030-drops-130749},
  doi =		{10.4230/LIPIcs.TYPES.2019.10},
  annote =	{Keywords: Cubical Agda, higher inductive types}
}

Keywords: Cubical Agda, higher inductive types
Collection: 25th International Conference on Types for Proofs and Programs (TYPES 2019)
Issue Date: 2020
Date of publication: 24.09.2020
Supplementary Material: Accompanying Agda code is available to download (https://doi.org/10.5281/zenodo.3941063).

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