Cofree

Cofree is a dual notion in category theory used to describe a universal coalgebra construction. Given an endofunctor F: C → C, a cofree F-coalgebra on an object A in C consists of a coalgebra (C, γ: C → F(C)) together with a morphism ε: C → A such that for every coalgebra (D, δ: D → F(D)) and every morphism f: D → A, there exists a unique coalgebra morphism h: D → C with ε ∘ h = f. Here, a coalgebra morphism h satisfies γ ∘ h = F(h) ∘ δ. In other words, (C, γ, ε) is universal among coalgebras mapping to A, playing the dual role to a free object.

In practical terms, cofree coalgebras provide a canonical way to “coinductively” generate and reason about behaviors parameterized by A. They are central in coalgebra theory and in the semantics of corecursive definitions, where unfolding or observing-structure is modeled by coalgebraic maps.

A standard example appears in Set with F(X) = A × X. The cofree F-coalgebra on A is the stream coalgebra on A, whose carrier is the set A^N of infinite streams of elements of A. The coalgebra structure γ(s) = (head(s), tail(s)) and the projection ε(s) = head(s) yield the universal property: for any coalgebra (D, δ) and map f: D → A, there is a unique coalgebra morphism h: D → A^N with head(h(d)) = f(d) and tail(h(d)) = h(δ(d)).

Cofree constructions thus contrast with free constructions by dualizing initiality to terminality in the appropriate comma category. Their existence depends on the category and the functor; they are well-behaved for many common endofunctors in Set, but not guaranteed in general.