eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2015-06-15
17
30
10.4230/LIPIcs.TLCA.2015.17
article
Non-Wellfounded Trees in Homotopy Type Theory
Ahrens, Benedikt
Capriotti, Paolo
Spadotti, Régis
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.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol038-tlca2015/LIPIcs.TLCA.2015.17/LIPIcs.TLCA.2015.17.pdf
Homotopy Type Theory
coinductive types
computer theorem proving
Agda