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}$ -homomorphism 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:

\includegraphics

HoTT_fig_5.4.1.png

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:

\includegraphics

HoTT_fig_5.4.2.png

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