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 give to it.
Definition 5.4.1.
A -algebra is a type with two elements , . The type of such algebras is
Definition 5.4.2.
A -homomorphism
between -algebras and is a function such that and for all . The type of such homomorphisms is
We thus have a category of -algebras and -homomorphisms, and the claim is that 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 -groupoids, we actually have an -category of -algebras, and we should ask to be initial in the appropriate -categorical sense.
Fortunately, we can formulate this without needing to define -categories.
Definition 5.4.3.
A -algebra is called homotopy-initial,
or h-initial
for short, if for any other -algebra , the type of -homomorphisms from to is contractible. Thus,
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 -algebras are equal. Thus, the type of h-initial -algebras is a mere proposition.
Proof.
Suppose and are h-initial -algebras. Then is contractible, hence inhabited by some -homomorphism , and likewise we have an -homomorphism . Now the composite is a -homomorphism from to , as is ; but is contractible, so . Similarly, . Hence , and so . 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 (or ) is h-initial are necessarily equal, which finishes the proof. ∎
We now have the following theorem.
Theorem 5.4.5.
The -algebra is homotopy initial.
Sketch of proof.
Fix an arbitrary -algebra . The recursion principle of yields a function defined by
These two equalities make an -homomorphism, which we can take as the center of contraction for .
The uniqueness theorem (Theorem 5.1.1 (http://planetmath.org/51introductiontoinductivetypes#Thmprethm1)) then implies that any other -homomorphism is equal to .
∎
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 into a -algebra is the same as to give a function , and a function is a -homomorphism just when .
In categorical language, this means the -algebras are the algebras for the endofunctor of the category of types.
For a more generic case, consider the -type associated to and . In this case we have an associated polynomial functor:
(5.4.6) |
Actually, this assignment is functorial only up to homotopy, but this makes no difference in what follows.
By definition, a -algebra
is then a type equipped a function .
By the universal property of -types, this is equivalent
to giving a function .
We will also call such objects -algebras
for and , and we write
Similarly, for -algebras and , a homomorphism between them consists of a function and a homotopy between maps
where is the result of the easily-definable action of on . Such an algebra homomorphism can be represented suggestively in the form:
HoTT_fig_5.4.1.png
In terms of elements, is a -homomorphism (or -homomorphism) if
We have the type of -homomorphisms:
Finally, a -algebra is said to be homotopy-initial if for every -algebra , the type of all algebra homomorphisms is contractible. That is,
Now the analogous theorem to Theorem 5.4.5 (http://planetmath.org/54inductivetypesareinitialalgebras#Thmprethm2) is:
Theorem 5.4.7.
For any type and type family , the -algebra is h-initial.
Sketch of proof.
Suppose we have and ,
and consider the associated polynomial functor .
Let . Then using
the -introduction rule from §5.3 (http://planetmath.org/53wtypes), we have a structure map .
We want to show that the algebra is
h-initial. So, let us consider another algebra and show that the type
of -homomorphisms from to is contractible. To do
so, observe that the -elimination rule and the -computation
rule allow us to define a -homomorphism ,
thus showing that is inhabited. It is furthermore necessary to show that for every -homomorphism , there is an identity
proof
(5.4.8) |
This uses the fact that, in general, a type of the form is equivalent to the type of what we call algebra -cells, whose canonical elements are pairs of the form , where and is a higher identity proof between the identity proofs represented by the following pasting diagrams:
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
The identity proof is now constructed by function extensionality and -elimination so as to guarantee the existence of the required identity proof . ∎
Title | 5.4 Inductive types are initial algebras |
\metatable |