This page collects a list of libraries of mathematics formalized in proof assistants using homotopy type theory and univalent foundations, sorted by proof assistant.
Coq is a proof assistant based originally on the intensional Calculus of Inductive Constructions?.
UniMath project. Following the lead of Voevodsky’s Foundations library (see below), UniMath generally uses only the core type constructors, such as Pi-types and Sigma-types.
Coq-HoTT. This library roughly uses the type theory of the HoTT Book, including higher inductive types implemented as “private” inductive types. It also uses more advanced features of Coq such as named record types, tactics, and typeclasses. It includes formalizations of many results in synthetic homotopy theory.
Vladimir Voevodsky‘s Foundations repository (now a part of UniMath)
A repository of files for Inductive types in HoTT, by Steve Awodey, Nicola Gambino, and Kristina Sojakova. (See this blog post.)
Agda is a proof assistant based originally on intensional Martin-Lof Type Theory?. By default it allows general pattern-matching which can prove axiom K making it incompatible with HoTT, but the --without-K flag turns this off.
Agda has a --cubical mode that implements a version of cubical type theory that is similar to that of CCHM. The following libraries use this feature.
RedTT is (was?) an implementation of cartesian cubical type theory, with some basic development in an associated library.
Arend implements a theory that enhances Book HoTT with an interval type similar to that of cubical type theory, but without the extra structure necessary to make univalence computational.
Lean is a proof assistant implementing dependent type theory. Current versions of Lean (3 and now 4) have UIP built-in and are not HoTT-compatible, but the old Lean 2 had a HoTT mode.
Last revised on March 11, 2024 at 19:32:48. See the history of this page for a list of all contributions to it.