Constructing initial algebras using inflationary iteration

MaRDI QIDQ6153329zbMATH OpenFDO

Authors Andrew M. Pitts, S. C. Steenkamp

Publication date 13 February 2024

Full work available at URL https://arxiv.org/abs/2105.03252, https://cgi.cse.unsw.edu.au/~eptcs/paper.cgi?ACT2021.7

Mathematics Subject Classification ID

Other constructive mathematics (03F65) Adjoint functors (universal constructions, reflective subcategories, Kan extensions, etc.) (18A40)

Recommendations

• Initial algebras and terminal coalgebras in many-sorted sets
• Iterative algebras at work
• Fixed points of set functors: how many iterations are needed?
• On terminal coalgebras derived from initial algebras
• Free iterative theories: a coalgebraic view

Cites work

• A general formulation of simultaneous inductive-recursive definitions in type theory
• Axioms for modelling cubical type theory in a topos
• Constructing infinitary quotient-inductive types
• Containers: Constructing strictly positive types
• Homotopy type theory. Univalent foundations of mathematics
• scientific article; zbMATH DE number 3910392 (Why is no real title available?)
• scientific article; zbMATH DE number 50149 (Why is no real title available?)
• scientific article; zbMATH DE number 3458870 (Why is no real title available?)
• scientific article; zbMATH DE number 1289305 (Why is no real title available?)
• scientific article; zbMATH DE number 575948 (Why is no real title available?)
• scientific article; zbMATH DE number 1956528 (Why is no real title available?)
• scientific article; zbMATH DE number 2117177 (Why is no real title available?)
• Internal universes in models of homotopy type theory
• Intuitionistic sets and ordinals
• Large and infinitary quotient inductive-inductive types
• On the Bourbaki-Witt principle in toposes
• On the construction of free algebras for equational systems
• Quotient inductive-inductive types
• The axiom of multiple choice and models for constructive set theory
• The weak choice principle WISC may fail in the category of sets
• Type theories, toposes and constructive set theory: Predicative aspects of AST
• Type-based termination, inflationary fixed-points, and mixed inductive-coinductive types
• Types for Proofs and Programs
• Well-founded recursion with copatterns and sized types
• Wellfounded trees in categories

Cited in

(2)

• Initial algebras unchained -- a novel initial algebra construction formalized in Agda
• Broad infinity and generation principles

This page was built for publication: Constructing initial algebras using inflationary iteration

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