Terminal coalgebras and free iterative theories

AbstractEvery finitary endofunctor H of Set can be represented via a finitary signature Σ and a collection of equations called “basic”. We describe a terminal coalgebra for H as the terminal Σ-coalgebra (of all Σ-trees) modulo the congruence of applying the basic equations potentially infinitely often. As an application we describe a free iterative theory on H (in the sense of Calvin Elgot) as the theory of all rational Σ-trees modulo the analogous congruence. This yields a number of new examples of iterative theories, e.g., the theory of all strongly extensional, rational, finitely branching trees, free on the finite power-set functor, or the theory of all binary, rational unordered trees, free on one commutative binary operation