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

Thorsten Wißmann, Stefan Milius

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…