Non-wellfounded trees in Homotopy Type Theory
Logic in Computer Science
2019-07-16 v1 Category 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\"of type theory with natural numbers and Voevodsky's Univalence Axiom. Our results are mechanized in the computer proof assistant Agda.
Keywords
Cite
@article{arxiv.1504.02949,
title = {Non-wellfounded trees in Homotopy Type Theory},
author = {Benedikt Ahrens and Paolo Capriotti and Régis Spadotti},
journal= {arXiv preprint arXiv:1504.02949},
year = {2019}
}
Comments
14 pages, to be published in proceedings of TLCA 2015; ancillary files contain Agda files with formalized proofs