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

zbMATH Keywords

inductive typesinitial algebra semanticsrepresentation of substitutionunivalent mathematics

Mathematics Subject Classification ID

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 (4)

C-system of a module over a \(Jf\)-relative monad ⋮ For Finitary Induction-Induction, Induction is Enough ⋮ UniMath ⋮ Heterogeneous Substitution Systems Revisited

Uses Software

• Coq
• cubicaltt

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

This page was built for publication: From signatures to monads in \textsf{UniMath}