Non-Wellfounded Trees in Homotopy Type Theory

Authors Benedikt Ahrens, Paolo Capriotti, Régis Spadotti

Thumbnail PDF


  • Filesize: 0.53 MB
  • 14 pages

Document Identifiers

Author Details

Benedikt Ahrens
Paolo Capriotti
Régis Spadotti

Cite AsGet BibTex

Benedikt Ahrens, Paolo Capriotti, and Régis Spadotti. Non-Wellfounded Trees in Homotopy Type Theory. In 13th International Conference on Typed Lambda Calculi and Applications (TLCA 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 38, pp. 17-30, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)


We prove a conjecture about the constructibility of conductive types - in the principled form of indexed M-types - in Homotopy Type Theory. The conjecture says that in the presence of inductive types, coinductive types are derivable. Indeed, in this work, we construct coinductive types in a subsystem of Homotopy Type Theory; this subsystem is given by Intensional Martin-Löf type theory with natural numbers and Voevodsky's Univalence Axiom. Our results are mechanized in the computer proof assistant Agda.
  • Homotopy Type Theory
  • coinductive types
  • computer theorem proving
  • Agda


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


  1. Michael Abbott, Thorsten Altenkirch, and Neil Ghani. Containers: Constructing strictly positive types. Theor. Comput. Sci., 342(1):3-27, 2005. URL:
  2. Benedikt Ahrens, Paolo Capriotti, and Régis Spadotti. Non-wellfounded trees in Homotopy Type Theory, 2015. URL:
  3. Benedikt Ahrens, Krzysztof Kapulkin, and Michael Shulman. Univalent categories and the Rezk completion. Mathematical Structures in Computer Science, FirstView:1-30, 1 2015. URL:
  4. Thorsten Altenkirch, Neil Ghani, Peter Hancock, Conor McBride, and Peter Morris. Indexed Containers. available at URL:
  5. Jeremy Avigad, Krzysztof Kapulkin, and Peter LeFanu Lumsdaine. Homotopy limits in type theory. Mathematical Structures in Computer Science, FirstView:1-31, 1 2015. URL:
  6. Steve Awodey, Nicola Gambino, and Kristina Sojakova. Inductive types in homotopy type theory. In Proceedings of Symposium on Logic In Computer Science, pages 95-104, 2012. URL:
  7. Michael Barr. Terminal coalgebras in well-founded set theory. Theor. Comput. Sci., 114(2):299-315, 1993. URL:
  8. James Cranch. Concrete Categories in Homotopy Type Theory, 2013. URL:
  9. Chris Kapulkin, Peter LeFanu Lumsdaine, and Vladimir Voevodsky. The Simplicial Model of Univalent Foundations, 2014. URL:
  10. HoTT mailing list. Discussion on coinductive types on HoTT mailing list, URL:
  11. Per Martin-Löf. Intuitionistic Type Theory. Bibliopolis, 1984. Google Scholar
  12. Kristina Sojakova. Higher inductive types as homotopy-initial algebras. In Proceedings of the Symposium on Principles of Programming Languages, pages 31-42, 2015. URL:
  13. The Univalent Foundations Program. Homotopy Type Theory: Univalent Foundations of Mathematics., Institute for Advanced Study, 2013.
  14. Benno van den Berg and Federico De Marchi. Non-well-founded trees in categories. Ann. Pure Appl. Logic, 146(1):40-59, 2007. URL:
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