Initial Algebra - Final Coalgebra

Dually, a final coalgebra is a terminal object in the category of F-coalgebras. The finality provides a general framework for coinduction and corecursion.

For example, using the same functor 1+(-) as before, a coalgebra is a set X together with a truth-valued test function p : X → 2 and a partial function f : X → X whose domain is formed by those x ∈ X for which p(x) = 0. The set N ∪ {ω} consisting of the natural numbers extended with a new element ω is the carrier of the final coalgebra in the category, where p is the test for zero: p(0) = 1, p(n+1) = p(ω) = 0; and f is the predecessor function (the inverse of the successor function) on the positive naturals, but acts like the identity on the new element ω: f(n+1) = n, f(ω) = ω.

For a second example, consider the same functor 1+N×(-) as before. In this case the carrier of the final coalgebra consists of all lists of natural numbers, finite as well as infinite. The operations are a test function testing whether a list is empty, and a deconstruction function defined on nonempty lists returning a pair consisting of the head and the tail of the input list.