UniMath

swMATH15140MaRDI QIDQ27033

No author found.

Source code repository: https://github.com/UniMath/UniMath

Described by source

• From signatures to monads in \textsf{UniMath}

Related Items (26)

Categorical structures for type theory in univalent foundations ⋮ A certified program for the Karatsuba method to multiply polynomials ⋮ The construction of set-truncated higher inductive types ⋮ Bicategories in univalent foundations ⋮ The Scott model of PCF in univalent type theory ⋮ Type theory and formalisation of mathematics ⋮ Internal languages of finitely complete \((\infty , 1)\)-categories ⋮ Homotopy type theory in Lean ⋮ Meaning explanations at higher dimension ⋮ The Interpretation Lifting Theorem for C-Systems ⋮ C-system of a module over a \(Jf\)-relative monad ⋮ Unnamed Item ⋮ Homotopical inverse diagrams in categories with attributes ⋮ Mac Lane's comparison theorem for the Kleisli construction formalized in Coq ⋮ Unnamed Item ⋮ Displayed Categories ⋮ A trustful monad for axiomatic reasoning with probability and nondeterminism ⋮ Displayed Categories ⋮ An introduction to univalent foundations for mathematicians ⋮ Construction of the circle in \textit{UniMath} ⋮ Lawvere theories and C-systems ⋮ High-level signatures and initial semantics ⋮ A meaning explanation for HoTT ⋮ Some Wellfounded Trees in UniMath ⋮ Heterogeneous Substitution Systems Revisited ⋮ The (Pi,lambda)-structures on the C-systems defined by universe categories

This page was built for software: UniMath