# 5.4 Inductive types are initial algebras

As suggested earlier, inductive types also have a category-theoretic universal property^{}.
They are *homotopy-initial algebras ^{}*: initial objects

^{}(up to coherent homotopy

^{}) in a category

^{}of “algebras” determined by the specified constructors. As a simple example, consider the natural numbers

^{}. The appropriate sort of “algebra” here is a type equipped with the same structure

^{}that the constructors of $\mathbb{N}$ give to it.

###### Definition 5.4.1.

A $\mathrm{N}$-algebra is a type $C$ with two elements ${c}_{\mathrm{0}}\mathrm{:}C$, ${c}_{s}\mathrm{:}C\mathrm{\to}C$. The type of such algebras is

$$\mathbb{N}\mathrm{\U0001d5a0\U0001d5c5\U0001d5c0}:\equiv \sum _{C:\mathcal{U}}C\times (C\to C).$$ |

###### Definition 5.4.2.

A $\mathrm{N}$-homomorphism^{}
between $\mathrm{N}$-algebras $\mathrm{(}C\mathrm{,}{c}_{\mathrm{0}}\mathrm{,}{c}_{s}\mathrm{)}$ and $\mathrm{(}D\mathrm{,}{d}_{\mathrm{0}}\mathrm{,}{d}_{s}\mathrm{)}$ is a function $h\mathrm{:}C\mathrm{\to}D$ such that $h\mathit{}\mathrm{(}{c}_{\mathrm{0}}\mathrm{)}\mathrm{=}{d}_{\mathrm{0}}$ and $h\mathit{}\mathrm{(}{c}_{s}\mathit{}\mathrm{(}c\mathrm{)}\mathrm{)}\mathrm{=}{d}_{s}\mathit{}\mathrm{(}h\mathit{}\mathrm{(}c\mathrm{)}\mathrm{)}$ for all $c\mathrm{:}C$. The type of such homomorphisms is

$$\mathbb{N}\mathrm{\U0001d5a7\U0001d5c8\U0001d5c6}((C,{c}_{0},{c}_{s}),(D,{d}_{0},{d}_{s})):\equiv \sum _{(h:C\to D)}(h({c}_{0})={d}_{0})\times {\prod}_{(c:C)}(h({c}_{s}(c))={d}_{s}(h(c))).$$ |

We thus have a category of $\mathbb{N}$-algebras and $\mathbb{N}$-homomorphisms, and the claim is that $\mathbb{N}$ is the initial object of this category.
A category theorist will immediately recognize this as the definition of a *natural numbers object* in a category.

Of course, since our types behave like $\mathrm{\infty}$-groupoids^{}, we actually have an $(\mathrm{\infty},1)$-category of $\mathbb{N}$-algebras, and we should ask $\mathbb{N}$ to be initial in the appropriate $(\mathrm{\infty},1)$-categorical sense.
Fortunately, we can formulate this without needing to define $(\mathrm{\infty},1)$-categories.

###### Definition 5.4.3.

A $\mathrm{N}$-algebra $I$ is called homotopy-initial,
or h-initial
for short, if for any other $\mathrm{N}$-algebra $C$, the type of $\mathrm{N}$-homomorphisms from $I$ to $C$ is contractible^{}. Thus,

$${\mathrm{\U0001d5c2\U0001d5cc\U0001d5a7\U0001d5c2\U0001d5c7\U0001d5c2\U0001d5cd}}_{\mathbb{N}}(I):\equiv \prod _{C:\mathbb{N}\mathrm{\U0001d5a0\U0001d5c5\U0001d5c0}}\mathrm{\U0001d5c2\U0001d5cc\U0001d5a2\U0001d5c8\U0001d5c7\U0001d5cd\U0001d5cb}(\mathbb{N}\mathrm{\U0001d5a7\U0001d5c8\U0001d5c6}(I,C)).$$ |

When they exist, h-initial algebras are unique — not just up to isomorphism^{}, as usual in category theory^{}, but up to equality, by the univalence axiom.

###### Theorem 5.4.4.

Any two h-initial $\mathrm{N}$-algebras are equal. Thus, the type of h-initial $\mathrm{N}$-algebras is a mere proposition.

###### Proof.

