This directory contains some results about inductive and coinductive types. Since UniMath doesn’t support general definitions with Coq’s (co)inductive types, these types are instead studied in the form of W-types (resp. M-types), which are characterized as initial (resp. final) algebras (resp. coalgebras) for polynomial functors.
The proofs of uniqueness for M- and W-types are based on results in “Non-wellfounded trees in homotopy type theory” and the corresponding Agda formalization by Benedikt Ahrens, Paolo Capriotti, and Régis Spadotti.
Package written by Langston Barrett (@siddharthist).