Constructing Initial Algebras Using Inflationary Iteration

Abstract

An old theorem of Adámek constructs initial algebras for sufficiently cocontinuous endofunctors via transfinite iteration over ordinals in classical set theory. We prove a new version that works in constructive logic, using "inflationary" iteration over a notion of size that abstracts from limit ordinals just their transitive, directed and well-founded properties. Borrowing from Taylor's constructive treatment of ordinals, we show that sizes exist with upper bounds for any given signature of indexes. From this it follows that there is a rich class of endofunctors to which the new theorem applies, provided one admits a weak form of choice (WISC) due to Streicher, Moerdijk, van den Berg and Palmgren, and which is known to hold in the internal constructive logic of many kinds of topos.

arXiv commentIn Proceedings ACT 2021, arXiv:2211.01102

References in corpus (10)

• Quotient inductive-inductive types
• Type-Based Termination, Inflationary Fixed-Points, and Mixed Inductive-Coinductive Types
• Internal Universes in Models of Homotopy Type Theory
• Quotients, inductive types, and quotient inductive types
• W-Types with Reductions and the Small Object Argument
• On the Bourbaki-Witt Principle in Toposes
• The weak choice principle WISC may fail in the category of sets
• Large and Infinitary Quotient Inductive-Inductive Types
• Constructing Infinitary Quotient-Inductive Types
• Broad Infinity and Generation Principles

Cited by in corpus (1)

• Broad Infinity and Generation Principles