A categorical semantics for inductive-inductive definitions

DOI10.1007/978-3-642-22944-2_6MaRDI QIDQ3090862zbMATH OpenOpenAlexWikidataFDO

Authors Thorsten Altenkirch, Peter A. Morris, Fredrik Nordvall Forsberg, Anton Setzer

Publication date 2 September 2011

Published in Algebra and Coalgebra in Computer Science (Search for Journal in Brave)

Full work available at URL https://cronfa.swan.ac.uk/Record/cronfa7505/Download/0007505-18052015005827.pdf

Mathematics Subject Classification ID

Theories (e.g., algebraic theories), structure, and semantics (18C10) Abstract data types; algebraic specification (68Q65)

Recommendations

• A finite axiomatisation of inductive-inductive definitions
• Inductive-inductive definitions
• Positive inductive-recursive definitions
• Dependent inductive and coinductive types are fibrational dialgebras
• Semantics of constructions. II: The initial algebraic approach

Cited in

(15)

• From realizability to induction via dependent intersection
• Homotopy-initial algebras in type theory
• Inductive-inductive definitions
• A finite axiomatisation of inductive-inductive definitions
• A syntax for higher inductive-inductive types
• Dependent inductive and coinductive types are fibrational dialgebras
• Bicategories in univalent foundations
• Modal meet-implication logic
• Modules over monads and operational semantics (expanded version)
• Indexed containers
• On the category of \(L\)-fuzzy automata, coalgebras and dialgebras
• Impredicative encodings of inductive-inductive data in Cedille
• On L-fuzzy automata, coalgebras and dialgebras: associated categories and L-fuzzy topologies
• Modules over monads and operational semantics
• On categories associated with L-valued fuzzy approximation spaces

This page was built for publication: A categorical semantics for inductive-inductive definitions

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3090862)