based on plain type theory/set theory:
based on dependent type theory/homotopy type theory:
based on cubical type theory:
1lab (cross-linked reference resource)
based on modal type theory:
based on simplicial type theory:
For monoidal category theory:
projects for formalization of mathematics with proof assistants:
Archive of Formal Proofs (using Isabelle)
ForMath project (using Coq)
UniMath project (using Coq and Agda)
Xena project (using Lean)
Other proof assistants
Historical projects that died out:
Last revised on September 18, 2023 at 15:17:54. See the history of this page for a list of all contributions to it.