# 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 $\mathbb{N}$-algebra is a type $C$ with two elements $c_{0}:C$, $c_{s}:C\to C$. The type of such algebras is

 $\mathbb{N}\mathsf{Alg}:\!\!\equiv\mathchoice{\sum_{C:\mathcal{U}}\,}{% \mathchoice{{\textstyle\sum_{(C:\mathcal{U})}}}{\sum_{(C:\mathcal{U})}}{\sum_{% (C:\mathcal{U})}}{\sum_{(C:\mathcal{U})}}}{\mathchoice{{\textstyle\sum_{(C:% \mathcal{U})}}}{\sum_{(C:\mathcal{U})}}{\sum_{(C:\mathcal{U})}}{\sum_{(C:% \mathcal{U})}}}{\mathchoice{{\textstyle\sum_{(C:\mathcal{U})}}}{\sum_{(C:% \mathcal{U})}}{\sum_{(C:\mathcal{U})}}{\sum_{(C:\mathcal{U})}}}C\times(C\to C).$
###### Definition 5.4.2.

A $\mathbb{N}$ between $\mathbb{N}$-algebras $(C,c_{0},c_{s})$ and $(D,d_{0},d_{s})$ is a function $h:C\to D$ such that $h(c_{0})=d_{0}$ and $h(c_{s}(c))=d_{s}(h(c))$ for all $c:C$. The type of such homomorphisms is

 $\mathbb{N}\mathsf{Hom}((C,c_{0},c_{s}),(D,d_{0},d_{s})):\!\!\equiv\sum_{(h:C% \to D)}\,(h(c_{0})=d_{0})\times\mathchoice{{\textstyle\prod_{(c:C)}}}{\prod_{(% c:C)}}{\prod_{(c:C)}}{\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 $\infty$-groupoids, we actually have an $(\infty,1)$-category of $\mathbb{N}$-algebras, and we should ask $\mathbb{N}$ to be initial in the appropriate $(\infty,1)$-categorical sense. Fortunately, we can formulate this without needing to define $(\infty,1)$-categories.

###### Definition 5.4.3.

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

 $\mathsf{isHinit}_{\mathbb{N}}(I):\!\!\equiv\mathchoice{\prod_{C:\mathbb{N}% \mathsf{Alg}}\,}{\mathchoice{{\textstyle\prod_{(C:\mathbb{N}\mathsf{Alg})}}}{% \prod_{(C:\mathbb{N}\mathsf{Alg})}}{\prod_{(C:\mathbb{N}\mathsf{Alg})}}{\prod_% {(C:\mathbb{N}\mathsf{Alg})}}}{\mathchoice{{\textstyle\prod_{(C:\mathbb{N}% \mathsf{Alg})}}}{\prod_{(C:\mathbb{N}\mathsf{Alg})}}{\prod_{(C:\mathbb{N}% \mathsf{Alg})}}{\prod_{(C:\mathbb{N}\mathsf{Alg})}}}{\mathchoice{{\textstyle% \prod_{(C:\mathbb{N}\mathsf{Alg})}}}{\prod_{(C:\mathbb{N}\mathsf{Alg})}}{\prod% _{(C:\mathbb{N}\mathsf{Alg})}}{\prod_{(C:\mathbb{N}\mathsf{Alg})}}}\mathsf{% isContr}(\mathbb{N}\mathsf{Hom}(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 $\mathbb{N}$-algebras are equal. Thus, the type of h-initial $\mathbb{N}$-algebras is a mere proposition.

###### Proof.

Suppose $I$ and $J$ are h-initial $\mathbb{N}$-algebras. Then $\mathbb{N}\mathsf{Hom}(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 $\mathsf{id}_{I}$; but $\mathbb{N}\mathsf{Hom}(I,I)$ is contractible, so $g\circ f=\mathsf{id}_{I}$. Similarly, $f\circ g=\mathsf{id}_{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 $\mathbb{N}$-algebra $(\mathbb{N},\mathbf{0},\mathsf{succ})$ 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

 $\displaystyle f(0)$ $\displaystyle:\!\!\equiv c_{0}$ $\displaystyle f(\mathsf{succ}(n))$ $\displaystyle:\!\!\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}\mathsf{Hom}(\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+\mathbf{1}\to C$, and a function $f:C\to D$ is a $\mathbb{N}$-homomorphism just when $f\circ c\sim d\circ(f+\mathbf{1})$. 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 $\mathsf{W}$-type associated to $A:\mathcal{U}$ and $B:A\to\mathcal{U}$. In this case we have an associated polynomial functor:

 $P(X)=\mathchoice{\sum_{x:A}\,}{\mathchoice{{\textstyle\sum_{(x:A)}}}{\sum_{(x:% A)}}{\sum_{(x:A)}}{\sum_{(x:A)}}}{\mathchoice{{\textstyle\sum_{(x:A)}}}{\sum_{% (x:A)}}{\sum_{(x:A)}}{\sum_{(x:A)}}}{\mathchoice{{\textstyle\sum_{(x:A)}}}{% \sum_{(x:A)}}{\sum_{(x:A)}}{\sum_{(x:A)}}}(B(x)\rightarrow 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\rightarrow C$. By the universal property of $\Sigma$-types, this is equivalent to giving a function $\mathchoice{\prod_{a:A}\,}{\mathchoice{{\textstyle\prod_{(a:A)}}}{\prod_{(a:A)% }}{\prod_{(a:A)}}{\prod_{(a:A)}}}{\mathchoice{{\textstyle\prod_{(a:A)}}}{\prod% _{(a:A)}}{\prod_{(a:A)}}{\prod_{(a:A)}}}{\mathchoice{{\textstyle\prod_{(a:A)}}% }{\prod_{(a:A)}}{\prod_{(a:A)}}{\prod_{(a:A)}}}(B(a)\to C)\to C$. We will also call such objects $\mathsf{W}$-algebras for $A$ and $B$, and we write

 $\mathsf{W}\mathsf{Alg}(A,B):\!\!\equiv\mathchoice{\sum_{(C:\mathcal{U})}\,}{% \mathchoice{{\textstyle\sum_{(C:\mathcal{U})}}}{\sum_{(C:\mathcal{U})}}{\sum_{% (C:\mathcal{U})}}{\sum_{(C:\mathcal{U})}}}{\mathchoice{{\textstyle\sum_{(C:% \mathcal{U})}}}{\sum_{(C:\mathcal{U})}}{\sum_{(C:\mathcal{U})}}{\sum_{(C:% \mathcal{U})}}}{\mathchoice{{\textstyle\sum_{(C:\mathcal{U})}}}{\sum_{(C:% \mathcal{U})}}{\sum_{(C:\mathcal{U})}}{\sum_{(C:\mathcal{U})}}}\mathchoice{% \prod_{(a:A)}\,}{\mathchoice{{\textstyle\prod_{(a:A)}}}{\prod_{(a:A)}}{\prod_{% (a:A)}}{\prod_{(a:A)}}}{\mathchoice{{\textstyle\prod_{(a:A)}}}{\prod_{(a:A)}}{% \prod_{(a:A)}}{\prod_{(a:A)}}}{\mathchoice{{\textstyle\prod_{(a:A)}}}{\prod_{(% a:A)}}{\prod_{(a:A)}}{\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})\rightarrow(D,s_{D})$ consists of a function $f:C\rightarrow D$ and a homotopy between maps $PC\rightarrow D$

 $s_{f}:f\circ s_{C}\,=s_{D}\circ Pf,$

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

In terms of elements, $f$ is a $P$-homomorphism (or $\mathsf{W}$-homomorphism) if

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

We have the type of $\mathsf{W}$-homomorphisms:

 $\mathsf{W}\mathsf{Hom}_{A,B}((C,c),(D,d)):\!\!\equiv\mathchoice{\sum_{(h:C\to D% )}\,}{\mathchoice{{\textstyle\sum_{(h:C\to D)}}}{\sum_{(h:C\to D)}}{\sum_{(h:C% \to D)}}{\sum_{(h:C\to D)}}}{\mathchoice{{\textstyle\sum_{(h:C\to D)}}}{\sum_{% (h:C\to D)}}{\sum_{(h:C\to D)}}{\sum_{(h:C\to D)}}}{\mathchoice{{\textstyle% \sum_{(h:C\to D)}}}{\sum_{(h:C\to D)}}{\sum_{(h:C\to D)}}{\sum_{(h:C\to D)}}}% \mathchoice{\prod_{(a:A)}\,}{\mathchoice{{\textstyle\prod_{(a:A)}}}{\prod_{(a:% A)}}{\prod_{(a:A)}}{\prod_{(a:A)}}}{\mathchoice{{\textstyle\prod_{(a:A)}}}{% \prod_{(a:A)}}{\prod_{(a:A)}}{\prod_{(a:A)}}}{\mathchoice{{\textstyle\prod_{(a% :A)}}}{\prod_{(a:A)}}{\prod_{(a:A)}}{\prod_{(a:A)}}}\mathchoice{\prod_{(f:B(a)% \to C)}\,}{\mathchoice{{\textstyle\prod_{(f:B(a)\to C)}}}{\prod_{(f:B(a)\to C)% }}{\prod_{(f:B(a)\to C)}}{\prod_{(f:B(a)\to C)}}}{\mathchoice{{\textstyle\prod% _{(f:B(a)\to C)}}}{\prod_{(f:B(a)\to C)}}{\prod_{(f:B(a)\to C)}}{\prod_{(f:B(a% )\to C)}}}{\mathchoice{{\textstyle\prod_{(f:B(a)\to C)}}}{\prod_{(f:B(a)\to C)% }}{\prod_{(f:B(a)\to C)}}{\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})\rightarrow(D,s_{D})$ is contractible. That is,

 $\mathsf{isHinit}_{\mathsf{W}}(A,B,I):\!\!\equiv\mathchoice{\prod_{C:\mathsf{W}% \mathsf{Alg}(A,B)}\,}{\mathchoice{{\textstyle\prod_{(C:\mathsf{W}\mathsf{Alg}(% A,B))}}}{\prod_{(C:\mathsf{W}\mathsf{Alg}(A,B))}}{\prod_{(C:\mathsf{W}\mathsf{% Alg}(A,B))}}{\prod_{(C:\mathsf{W}\mathsf{Alg}(A,B))}}}{\mathchoice{{\textstyle% \prod_{(C:\mathsf{W}\mathsf{Alg}(A,B))}}}{\prod_{(C:\mathsf{W}\mathsf{Alg}(A,B% ))}}{\prod_{(C:\mathsf{W}\mathsf{Alg}(A,B))}}{\prod_{(C:\mathsf{W}\mathsf{Alg}% (A,B))}}}{\mathchoice{{\textstyle\prod_{(C:\mathsf{W}\mathsf{Alg}(A,B))}}}{% \prod_{(C:\mathsf{W}\mathsf{Alg}(A,B))}}{\prod_{(C:\mathsf{W}\mathsf{Alg}(A,B)% )}}{\prod_{(C:\mathsf{W}\mathsf{Alg}(A,B))}}}\mathsf{isContr}(\mathsf{W}% \mathsf{Hom}_{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:\mathcal{U}$ and type family $B:A\to\mathcal{U}$, the $\mathsf{W}$-algebra $(\mathchoice{\mathchoice{{\textstyle\mathsf{W}_{(x:A)}}}{\mathsf{W}_{(x:A)}}{% \mathsf{W}_{(x:A)}}{\mathsf{W}_{(x:A)}}}{\mathchoice{{\textstyle\mathsf{W}_{(x% :A)}}}{\mathsf{W}_{(x:A)}}{\mathsf{W}_{(x:A)}}{\mathsf{W}_{(x:A)}}}{% \mathchoice{{\textstyle\mathsf{W}_{(x:A)}}}{\mathsf{W}_{(x:A)}}{\mathsf{W}_{(x% :A)}}{\mathsf{W}_{(x:A)}}}{\mathchoice{{\textstyle\mathsf{W}_{(x:A)}}}{\mathsf% {W}_{(x:A)}}{\mathsf{W}_{(x:A)}}{\mathsf{W}_{(x:A)}}}B(x),{\mathsf{sup}})$ 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\mathchoice{\sum_{x:A}\,}{\mathchoice{{\textstyle\sum_{(x:A)}}}% {\sum_{(x:A)}}{\sum_{(x:A)}}{\sum_{(x:A)}}}{\mathchoice{{\textstyle\sum_{(x:A)% }}}{\sum_{(x:A)}}{\sum_{(x:A)}}{\sum_{(x:A)}}}{\mathchoice{{\textstyle\sum_{(x% :A)}}}{\sum_{(x:A)}}{\sum_{(x:A)}}{\sum_{(x:A)}}}(B(x)\to X)$. Let $W:\!\!\equiv\mathchoice{\mathchoice{{\textstyle\mathsf{W}_{(x:A)}}}{\mathsf{W}% _{(x:A)}}{\mathsf{W}_{(x:A)}}{\mathsf{W}_{(x:A)}}}{\mathchoice{{\textstyle% \mathsf{W}_{(x:A)}}}{\mathsf{W}_{(x:A)}}{\mathsf{W}_{(x:A)}}{\mathsf{W}_{(x:A)% }}}{\mathchoice{{\textstyle\mathsf{W}_{(x:A)}}}{\mathsf{W}_{(x:A)}}{\mathsf{W}% _{(x:A)}}{\mathsf{W}_{(x:A)}}}{\mathchoice{{\textstyle\mathsf{W}_{(x:A)}}}{% \mathsf{W}_{(x:A)}}{\mathsf{W}_{(x:A)}}{\mathsf{W}_{(x:A)}}}B(x)$. Then using the $\mathsf{W}$-introduction rule from §5.3 (http://planetmath.org/53wtypes), we have a structure map $s_{W}:\!\!\equiv{\mathsf{sup}}:PW\rightarrow 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\mathsf{W}\mathsf{Hom}_{A,B}((W,s_{W}),(C,s_{C}))$ of $\mathsf{W}$-homomorphisms from $(W,s_{W})$ to $(C,s_{C})$ is contractible. To do so, observe that the $\mathsf{W}$-elimination rule and the $\mathsf{W}$-computation rule allow us to define a $\mathsf{W}$-homomorphism $(f,s_{f}):(W,s_{W})\rightarrow(C,s_{C})$, thus showing that $T$ is inhabited. It is furthermore necessary to show that for every $\mathsf{W}$-homomorphism $(g,s_{g}):(W,s_{W})\rightarrow(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 $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 $\mathsf{W}$-elimination so as to guarantee the existence of the required identity proof $s_{e}$. ∎

 Title 5.4 Inductive types are initial algebras \metatable