Suppose $I$ and $J$ are h-initial $\mathbb{N}$-algebras. Then $\mathbb{N}\mathrm{\U0001d5a7\U0001d5c8\U0001d5c6}(I,J)$ is contractible, hence inhabited by some $\mathbb{N}$-homomorphism $f:I\to J$, and likewise we have an $\mathbb{N}$-homomorphism $g:J\to I$. Now the composite $g\circ f$ is a $\mathbb{N}$-homomorphism from $I$ to $I$, as is ${\mathrm{\U0001d5c2\U0001d5bd}}_{I}$; but $\mathbb{N}\mathrm{\U0001d5a7\U0001d5c8\U0001d5c6}(I,I)$ is contractible, so $g\circ f={\mathrm{\U0001d5c2\U0001d5bd}}_{I}$. Similarly, $f\circ g={\mathrm{\U0001d5c2\U0001d5bd}}_{J}$. Hence $I\simeq J$, and so $I=J$. Since being contractible is a mere proposition and dependent products preserve mere propositions, it follows that being h-initial is itself a mere proposition. Thus any two proofs that $I$ (or $J$) is h-initial are necessarily equal, which finishes the proof. ∎

We now have the following theorem.

###### Theorem 5.4.5.

The $\mathrm{N}$-algebra $\mathrm{(}\mathrm{N}\mathrm{,}\mathrm{0}\mathrm{,}\mathrm{succ}\mathrm{)}$ is homotopy initial.

###### Sketch of proof.

Fix an arbitrary $\mathbb{N}$-algebra $(C,{c}_{0},{c}_{s})$. The recursion principle of $\mathbb{N}$ yields a function $f:\mathbb{N}\to C$ defined by

$f(0)$ | $:\equiv {c}_{0}$ | ||

$f(\mathrm{\U0001d5cc\U0001d5ce\U0001d5bc\U0001d5bc}(n))$ | $:\equiv {c}_{s}(f(n)).$ |

