2026-07-23T08:49:34Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:5152 2024-03-06T10:36:09Z ddc:004 open_access

Non-Wellfounded Trees in Homotopy Type Theory Ahrens, Benedikt Capriotti, Paolo Spadotti, Régis Homotopy Type Theory coinductive types computer theorem proving Agda 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Benedikt Ahrens and Paolo Capriotti and Régis Spadotti 2015 Is Part Of LIPIcs, Volume 38, 13th International Conference on Typed Lambda Calculi and Applications (TLCA 2015) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.TLCA.2015.17 urn:nbn:de:0030-drops-51522 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TLCA.2015.17 eng https://creativecommons.org/licenses/by/3.0/legalcode