UniMath
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
References in zbMATH (referenced in 15 articles , 1 standard article )
Showing results 1 to 15 of 15.
Sorted by year (- Kapulkin, Krzysztof; Lumsdaine, Peter LeFanu: Homotopical inverse diagrams in categories with attributes (2021)
- Ekici, Burak; Kaliszyk, Cezary: Mac Lane’s comparison theorem for the Kleisli construction formalized in Coq (2020)
- Fiore, Marcelo; Voevodsky, Vladimir: Lawvere theories and C-systems (2020)
- Ahrens, Benedikt; Lefanu Lumsdaine, Peter: Displayed categories (2019)
- Ahrens, Benedikt; Matthes, Ralph; Mörtberg, Anders: From signatures to Monads in \textsfUniMath (2019)
- Kapulkin, Krzysztof; Szumiło, Karol: Internal languages of finitely complete ((\infty, 1))-categories (2019)
- Ahrens, Benedikt; Lumsdaine, Peter Lefanu; Voevodsky, Vladimir: Categorical structures for type theory in univalent foundations (2018)
- Ahrens, Benedikt; Matthes, Ralph: Heterogeneous substitution systems revisited (2018)
- Angiuli, Carlo; Harper, Robert: Meaning explanations at higher dimension (2018)
- Grayson, Daniel R.: An introduction to univalent foundations for mathematicians (2018)
- Ahrens, Benedikt; Lumsdaine, Peter LeFanu: Displayed categories (2017)
- Coquand, Thierry: Type theory and formalisation of mathematics (2017)
- van Doorn, Floris; von Raumer, Jakob; Buchholtz, Ulrik: Homotopy type theory in Lean (2017)
- Voevodsky, Vladimir: The ((\Pi,\lambda))-structures on the C-systems defined by universe categories (2017)
- Ahrens, Benedikt; Mörtberg, Anders: Some wellfounded trees in UniMath (extended abstract) (2016)