catamorphism [math-000I]

The theorem actually proves the corresponding $C$ -object $i$ of initial algebra $(F, i, j)$ is a fixed point of $F$ . By reversing $j$ with its inverse, we get a commute diagram below.

In Haskell, we are able to define initial algebra

newtype Fix f = Fix (f (Fix f))

unFix :: Fix f -> f (Fix f)
unFix (Fix x) = x

View $j$ as constructor Fix, $j^{-1}$ as unFix, then we can define m = alg . fmap m . unFix. Since m :: Fix f -> a, we have definition of catamorphism.

cata :: Functor f => (f a -> a) -> Fix f -> a
cata alg = alg . fmap (cata alg) . unFix

An usual example is foldr, a convenient specialization of catamorphism.