Constructing Initial Algebras Using Inflationary Iteration
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.