swMATH15140MaRDI QIDQ27033FDOQ27033
Author name not available (Why is that?)
Official website: https://github.com/UniMath/UniMath
Source code repository: https://github.com/UniMath/UniMath
Cited In (39)
- Displayed Categories
- Mac Lane's comparison theorem for the Kleisli construction formalized in Coq
- Monae
- Lawvere theories and C-systems
- Bicategories in univalent foundations
- Displayed categories
- A certified program for the Karatsuba method to multiply polynomials
- Construction of the circle in \textit{UniMath}
- High-level signatures and initial semantics
- The construction of set-truncated higher inductive types
- The Interpretation Lifting Theorem for C-Systems
- Coq/SSReflect
- A trustful monad for axiomatic reasoning with probability and nondeterminism
- HoTT
- Lean
- Some Wellfounded Trees in UniMath
- C-system of a module over a \(Jf\)-relative monad
- The (Pi,lambda)-structures on the C-systems defined by universe categories
- Globular
- cubicaltt
- RedPRL
- Tycon
- Type theory and formalisation of mathematics
- A meaning explanation for HoTT
- Title not available (Why is that?)
- mathlib
- UALib
- DoCon-A
- Categorical structures for type theory in univalent foundations
- finmap
- Homotopy type theory in Lean
- Meaning explanations at higher dimension
- The Scott model of PCF in univalent type theory
- Title not available (Why is that?)
- Heterogeneous substitution systems revisited
- An introduction to univalent foundations for mathematicians
- Cubical Agda
- Internal languages of finitely complete \((\infty , 1)\)-categories
- Homotopical inverse diagrams in categories with attributes
This page was built for software: UniMath
