constructive mathematics, realizability, computability
propositions as types, proofs as programs, computational trinitarianism
natural deduction metalanguage, practical foundations
type theory (dependent, intensional, observational type theory, homotopy type theory)
computational trinitarianism =
propositions as types +programs as proofs +relation type theory/category theory
UniMath is a library of formalized mathematics (formal proof) based on the univalent foundations of mathematics (homotopy type theory with the univalence axiom) and currently developed with the Coq proof assistant. It is thus a particular library of formalized homotopy type theory.
Current “coordinating committee” (according to the home page):
Web resources:
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 March 7, 2024 at 14:50:19. See the history of this page for a list of all contributions to it.