UniMath - a library of mathematics formalized in the univalent style. he univalent style of formalization of mathematics in the type theories such as the ones used in Coq, Agda or Lean is based on the discovery in 2009 of a new class of models of such type theories. These “univalent models” led to the new intuition that resulted in the introduction into the type theory of the concept of h-level. This most important concept implies in particular that to obtain good intuitive behavior one should define propositions as types of h-level 1 and sets as types of h-level 2. Instead of syntactic Prop one then *defines* a type hProp(U) - the type of types of h-level 1 in the universe U and the type hSet(U) - the type of types of h-level 2 in U. With types of h-level 1 and 2 one can efficiently formalize all of the set-theoretic mathematics. With types of h-level 3 one can efficiently formalize mathematics at the level of categories etc. Univalent style allows to directly formalize constructive mathematics and to formalize classical mathematics by adding the excluded middle axiom for types of h-level 1 and the axiom of choice for types of h-level 2. UniMath is a growing library of constructive mathematics formalized in the univalent style using a small subset of Coq language.

Keywords for this software

Anything in here will be replaced on browsers that support the canvas element