Constructing initial algebras using inflationary iteration

zbMATH Open1530.18006arXiv2105.03252MaRDI QIDQ6153329FDOQ6153329

Authors: Andrew M. Pitts, S. C. Steenkamp 

Publication date: 13 February 2024

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

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

Mathematics Subject Classification ID

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

Cites Work

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

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)