These two equalities make $f$ an $\mathbb{N}$-homomorphism, which we can take as the center of contraction^{} for $\mathbb{N}\mathrm{\U0001d5a7\U0001d5c8\U0001d5c6}(\mathbb{N},C)$.
The uniqueness theorem (Theorem 5.1.1 (http://planetmath.org/51introductiontoinductivetypes#Thmprethm1)) then implies that any other $\mathbb{N}$-homomorphism is equal to $f$.
∎

To place this in a more general context, it is useful to consider the notion of *algebra for an endofunctor*.
Note that to make a type $C$ into a $\mathbb{N}$-algebra is the same as to give a function $c:C+\mathrm{\U0001d7cf}\to C$, and a function $f:C\to D$ is a $\mathbb{N}$-homomorphism just when $f\circ c\sim d\circ (f+\mathrm{\U0001d7cf})$.
In categorical language^{}, this means the $\mathbb{N}$-algebras are the algebras for the endofunctor $F(X):\equiv X+1$ of the category of types.

For a more generic case, consider the $\U0001d5b6$-type associated to $A:\mathcal{U}$ and $B:A\to \mathcal{U}$. In this case we have an associated polynomial functor:

$$P(X)=\sum _{x:A}(B(x)\to X).$$ | (5.4.6) |

Actually, this assignment is functorial only up to homotopy, but this makes no difference^{} in what follows.
By definition, a $P$-algebra
is then a type $C$ equipped a function ${s}_{C}:PC\to C$.
By the universal property of $\mathrm{\Sigma}$-types, this is equivalent^{} to giving a function ${\prod}_{(a:A)}(B(a)\to C)\to C$.
We will also call such objects $\U0001d5b6$-algebras
for $A$ and $B$, and we write

$$\mathrm{\U0001d5b6\U0001d5a0\U0001d5c5\U0001d5c0}(A,B):\equiv \sum _{(C:\mathcal{U})}\prod _{(a:A)}(B(a)\to C)\to C.$$ |

Similarly, for $P$-algebras $(C,{s}_{C})$ and $(D,{s}_{D})$, a homomorphism between them $(f,{s}_{f}):(C,{s}_{C})\to (D,{s}_{D})$ consists of a function $f:C\to D$ and a homotopy between maps $PC\to D$

$${s}_{f}:f\circ {s}_{C}={s}_{D}\circ Pf,$$ |

where $Pf:PC\to PD$ is the result of the easily-definable action of $P$ on $f:C\to D$. Such an algebra homomorphism can be represented suggestively in the form:

In terms of elements, $f$ is a $P$-homomorphism (or $\U0001d5b6$-homomorphism) if

$$f({s}_{C}(a,h))={s}_{D}(a,\lambda b.f(h(b))).$$ |

We have the type of $\U0001d5b6$-homomorphisms:

$${\mathrm{\U0001d5b6\U0001d5a7\U0001d5c8\U0001d5c6}}_{A,B}((C,c),(D,d)):\equiv \sum _{(h:C\to D)}\prod _{(a:A)}\prod _{(f:B(a)\to C)}h(c(a,f))=\lambda b.h(f(b))$$ |

Finally, a $P$-algebra $(C,{s}_{C})$ is said to be homotopy-initial if for every $P$-algebra $(D,{s}_{D})$, the type of all algebra homomorphisms $(C,{s}_{C})\to (D,{s}_{D})$ is contractible. That is,

$${\mathrm{\U0001d5c2\U0001d5cc\U0001d5a7\U0001d5c2\U0001d5c7\U0001d5c2\U0001d5cd}}_{\U0001d5b6}(A,B,I):\equiv \prod _{C:\mathrm{\U0001d5b6\U0001d5a0\U0001d5c5\U0001d5c0}(A,B)}\mathrm{\U0001d5c2\U0001d5cc\U0001d5a2\U0001d5c8\U0001d5c7\U0001d5cd\U0001d5cb}({\mathrm{\U0001d5b6\U0001d5a7\U0001d5c8\U0001d5c6}}_{A,B}(I,C)).$$ |

Now the analogous theorem to Theorem 5.4.5 (http://planetmath.org/54inductivetypesareinitialalgebras#Thmprethm2) is:

###### Theorem 5.4.7.

For any type $A\mathrm{:}\mathrm{U}$ and type family $B\mathrm{:}A\mathrm{\to}\mathrm{U}$, the $\mathrm{W}$-algebra $\mathrm{(}{\mathrm{W}}_{\mathrm{(}x\mathrm{:}A\mathrm{)}}\mathit{}B\mathit{}\mathrm{(}x\mathrm{)}\mathrm{,}\mathrm{sup}\mathrm{)}$ is h-initial.

###### Sketch of proof.

Suppose we have $A:\mathcal{U}$ and $B:A\to \mathcal{U}$,
and consider the associated polynomial functor $P(X):\equiv {\sum}_{(x:A)}(B(x)\to X)$.
Let $W:\equiv {\U0001d5b6}_{(x:A)}B(x)$. Then using
the $\U0001d5b6$-introduction rule from §5.3 (http://planetmath.org/53wtypes), we have a structure map^{} ${s}_{W}:\equiv \mathrm{\U0001d5cc\U0001d5ce\U0001d5c9}:PW\to W$.
We want to show that the algebra $(W,{s}_{W})$ is
h-initial. So, let us consider another algebra $(C,{s}_{C})$ and show that the type $T:\equiv {\mathrm{\U0001d5b6\U0001d5a7\U0001d5c8\U0001d5c6}}_{A,B}((W,{s}_{W}),(C,{s}_{C}))$
of $\U0001d5b6$-homomorphisms from $(W,{s}_{W})$ to $(C,{s}_{C})$ is contractible. To do
so, observe that the $\U0001d5b6$-elimination rule and the $\U0001d5b6$-computation
rule allow us to define a $\U0001d5b6$-homomorphism $(f,{s}_{f}):(W,{s}_{W})\to (C,{s}_{C})$,
thus showing that $T$ is inhabited. It is furthermore necessary to show that for every $\U0001d5b6$-homomorphism $(g,{s}_{g}):(W,{s}_{W})\to (C,{s}_{C})$, there is an identity^{} proof

$$p:(f,{s}_{f})=(g,{s}_{g}).$$ | (5.4.8) |

This uses the fact that, in general, a type of the form $(f,{s}_{f})=(g,{s}_{g})$ is equivalent to the type of what we call algebra $\mathrm{2}$-cells, whose canonical elements are pairs of the form $(e,{s}_{e})$, where $e:f=g$ and ${s}_{e}$ is a higher identity proof between the identity proofs represented by the following pasting diagrams:

In light of this fact, to prove that there exists an element as in (5.4.8), it is sufficient to show that there is an algebra 2-cell

$$(e,{s}_{e}):(f,{s}_{f})=(g,{s}_{g}).$$ |

The identity proof $e:f=g$ is now constructed by function extensionality and $\U0001d5b6$-elimination so as to guarantee the existence of the required identity proof ${s}_{e}$. ∎

Title | 5.4 Inductive types are initial algebras |

\metatable |