Non-wellfounded trees in Homotopy Type Theory

TL;DR

This paper proves that coinductive types, specifically indexed M-types, can be constructed within a subsystem of Homotopy Type Theory that includes inductive types, natural numbers, and the Univalence Axiom, with formal verification in Agda.

Contribution

It demonstrates that coinductive types are derivable from inductive types in a specific Homotopy Type Theory subsystem, confirming a conjecture.

Findings

Constructed coinductive types in a subsystem of HoTT.

Mechanized proofs in Agda confirm the results.

Validated the conjecture about the constructibility of coinductive types.

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.