Universal algebra in UniMath
From MaRDI portal
Cites work
- A machine-checked proof of Birkhoff's variety theorem in Martin-Löf type theory
- An introduction to small scale reflection in Coq
- Applying universal algebra to lambda calculus
- Automata, Languages and Programming
- Basic constructive modality
- Bicategories in univalent foundations
- Categorical and algebraic aspects of the intuitionistic modal logic \(\mathrm{IEL}^{\text{--}}\) and its predicate extensions
- Construction of the circle in \textit{UniMath}
- Curry-Howard-Lambek correspondence for intuitionistic belief
- Displayed categories
- Electronic communication of mathematics and the interaction of computer algebra systems and proof assistants
- From signatures to monads in \textsf{UniMath}
- High-level signatures and initial semantics
- scientific article; zbMATH DE number 4179333 (Why is no real title available?)
- scientific article; zbMATH DE number 3910392 (Why is no real title available?)
- scientific article; zbMATH DE number 3961577 (Why is no real title available?)
- scientific article; zbMATH DE number 1424016 (Why is no real title available?)
- Inductive types in homotopy type theory
- Intuitionistic modal logic: a 15-year retrospective
- Mixing computations and proofs
- Modular specification of monads through higher-order presentations
- Notions of computation and monads
- On the security of public key protocols
- Preface to Intuitionistic modal logic 2017
- The category theoretic understanding of universal algebra: Lawvere theories and monads
- Types for Proofs and Programs
- W-types in homotopy type theory
- W-types in homotopy-type theory – CORRIGENDUM
- What is a model of the lambda calculus?
This page was built for publication: Universal algebra in UniMath
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q7031110)
