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.
A -algebra is a type with two elements , . The type of such algebras 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.
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,
Any two h-initial -algebras are equal. Thus, the type of h-initial -algebras is a mere proposition.
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.
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:
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:
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:
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
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:
|Title||5.4 Inductive types are initial algebras|