Higher Inductive Type Eliminators Without Paths

Author Nils Anders Danielsson

Thumbnail PDF


  • Filesize: 436 kB
  • 18 pages

Document Identifiers

Author Details

Nils Anders Danielsson
  • University of Gothenburg, Sweden


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 AsGet 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)


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
  • Cubical Agda
  • higher inductive types


  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    PDF Downloads


  1. The Agda Team. Agda User Manual, Release 2.6.1, 2020. URL: https://readthedocs.org/projects/agda/downloads/pdf/v2.6.1/.
  2. 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.
  3. Nils Anders Danielsson. Code related to the paper "Higher Inductive Type Eliminators Without Paths", 2020. URL: https://doi.org/10.5281/zenodo.3941063.
  4. 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. Google Scholar
  5. Anders Mörtberg, Andrea Vezzosi, et al. An experimental library for Cubical Agda. Agda code, 2020. URL: https://github.com/agda/cubical/.
  6. 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.
  7. The Univalent Foundations Program. Homotopy Type Theory. URL: https://homotopytypetheory.org/book/, first edition, 2013.
  8. 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.
Questions / Remarks / Feedback

Feedback for Dagstuhl Publishing

Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail