Non-Wellfounded Trees in Homotopy Type Theory

Authors Benedikt Ahrens, Paolo Capriotti, Régis Spadotti



PDF
Thumbnail PDF

File

LIPIcs.TLCA.2015.17.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)
https://doi.org/10.4230/LIPIcs.TLCA.2015.17

Abstract

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.
Keywords
  • Homotopy Type Theory
  • coinductive types
  • computer theorem proving
  • Agda

Metrics

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

References

  1. Michael Abbott, Thorsten Altenkirch, and Neil Ghani. Containers: Constructing strictly positive types. Theor. Comput. Sci., 342(1):3-27, 2005. URL: http://dx.doi.org/10.1016/j.tcs.2005.06.002.
  2. Benedikt Ahrens, Paolo Capriotti, and Régis Spadotti. Non-wellfounded trees in Homotopy Type Theory, 2015. URL: http://arxiv.org/abs/1504.02949.
  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: http://dx.doi.org/10.1017/S0960129514000486.
  4. Thorsten Altenkirch, Neil Ghani, Peter Hancock, Conor McBride, and Peter Morris. Indexed Containers. available at URL: http://www.cs.nott.ac.uk/~txa/publ/jcont.pdf.
  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: http://dx.doi.org/10.1017/S0960129514000498.
  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: http://dx.doi.org/10.1109/LICS.2012.21.
  7. Michael Barr. Terminal coalgebras in well-founded set theory. Theor. Comput. Sci., 114(2):299-315, 1993. URL: http://dx.doi.org/10.1016/0304-3975(93)90076-6.
  8. James Cranch. Concrete Categories in Homotopy Type Theory, 2013. URL: http://arxiv.org/abs/1311.1852.
  9. Chris Kapulkin, Peter LeFanu Lumsdaine, and Vladimir Voevodsky. The Simplicial Model of Univalent Foundations, 2014. URL: http://arxiv.org/abs/1211.2851.
  10. HoTT mailing list. Discussion on coinductive types on HoTT mailing list, URL: https://groups.google.com/d/msg/homotopytypetheory/tYRTcI2Opyo/PIrI6t5me-oJ.
  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: http://dx.doi.org/10.1145/2676726.2676983.
  13. The Univalent Foundations Program. Homotopy Type Theory: Univalent Foundations of Mathematics. http://homotopytypetheory.org/book, 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: http://arxiv.org/abs/math/0409158.
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail