# nLab catamorphism

Contents

### Context

#### Algebra

higher algebra

universal algebra

category theory

# Contents

## Idea

In the study of recursion schemes, a catamorphism is the simple case of a fold over an inductive data type. In category theoretic terms, this is simply the unique homomorphism out of an initial algebra.

## Definition

Given an endofunctor $F$ such that the category of $F$-algebras has an initial object $(\mu F, in)$, the catamorphism for an $F$-algebra $(A, \varphi)$ is the unique homomorphism from the initial $F$-algebra $(\mu F, in)$ to $(A, \varphi)$. The unique morphism between the carriers is also denoted $cata \varphi \colon \mu F \rightarrow A$.

From the commuting square of the homomorphism, we have $(cata \varphi) \circ in = \varphi \circ F (cata \varphi)$. By Lambek's theorem, $\mathit{in}$ has an inverse $\mathit{out}$, so the catamorphism can be recursively defined by $cata \varphi = \varphi \circ F (cata \varphi) \circ out$.

## Properties

### Fusion law

###### Lemma

Let $h \colon A \rightarrow B$ be a homomorphism between two $F$-algebras $\varphi \colon F A \rightarrow A$ and $\psi \colon F B \rightarrow B$ so that $h \circ \varphi = \psi \circ F h$. Then $h \circ cata \varphi = cata \psi$.

## As a recursion scheme

If $\mu F$ is an inductive type, then the catamorphism is a fold over the type. Some recursive functions can then be implemented in terms of a catamorphism.

### Example: Natural numbers

Let $F$ be the functor $F X = 1 + X$ so that the naturals $\mathbb{N} = \mu F$ are represented by the fixed point of $F$ (i.e. the carrier of the initial F-algebra). The recursor for the naturals can then be defined by a catamorphism.

$\begin{array}{l l} natrec &: \forall A. A \rightarrow (A \rightarrow A) \rightarrow \mathbb{N} \rightarrow A \\ natrec & A z s = cata \varphi, where \\ & \varphi (inl \ast) = z \\ & \varphi (inr n) = s n \end{array}$