Corecursive algebras are algebras that admit unique solutions of recursive equation systems. We study these and a generalization: completely iterative algebras. The terminal coalgebra turns out to be the initial corecursive algebra as well as the initial completely iterative algebra. Dually, the initial algebra is the initial (parametrically) recursive coalgebra. These results explain the title of the chapter. We apply recursive coalgebras in order to obtain a new proof of the Initial Algebra Theorem from Chapter 6.

Well-founded coalgebras generalize well-foundedness for graphs, and they capture the induction principle for well-founded orders on an abstract level. Taylor’s General Recursion Theorem shows that, under hypotheses, every well-founded coalgebra is parametrically recursive. We give a new proof of this result, and we show that it holds for all set functors, and for all endofunctors preserving monomorphisms on a complete and well-powered category with smooth monomorphisms. The converse of the theorem holds for set functors preserving inverse images. We provide an iterative construction of the well-founded part of a given coalgebra: It is carried by the least fixed point of Jacobs’ next-time operator.

This chapter presents a number of sufficient conditions to guarantee that an endofunctor has an initial algebra or a terminal coalgebra. We generalize Kawahara and Mori’s notion of a bounded set functor and prove that for a cocomplete and co-well-powered category with a terminal object, every endofunctor bounded by a generating set has a terminal coalgebra. We use this to show that every accessible endofunctor on a locally presentable category has an initial algebra and a terminal coalgebra. We introduce pre-accessible functors and prove that on a cocomplete and co-well-powered category, the initial-algebra chain of a pre-accessible functor converges, and so the initial algebra exists. If the base category is locally presentable and the functor preserves monomorphisms, then the terminal coalgebra exists.

This chapter presents initial algebras and terminal coalgebras obtained by the most common method. For the initial algebra, this is by iteration starting from the initial object through the natural numbers. For the terminal coalgebra, this is the dual: the iteration begins with the terminal object. The chapter is mainly concerned with examples drawn from sets, posets, complete partial orders, and metric spaces.

This chapter highlights connections of the book’s topics to structures used in all areas of mathematics. Cantor famously proved that no set can be mapped onto its power set. We present some analogous results for metric spaces and posets. On the category of topological spaces, we consider endofunctors built from the Vietoris endofunctor using products, coproducts, composition, and constant functors restricted for Hausdorff spaces. Every such functor has an initial algebra and a terminal coalgebra. Similar results hold for the Hausdorff functor on (complete) metric spaces. Extending a result of Freyd, we exhibit structures on the unit interval [0, 1] making it a terminal coalgebra of an endofunctor on bipointed metric spaces. The positive irrationals and other subsets of the real line are described as terminal coalgebras or corecursive algebras for some set functors, calling on results from the theory of continued fractions.

The theme of this chapter is the relation between the initial algebra for a set functor and the terminal coalgebra, assuming that both exist and that the endofunctor is non-trivial. We introduced a notion called pre-continuity. Pre-continuous set functors generalize finitary and continuous set functors. For such functors, the initial algebra and the terminal coalgebra have the same Cauchy completion and the same ideal completion: the $\omega$-iteration of the terminal-coalgebra chain. It follows that for a non-trivial continuous set functor, the terminal coalgebra is the Cauchy completion of the initial algebra.

The rational fixed point of an endofunctor is a fixed point which is in general different from its initial algebra and its terminal coalgebra. It collects precisely the behaviours of all ‘finite’ coalgebras of a given endofunctor. For sets, they are those with finitely many states. Examples of rational fixed points include regular languages, eventually periodic and rational streams, etc. To study the rational fixed point in categories beyond sets, we discuss locally finitely presentable categories, and we do so in some detail. We characterize the rational fixed point as an initial iterative algebra. The chapter goes into details on many examples, such as rational fixed points in nominal sets. It discusses the rational fixed point and several other fixed points as well, and it summarizes much of what is known about them.

This chapter provides examples of the central concepts of the book: initial algebras and terminal coalgebras. These are mainly for polynomial endofunctors on the category of sets, but also for such functors on sorted sets, nominal sets, and presheaves. We discuss connections to induction and recursion and to their duals, coinduction and corecursion, and also to bisimulation. We present Lambek’s Lemma, a result used throughout the book.

This chapter presents simple and reachable coalgebras and constructions of the simple quotient of a coalgebra and the reachable part of a pointed one. It introduces well-pointed coalgebras: those which are both reachable and simple. Well-pointed coalgebras constitute a coalgebraic formulation of minimality of state-based systems. For set functors preserving intersections, we prove that the terminal coalgebra is formed by all well-pointed coalgebras, and the initial algebra by all well-founded, well-pointed coalgebras (both considered up to isomorphism) with canonical structures.

This chapter takes the iterative construction of initial algebras into the transfinite, generalizing work in Chapters 2 and 4. It begins with a brief presentation of ordinals, cardinals, regular cardinals, and Zermelo’s Theorem: Monotone functions on chain-complete posets have least fixed points obtainable by iteration. When a category has colimits of chains, if an endofunctor preserves colimits of chains of some ordinal length, then the initial-algebra chain converges in the same number of steps. We discuss the precise length of that iterative construction. We introduce the concept of smooth monomorphisms, providing a relation between iteration inside a subobject poset and in the ambient category. We prove the Initial Algebra Theorem: Under natural assumptions related to smoothness, the existence of a pre-fixed point of an endofunctor guarantees the existence of an initial algebra.

This chapter discusses terminal coalgebras obtained by methods other than the finitary iteration that we saw in Chapter 3. One way is by taking a quotient of a weakly terminal coalgebra. Another is to use Worrell’s Theorem: the terminal coalgebra of a finitary set functor is obtainable as a limit, using a doubled form of infinite iteration. The chapter also contains a number of presentations of the terminal coalgebra of the finite power-set functor on sets and of the first infinite limit of its terminal-coalgebra chain.

This chapter presents the limit-colimit coincidence in categories enriched either in complete partial orders or in complete metric spaces. This chapter thus works in settings where one has a theory of approximations of objects, either as joins of $\omega$-chains or as limits of Cauchy sequences, and with endofunctors preserving this structure. There are some additional requirements, and we discuss examples. In the settings which do satisfy those requirements, the initial algebra and the terminal coalgebras exist and their structures are inverses, giving what is known as a canonical fixed point (a limit-colimit coincidence). We recover some known results on this topic due to Smyth and Plotkin in the ordered setting and to America and Rutten in the metric setting. We also discuss applications to solving domain equations.

We motivate the book based on categorical formulations of recursion and induction. We also discuss the background that readers should have and preview many of the topics in the book.