5.4 Inductive types are initial algebras


As suggested earlier, inductive types also have a category-theoretic universal propertyMathworldPlanetmath. They are homotopy-initial algebrasPlanetmathPlanetmath: initial objectsMathworldPlanetmath (up to coherent homotopyMathworldPlanetmathPlanetmath) in a categoryMathworldPlanetmath of “algebras” determined by the specified constructors. As a simple example, consider the natural numbersMathworldPlanetmath. The appropriate sort of “algebra” here is a type equipped with the same structureMathworldPlanetmath that the constructors of give to it.

Definition 5.4.1.

A N-algebra is a type C with two elements c0:C, cs:CC. The type of such algebras is

𝖠𝗅𝗀:C:𝒰C×(CC).
Definition 5.4.2.

A N-homomorphismMathworldPlanetmathPlanetmathPlanetmathPlanetmathPlanetmathPlanetmathPlanetmathPlanetmath between N-algebras (C,c0,cs) and (D,d0,ds) is a function h:CD such that h(c0)=d0 and h(cs(c))=ds(h(c)) for all c:C. The type of such homomorphisms is

𝖧𝗈𝗆((C,c0,cs),(D,d0,ds)):(h:CD)(h(c0)=d0)×(c:C)(h(cs(c))=ds(h(c))).

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 -groupoidsPlanetmathPlanetmathPlanetmathPlanetmathPlanetmathPlanetmath, we actually have an (,1)-category of -algebras, and we should ask to be initial in the appropriate (,1)-categorical sense. Fortunately, we can formulate this without needing to define (,1)-categories.

Definition 5.4.3.

A N-algebra I is called homotopy-initial, or h-initial for short, if for any other N-algebra C, the type of N-homomorphisms from I to C is contractibleMathworldPlanetmath. Thus,

𝗂𝗌𝖧𝗂𝗇𝗂𝗍(I):C:𝖠𝗅𝗀𝗂𝗌𝖢𝗈𝗇𝗍𝗋(𝖧𝗈𝗆(I,C)).

When they exist, h-initial algebras are unique — not just up to isomorphismMathworldPlanetmathPlanetmath, as usual in category theoryMathworldPlanetmathPlanetmathPlanetmathPlanetmath, but up to equality, by the univalence axiom.

Theorem 5.4.4.

Any two h-initial N-algebras are equal. Thus, the type of h-initial N-algebras is a mere proposition.

Proof.

Suppose I and J are h-initial -algebras. Then 𝖧𝗈𝗆(I,J) is contractible, hence inhabited by some -homomorphism f:IJ, and likewise we have an -homomorphism g:JI. Now the composite gf is a -homomorphism from I to I, as is 𝗂𝖽I; but 𝖧𝗈𝗆(I,I) is contractible, so gf=𝗂𝖽I. Similarly, fg=𝗂𝖽J. Hence IJ, 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 N-algebra (N,0,succ) is homotopy initial.

Sketch of proof.

Fix an arbitrary -algebra (C,c0,cs). The recursion principle of yields a function f:C defined by

f(0) :c0
f(𝗌𝗎𝖼𝖼(n)) :cs(f(n)).

These two equalities make f an -homomorphism, which we can take as the center of contractionPlanetmathPlanetmath for 𝖧𝗈𝗆(,C). The uniqueness theorem (Theorem 5.1.1 (http://planetmath.org/51introductiontoinductivetypes#Thmprethm1)) then implies that any other -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 -algebra is the same as to give a function c:C+𝟏C, and a function f:CD is a -homomorphism just when fcd(f+𝟏). In categorical languagePlanetmathPlanetmath, this means the -algebras are the algebras for the endofunctor F(X):X+1 of the category of types.

For a more generic case, consider the 𝖶-type associated to A:𝒰 and B:A𝒰. In this case we have an associated polynomial functor:

P(X)=x:A(B(x)X). (5.4.6)

Actually, this assignment is functorial only up to homotopy, but this makes no differencePlanetmathPlanetmath in what follows. By definition, a P-algebra is then a type C equipped a function sC:PCC. By the universal property of Σ-types, this is equivalentMathworldPlanetmathPlanetmathPlanetmathPlanetmath to giving a function (a:A)(B(a)C)C. We will also call such objects 𝖶-algebras for A and B, and we write

𝖶𝖠𝗅𝗀(A,B):(C:𝒰)(a:A)(B(a)C)C.

Similarly, for P-algebras (C,sC) and (D,sD), a homomorphism between them (f,sf):(C,sC)(D,sD) consists of a function f:CD and a homotopy between maps PCD

sf:fsC=sDPf,

where Pf:PCPD is the result of the easily-definable action of P on f:CD. 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 𝖶-homomorphism) if

f(sC(a,h))=sD(a,λb.f(h(b))).

We have the type of 𝖶-homomorphisms:

𝖶𝖧𝗈𝗆A,B((C,c),(D,d)):(h:CD)(a:A)(f:B(a)C)h(c(a,f))=λb.h(f(b))

Finally, a P-algebra (C,sC) is said to be homotopy-initial if for every P-algebra (D,sD), the type of all algebra homomorphisms (C,sC)(D,sD) is contractible. That is,

𝗂𝗌𝖧𝗂𝗇𝗂𝗍𝖶(A,B,I):C:𝖶𝖠𝗅𝗀(A,B)𝗂𝗌𝖢𝗈𝗇𝗍𝗋(𝖶𝖧𝗈𝗆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:U and type family B:AU, the W-algebra (W(x:A)B(x),sup) is h-initial.

Sketch of proof.

Suppose we have A:𝒰 and B:A𝒰, and consider the associated polynomial functor P(X):(x:A)(B(x)X). Let W:𝖶(x:A)B(x). Then using the 𝖶-introduction rule from §5.3 (http://planetmath.org/53wtypes), we have a structure mapPlanetmathPlanetmathPlanetmath sW:𝗌𝗎𝗉:PWW. We want to show that the algebra (W,sW) is h-initial. So, let us consider another algebra (C,sC) and show that the type T:𝖶𝖧𝗈𝗆A,B((W,sW),(C,sC)) of 𝖶-homomorphisms from (W,sW) to (C,sC) is contractible. To do so, observe that the 𝖶-elimination rule and the 𝖶-computation rule allow us to define a 𝖶-homomorphism (f,sf):(W,sW)(C,sC), thus showing that T is inhabited. It is furthermore necessary to show that for every 𝖶-homomorphism (g,sg):(W,sW)(C,sC), there is an identityPlanetmathPlanetmathPlanetmath proof

p:(f,sf)=(g,sg). (5.4.8)

This uses the fact that, in general, a type of the form (f,sf)=(g,sg) is equivalent to the type of what we call algebra 2-cells, whose canonical elements are pairs of the form (e,se), where e:f=g and se 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,se):(f,sf)=(g,sg).

The identity proof e:f=g is now constructed by function extensionality and 𝖶-elimination so as to guarantee the existence of the required identity proof se. ∎

Title 5.4 Inductive types are initial algebras
\metatable