LIPIcs.TYPES.2019.10.pdf
- Filesize: 436 kB
- 18 pages
Document
Higher Inductive Type Eliminators Without Paths
Author
Nils Anders Danielsson 
-
Part of:
Volume:
25th International Conference on Types for Proofs and Programs (TYPES 2019)
Series: Leibniz International Proceedings in Informatics (LIPIcs)
Conference: International Conference on Types for Proofs and Programs (TYPES) - License:
Creative Commons Attribution 3.0 Unported license
- Publication Date: 2020-09-24
File
Document Identifiers
Author Details
Acknowledgements
I would like to thank Anders Mörtberg and Andrea Vezzosi for helping me get to grips with Cubical Agda. I would also like to thank some anonymous reviewers for useful feedback.
Cite As Get BibTex
Nils Anders Danielsson. Higher Inductive Type Eliminators Without Paths. In 25th International Conference on Types for Proofs and Programs (TYPES 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 175, pp. 10:1-10:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
https://doi.org/10.4230/LIPIcs.TYPES.2019.10
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.
Subject Classification
ACM Subject Classification
- Theory of computation → Type theory
Keywords
- Cubical Agda
- higher inductive types
Metrics
- Access Statistics
-
Total Accesses (updated on a weekly basis)
0PDF Downloads
References
- The Agda Team. Agda User Manual, Release 2.6.1, 2020. URL: https://readthedocs.org/projects/agda/downloads/pdf/v2.6.1/.
- Cyril Cohen, Thierry Coquand, Simon Huber, and Anders Mörtberg. Cubical type theory: A constructive interpretation of the univalence axiom. In 21st International Conference on Types for Proofs and Programs, TYPES 2015, number 69 in LIPIcs, page 5:1–5:34, 2018. URL: https://doi.org/10.4230/LIPIcs.TYPES.2015.5.
- Nils Anders Danielsson. Code related to the paper "Higher Inductive Type Eliminators Without Paths", 2020. URL: https://doi.org/10.5281/zenodo.3941063.
-
Martin Hofmann and Thomas Streicher. The groupoid interpretation of type theory. In Twenty-five Years of Constructive Type Theory: Proceedings of a Congress Held in Venice, October 1995, volume 36 of Oxford Logic Guides, page 83–111. Oxford University Press, 1998.
- Anders Mörtberg, Andrea Vezzosi, et al. An experimental library for Cubical Agda. Agda code, 2020. URL: https://github.com/agda/cubical/.
- Andrew Swan. An algebraic weak factorisation system on 01-substitution sets: A constructive proof. Journal of Logic & Analysis, 8(1):1–35, 2016. URL: https://doi.org/10.4115/jla.2016.8.1.
- The Univalent Foundations Program. Homotopy Type Theory. URL: https://homotopytypetheory.org/book/, first edition, 2013.
- Andrea Vezzosi, Anders Mörtberg, and Andreas Abel. Cubical Agda: A dependently typed programming language with univalence and higher inductive types. Proceedings of the ACM on Programming Languages, 3(ICFP):87:1–87:29, 2019. URL: https://doi.org/10.1145/3341691.