Induction-recursion and initial algebras.

DOI10.1016/S0168-0072(02)00096-9zbMath1044.03021OpenAlexW2088156780MaRDI QIDQ1412830

Peter Dybjer, Anton Setzer

Publication date: 25 November 2003

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

Full work available at URL: https://doi.org/10.1016/s0168-0072(02)00096-9

zbMATH Keywords

constructive type theoryMartin-Löf type theoryslice categoriesinitial algebrasdependent type theoryinductive definitionMahlo cardinalsinductive-recursive definitions

Mathematics Subject Classification ID

Logic in computer science (03B70) Abstract data types; algebraic specification (68Q65) Large cardinals (03E55) Categorical semantics of formal languages (18C50) Second- and higher-order arithmetic and fragments (03F35) Metamathematics of constructive systems (03F50)

Related Items (15)

Subtyping without reduction ⋮ Interactive programming in Agda – Objects and graphical user interfaces ⋮ Type-theoretic approaches to ordinals ⋮ Intuitionistic fixed point logic ⋮ How to Reason Coinductively Informally ⋮ Containers, monads and induction recursion ⋮ Impredicative encodings of inductive-inductive data in Cedille ⋮ Continuous Functions on Final Coalgebras ⋮ Three extensional models of type theory ⋮ An induction principle for nested datatypes in intensional type theory ⋮ Variations on inductive-recursive definitions ⋮ Predicativity and constructive mathematics ⋮ Unnamed Item ⋮ Coalgebras as Types Determined by Their Elimination Rules ⋮ Indexed induction-recursion

Cites Work

• Type-theoretic interpretation of iterated, strictly positive inductive definitions
• Proof-theoretic analysis of KPM
• Ordinal notations based on a weakly Mahlo cardinal
• Generalized algebraic theories and contextual categories
• Inaccessibility in constructive set theory and type theory
• Collapsing functions based on recursively large ordinals: A well-ordering proof for KPM
• Inductive families
• Extending Martin-Löf type theory by one Mahlo-universe
• Locally cartesian closed categories and type theory
• A general formulation of simultaneous inductive-recursive definitions in type theory
• Internal type theory
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: Induction-recursion and initial algebras.