Fix an endofunctor $𝐹:\mathrm{𝒞︀}\to \mathrm{𝒞︀}$. A terminal $𝐹$-coalgebra, written $𝜈𝐹$, is a terminal object of the category of coalgebras $\text{Coalg}(𝐹)$ — equivalently, an initial algebra for ${𝐹}^{\text{op}}$.

Unfolding the universal property: a terminal coalgebra is a coalgebra $(𝜈𝐹,\text{out})$ such that every coalgebra $(𝑥,𝛾)$ admits a unique morphism $\text{unfold}𝛾:𝑥\to 𝜈𝐹$ satisfying

Fix an endofunctor $𝐹:\mathrm{𝒞︀}\to \mathrm{𝒞︀}$. An algebra $𝛼:𝐹𝐵\to 𝐵$ is corecursive when for every coalgebra $𝛾:𝑋\to 𝐹𝑋$ there is exactly one hylomorphism from $𝛾$ to $𝛼$. Equivalently, the functor $\text{𝖧𝗒𝗅𝗈}(-,𝛼)$ of the hylomorphism profunctor is constantly a singleton. It is the dual of a recursive coalgebra: an $𝐹$-algebra in $\mathrm{𝒞︀}$ is corecursive exactly when it is recursive as an ${𝐹}^{\text{op}}$-coalgebra in ${\mathrm{𝒞︀}}^{\text{op}}$.

Example. If $(𝜈𝐹,\text{𝗈𝗎𝗍})$ is a terminal coalgebra, then $\text{𝗈𝗎𝗍}$ is invertible and ${\text{𝗈𝗎𝗍}}^{-1}:𝐹(𝜈𝐹)\to 𝜈𝐹$ is a corecursive algebra: a solution of $ℎ=𝛾\star 𝐹ℎ\star {\text{𝗈𝗎𝗍}}^{-1}$ is the same thing as a solution of $ℎ\star \text{𝗈𝗎𝗍}=𝛾\star 𝐹ℎ$, that is, a coalgebra map into the terminal coalgebra, and there is exactly one, $\text{𝗎𝗇𝖿𝗈𝗅𝖽}𝛾$.

Fix an endofunctor $𝐹:\mathrm{𝒞︀}\to \mathrm{𝒞︀}$, a coalgebra $𝛾:𝑋\to 𝐹𝑋$ and an algebra $𝛼:𝐹𝐵\to 𝐵$. A hylomorphism (or coalgebra-to-algebra morphism) from $𝛾$ to $𝛼$ is a morphism $ℎ:𝑋\to 𝐵$ satisfying

Fix an endofunctor $𝐹:\mathrm{𝒞︀}\to \mathrm{𝒞︀}$. Hylomorphisms form a profunctor from coalgebras to algebras,

where $\text{𝖧𝗒𝗅𝗈}((𝑋,𝛾),(𝐵,𝛼))$ is the set of $ℎ:𝑋\to 𝐵$ with $ℎ=𝛾\star 𝐹ℎ\star 𝛼$.

The action is by composition. If $𝑔:(𝑌,𝛿)\to (𝑋,𝛾)$ is a coalgebra morphism ($𝑔\star 𝛾=𝛿\star 𝐹𝑔$) and $𝑘:(𝐵,𝛼)\to (𝐵\prime ,𝛼\prime )$ is an algebra morphism ($𝛼\star 𝑘=𝐹𝑘\star 𝛼\prime$), then $𝑔\star ℎ\star 𝑘$ is again a hylomorphism:

In these terms, a coalgebra $𝛾$ is recursive when $\text{𝖧𝗒𝗅𝗈}(𝛾,-)$ is the terminal functor, and an algebra $𝛼$ is corecursive when $\text{𝖧𝗒𝗅𝗈}(-,𝛼)$ is. For the inverse of an initial algebra the profunctor is representable, $\text{𝖧𝗒𝗅𝗈}({\text{𝗂𝗇}}^{-1},-)\cong \text{𝖠𝗅𝗀}(𝐹)(\text{𝗂𝗇},-)$, and dually $\text{𝖧𝗒𝗅𝗈}(-,{\text{𝗈𝗎𝗍}}^{-1})\cong \text{𝖢𝗈𝖺𝗅𝗀}(𝐹)(-,\text{𝗈𝗎𝗍})$ for a terminal coalgebra.

When every value of $\text{𝖧𝗒𝗅𝗈}$ is a singleton, every divide-and-conquer specification over $𝐹$ has exactly one solution. This is what local contractivity guarantees.

Fix an endofunctor $𝐹:\mathrm{𝒞︀}\to \mathrm{𝒞︀}$. A coalgebra $𝛾:𝑋\to 𝐹𝑋$ is recursive when for every algebra $𝛼:𝐹𝐵\to 𝐵$ there is exactly one hylomorphism $ℎ:𝑋\to 𝐵$ from $𝛾$ to $𝛼$, that is, exactly one solution of

Equivalently, the functor $\text{𝖧𝗒𝗅𝗈}(𝛾,-)$ of the hylomorphism profunctor is constantly a singleton.

Recursiveness is a coalgebraic form of well-foundedness: $𝛾$ decomposes each input into subproblems, and recursiveness says that every divide-and-conquer program built on this decomposition has a unique meaning, without mentioning an order on inputs. [1] use recursive coalgebras on categories of indexed families to obtain algorithms that are correct by the type of the map they compute.

Example. If $(𝜇𝐹,\text{𝗂𝗇})$ is an initial algebra, then $\text{𝗂𝗇}$ is invertible (Lambek’s lemma) and ${\text{𝗂𝗇}}^{-1}:𝜇𝐹\to 𝐹(𝜇𝐹)$ is a recursive coalgebra. Precomposing with the isomorphism $\text{𝗂𝗇}$, the equation $ℎ={\text{𝗂𝗇}}^{-1}\star 𝐹ℎ\star 𝛼$ is equivalent to $\text{𝗂𝗇}\star ℎ=𝐹ℎ\star 𝛼$, which says $ℎ$ is an algebra map out of the initial algebra; there is exactly one, $\text{𝖿𝗈𝗅𝖽}𝛼$.

The dual notion is a corecursive algebra.