@inproceedings{6a4a064e49204e6e95cdc4a1739f6bbe,
title = "Non-wellfounded trees in homotopy type theory",
abstract = "We prove a conjecture about the constructibility of coinductive 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{\"o}f type theory with natural numbers and Voevodsky's Univalence Axiom. Our results are mechanized in the computer proof assistant Agda.",
keywords = "Agda, Coinductive types, Computer theorem proving, Homotopy Type Theory",
author = "Benedikt Ahrens and Paolo Capriotti and R{\'e}gis Spadotti",
year = "2015",
month = jul,
day = "1",
doi = "10.4230/LIPIcs.TLCA.2015.17",
language = "English",
isbn = "978-3-939897-87-3",
volume = "38",
series = "Leibniz International Proceedings in Informatics (LIPIcs)",
publisher = "Schloss Dagstuhl",
pages = "17--30",
editor = "Thorsten Altenkirch",
booktitle = "13th International Conference on Typed Lambda Calculi and Applications (TLCA 2015)",
address = "Germany",
note = "13th International Conference on Typed Lambda Calculi and Applications (TLCA 2015) ; Conference date: 01-07-2015 Through 03-07-2015",
}