Initial Algebras Unchained -- A Novel Initial Algebra Construction Formalized in Agda

TL;DR

This paper introduces a new, non-ordinal-based initial algebra construction for endofunctors, formalized in Agda, which forms the colimit of finite recursive coalgebras and is applicable under accessible functors.

Contribution

A novel initial algebra construction that avoids transfinite steps, inspired by Pataraia's fixed point theorem, and formalized in Agda for constructive correctness.

Findings

Constructive proofs fully formalized in Agda.

Applicable to accessible endofunctors in locally presentable categories.

Provides an alternative to Adámek's classical construction.

Abstract

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.