This coq library aims to formalize a substantial body of mathematics using the univalent point of view.

View the Project on GitHub UniMath/UniMath

Heterogeneous substitution systems

Formalization of heterogeneous substitution systems as defined in

Matthes & Uustalu, Substitution in Non-wellfounded Syntax with Variable Binding

Report on the formalization and some additional results are given in

Ahrens & Matthes, Heterogeneous substitution systems revisited

Much more on signatures (binding signatures and signatures with strength) and effective constructions of initial algebras and fortiori heterogeneous substitution systems and monads is described in

Ahrens, Matthes & Mörtberg, From signatures to monads in UniMath

Still more recent material by Ahrens, Matthes & Mörtberg concerns multi-sorted systems.

Contents (alphabetic order of files)