This coq library aims to formalize a substantial body of mathematics using the univalent point of view.
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.
The definition of fibered algebras is based on “Homotopy-initial algebras in type theory” and the corresponding Coq formalization by Steve Awodey, Nicola Gambino, Kristina Sojakova.
Package written by Langston Barrett (@siddharthist).