LIPIcs.TLCA.2015.17.pdf
- Filesize: 0.53 MB
- 14 pages
Document
Non-Wellfounded Trees in Homotopy Type Theory
Authors
-
Part of:
Volume:
13th International Conference on Typed Lambda Calculi and Applications (TLCA 2015)
Series: Leibniz International Proceedings in Informatics (LIPIcs)
Conference: International Conference on Typed Lambda Calculi and Applications (TLCA) - License:
Creative Commons Attribution 3.0 Unported license
- Publication Date: 2015-06-15
Cite As Get 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.
Subject Classification
Keywords
- Homotopy Type Theory
- coinductive types
- computer theorem proving
- Agda
Metrics
- Access Statistics
-
Total Accesses (updated on a weekly basis)
0PDF Downloads
References
- 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.
- Benedikt Ahrens, Paolo Capriotti, and Régis Spadotti. Non-wellfounded trees in Homotopy Type Theory, 2015. URL: http://arxiv.org/abs/1504.02949.
- 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.
- 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.
- 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.
- 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.
- 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.
- James Cranch. Concrete Categories in Homotopy Type Theory, 2013. URL: http://arxiv.org/abs/1311.1852.
- Chris Kapulkin, Peter LeFanu Lumsdaine, and Vladimir Voevodsky. The Simplicial Model of Univalent Foundations, 2014. URL: http://arxiv.org/abs/1211.2851.
- HoTT mailing list. Discussion on coinductive types on HoTT mailing list, URL: https://groups.google.com/d/msg/homotopytypetheory/tYRTcI2Opyo/PIrI6t5me-oJ.
-
Per Martin-Löf. Intuitionistic Type Theory. Bibliopolis, 1984.
- 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.
- The Univalent Foundations Program. Homotopy Type Theory: Univalent Foundations of Mathematics. http://homotopytypetheory.org/book, Institute for Advanced Study, 2013.
- 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.