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öf type theory with natural numbers and Voevodsky's Univalence Axiom. Our results are mechanized in the computer proof assistant Agda.
REF encode M-types (types of coinductive trees) in homotopy type theory and prove that for these bisimilarity logically implies equality.
Non-wellfounded trees in Homotopy Type Theory
Proceedings of TLCA 2015, LIPIcs Vol. 38, pp. 17-30
Mathematics Computer Science