From signatures to monads in \textsf{UniMath}
DOI10.1007/s10817-018-9474-4zbMath1468.03007arXiv1612.00693OpenAlexW3102794350WikidataQ129537749 ScholiaQ129537749MaRDI QIDQ2319990
Anders Mörtberg, Benedikt Ahrens, Ralph Matthes
Publication date: 21 August 2019
Published in: Journal of Automated Reasoning (Search for Journal in Brave)
Full work available at URL: https://arxiv.org/abs/1612.00693
Mechanization of proofs and logical operations (03B35) Abstract and axiomatic homotopy theory in algebraic topology (55U35) Theories (e.g., algebraic theories), structure, and semantics (18C10) Monads (= standard construction, triple or triad), algebras for monads, homology and derived functors for monads (18C15) Formalization of mathematics in connection with theorem provers (68V20) Type theory (03B38)
Related Items
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Substitution in non-wellfounded syntax with variable binding
- Modules over monads and initial semantics
- Generalized algebraic theories and contextual categories
- Substitution: A formal methods case study using monads and transformations
- Generalised folds for nested datatypes
- The simplicial model of univalent foundations (after Voevodsky)
- Inductive types and type constraints in the second-order lambda calculus
- C-system of a module over a \(Jf\)-relative monad
- Inductive Types in Homotopy Type Theory
- A C-system defined by a universe category
- Modules over Monads and Linearity
- de Bruijn notation as a nested datatype
- Heterogeneous Substitution Systems Revisited
- Cubical Type Theory: a constructive interpretation of the univalence axiom
- Initial Semantics for higher-order typed syntax in Coq
- Non-wellfounded trees in Homotopy Type Theory
- Homotopy Type Theory: Univalent Foundations of Mathematics
- Univalent categories and the Rezk completion
- An experimental library of formalized Mathematics based on the univalent foundations
