The following pages link to UniMath (Q27033):
Displaying 26 items.
- Homotopy type theory in Lean (Q1687770) (← links)
- Meaning explanations at higher dimension (Q1688954) (← links)
- Construction of the circle in \textit{UniMath} (Q2031555) (← links)
- A meaning explanation for HoTT (Q2054122) (← links)
- A certified program for the Karatsuba method to multiply polynomials (Q2132545) (← links)
- The construction of set-truncated higher inductive types (Q2133178) (← links)
- Homotopical inverse diagrams in categories with attributes (Q2207273) (← links)
- Mac Lane's comparison theorem for the Kleisli construction formalized in Coq (Q2209259) (← links)
- Type theory and formalisation of mathematics (Q2399357) (← links)
- Internal languages of finitely complete \((\infty , 1)\)-categories (Q2414596) (← links)
- C-system of a module over a \(Jf\)-relative monad (Q2689172) (← links)
- Some Wellfounded Trees in UniMath (Q2819193) (← links)
- The (Pi,lambda)-structures on the C-systems defined by universe categories (Q2963471) (← links)
- Displayed Categories (Q3121521) (← links)
- Heterogeneous Substitution Systems Revisited (Q4580223) (← links)
- Categorical structures for type theory in univalent foundations (Q4683858) (← links)
- An introduction to univalent foundations for mathematicians (Q4684362) (← links)
- Lawvere theories and C-systems (Q4959711) (← links)
- (Q5009703) (← links)
- The Interpretation Lifting Theorem for C-Systems (Q5025082) (← links)
- (Q5031679) (← links)
- Bicategories in univalent foundations (Q5055496) (← links)
- The Scott model of PCF in univalent type theory (Q5055497) (← links)
- High-level signatures and initial semantics (Q5079724) (← links)
- Displayed Categories (Q5111300) (← links)
- A trustful monad for axiomatic reasoning with probability and nondeterminism (Q5152658) (← links)
