An Initial Algebra Theorem Without Iteration

The Initial Algebra Theorem by Trnkov\'a et al. states, under mild but inevitable assumptions, that an endofunctor has an initial algebra provided it has a pre-fixed point. The proof crucially depends on transfinitely iterating the functor and in fact shows that, equivalently, the (transfinite) initial-algebra chain stops. We give a constructive proof of the Initial Algebra Theorem that avoids transfinite iteration of the functor. This is made possible by using Pataraia's theorem to obtain the east fixed point of a monotone function on the partial order formed by all subobjects of a given pre-fixed point. Thanks to properties of recursive coalgebras, this least fixed point yields an initial algebra. Finally, using transfinite iteration we equivalently obtain convergence of the initial-algebra chain as an equivalent condition, overall yielding a streamlined version of the original proof.