UniMath
From MaRDI portal
Software:27033
swMATH15140MaRDI QIDQ27033FDOQ27033
Author name not available (Why is that?)
Source code repository: https://github.com/UniMath/UniMath
Cited In (26)
- Displayed Categories
- Mac Lane's comparison theorem for the Kleisli construction formalized in Coq
- Lawvere theories and C-systems
- Bicategories in univalent foundations
- A certified program for the Karatsuba method to multiply polynomials
- Construction of the circle in \textit{UniMath}
- Heterogeneous Substitution Systems Revisited
- High-level signatures and initial semantics
- The construction of set-truncated higher inductive types
- The Interpretation Lifting Theorem for C-Systems
- A trustful monad for axiomatic reasoning with probability and nondeterminism
- Displayed Categories
- 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
- Type theory and formalisation of mathematics
- A meaning explanation for HoTT
- Title not available (Why is that?)
- Categorical structures for type theory in univalent foundations
- 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?)
- An introduction to univalent foundations for mathematicians
- Internal languages of finitely complete \((\infty , 1)\)-categories
- Homotopical inverse diagrams in categories with attributes
This page was built for software: UniMath
