Constructing Initial Algebras Using Inflationary Iteration

TL;DR

This paper extends Adámek's classical theorem to constructive logic, using inflationary iteration over a generalized notion of size, enabling the construction of initial algebras in a broader, more constructive setting.

Contribution

It introduces a new constructive version of the initial algebra construction using inflationary iteration and size notions, applicable under weak choice assumptions.

Findings

Applicable to a wide class of endofunctors

Works within constructive logic and topos theory

Provides a new method for initial algebra construction

Abstract

An old theorem of Ad\'amek 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.