Cited in
(39)- Mac Lane's comparison theorem for the Kleisli construction formalized in Coq
- Displayed Categories
- 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
- Coq/SSReflect
- HoTT
- Lean
- Globular
- cubicaltt
- RedPRL
- Tycon
- mathlib
- UALib
- DoCon-A
- The construction of set-truncated higher inductive types
- The Interpretation Lifting Theorem for C-Systems
- Some Wellfounded Trees in UniMath
- C-system of a module over a \(Jf\)-relative monad
- A trustful monad for axiomatic reasoning with probability and nondeterminism
- The (Pi,lambda)-structures on the C-systems defined by universe categories
- Type theory and formalisation of mathematics
- A meaning explanation for HoTT
- scientific article; zbMATH DE number 7474655 (Why is no real title available?)
- Monae
- Categorical structures for type theory in univalent foundations
- Homotopy type theory in Lean
- Meaning explanations at higher dimension
- finmap
- Cubical Agda
- The Scott model of PCF in univalent type theory
- scientific article; zbMATH DE number 7379288 (Why is no real title available?)
- Heterogeneous substitution systems revisited
- 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
