C-system of a module over a \(Jf\)-relative monad

DOI10.1016/j.jpaa.2022.107283OpenAlexW2253436356MaRDI QIDQ2689172

Vladimir Voevodsky

Publication date: 9 March 2023

Published in: Journal of Pure and Applied Algebra (Search for Journal in Brave)

Full work available at URL: https://arxiv.org/abs/1602.00352

Mathematics Subject Classification ID

Other nonclassical logic (03B60) Monads (= standard construction, triple or triad), algebras for monads, homology and derived functors for monads (18C15) Categories of fibrations, relations to (K)-theory, relations to type theory (18N45)

Related Items (2)

Construction of the circle in \textit{UniMath} ⋮ From signatures to monads in \textsf{UniMath}

Uses Software

• UniMath

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Substitution in non-wellfounded syntax with variable binding
• Notions of computation and monads
• Modules over monads and initial semantics
• Generalized algebraic theories and contextual categories
• A set of postulates for the foundation of logic
• Nested abstract syntax in Coq
• The simplicial model of univalent foundations (after Voevodsky)
• Combinatorial structure of type dependency
• From signatures to monads in \textsf{UniMath}
• Coequalizers and free triples
• Nominal Sets
• Products of families of types and (Pi,lambda)-structures on C-systems
• The (Pi,lambda)-structures on the C-systems defined by universe categories
• Subsystems and regular quotients of C-systems
• A C-system defined by a universe category
• Monads Need Not Be Endofunctors
• Modules over Monads and Linearity
• Heterogeneous Substitution Systems Revisited
• The lambda calculus is algebraic
• Lawvere theories and C-systems
• Monads need not be endofunctors
• Every Standard Construction is Induced by a Pair of Adjoint Functors
• FUNCTORIAL SEMANTICS OF ALGEBRAIC THEORIES
• An experimental library of formalized Mathematics based on the univalent foundations
• Modules over relative monads for syntax and semantics

This page was built for publication: C-system of a module over a \(Jf\)-relative monad