  The initial algebra for an endofunctor F provides a recursion and induction
scheme for data structures whose constructors are described by F. The
initial-algebra construction by Ad\'amek (1974) starts with the initial object
(e.g. the empty set) and successively applies the functor until a fixed point
is reached, an idea inspired by Kleene's fixed point theorem. Depending on the
functor of interest, this may require transfinitely many steps indexed by
ordinal numbers until termination.
  We provide a new initial algebra construction which is not based on an
ordinal-indexed chain. Instead, our construction is loosely inspired by
Pataraia's fixed point theorem and forms the colimit of all finite recursive
coalgebras. This is reminiscent of the construction of the rational fixed point
of an endofunctor that forms the colimit of all finite coalgebras. For our main
correctness theorem, we assume the given endofunctor is accessible on a (weak
form of) locally presentable category. Our proofs are constructive and fully
formalized in Agda.
