5.2 Uniqueness of inductive types

We have defined “the” natural numbers to be a particular type $\mathbb{N}$ with particular inductive generators $0$ and $\mathsf{succ}$ . However, by the general principle of inductive definitions in type theory described in the previous section, there is nothing preventing us from defining another type in an identical way. That is, suppose we let $\mathbb{N}^{\prime}$ be the inductive type generated by the constructors

•

$0^{\prime}:\mathbb{N}^{\prime}$
•

$\mathsf{succ}^{\prime}:\mathbb{N}^{\prime}\to\mathbb{N}^{\prime}$ .

Then $\mathbb{N}^{\prime}$ will have identical-looking induction and recursion principles to $\mathbb{N}$ . When proving a statement $E:\mathbb{N}^{\prime}\to\mathcal{U}$ for all of these “new” natural numbers, it suffices to give the proofs $e_{z}:E(0^{\prime})$ and $e_{s}:\mathchoice{\prod_{(n:\mathbb{N}^{\prime})}\,}{\mathchoice{{\textstyle% \prod_{(n:\mathbb{N}^{\prime})}}}{\prod_{(n:\mathbb{N}^{\prime})}}{\prod_{(n:% \mathbb{N}^{\prime})}}{\prod_{(n:\mathbb{N}^{\prime})}}}{\mathchoice{{% \textstyle\prod_{(n:\mathbb{N}^{\prime})}}}{\prod_{(n:\mathbb{N}^{\prime})}}{% \prod_{(n:\mathbb{N}^{\prime})}}{\prod_{(n:\mathbb{N}^{\prime})}}}{\mathchoice% {{\textstyle\prod_{(n:\mathbb{N}^{\prime})}}}{\prod_{(n:\mathbb{N}^{\prime})}}% {\prod_{(n:\mathbb{N}^{\prime})}}{\prod_{(n:\mathbb{N}^{\prime})}}}\mathchoice% {\prod_{(x:E(n))}\,}{\mathchoice{{\textstyle\prod_{(x:E(n))}}}{\prod_{(x:E(n))% }}{\prod_{(x:E(n))}}{\prod_{(x:E(n))}}}{\mathchoice{{\textstyle\prod_{(x:E(n))% }}}{\prod_{(x:E(n))}}{\prod_{(x:E(n))}}{\prod_{(x:E(n))}}}{\mathchoice{{% \textstyle\prod_{(x:E(n))}}}{\prod_{(x:E(n))}}{\prod_{(x:E(n))}}{\prod_{(x:E(n% ))}}}E(\mathsf{succ}^{\prime}(n)).$ And the function $\mathsf{rec}_{\mathbb{N}^{\prime}}(E,e_{z},e_{s}):\mathchoice{\prod_{n:\mathbb% {N}^{\prime}}\,}{\mathchoice{{\textstyle\prod_{(n:\mathbb{N}^{\prime})}}}{% \prod_{(n:\mathbb{N}^{\prime})}}{\prod_{(n:\mathbb{N}^{\prime})}}{\prod_{(n:% \mathbb{N}^{\prime})}}}{\mathchoice{{\textstyle\prod_{(n:\mathbb{N}^{\prime})}% }}{\prod_{(n:\mathbb{N}^{\prime})}}{\prod_{(n:\mathbb{N}^{\prime})}}{\prod_{(n% :\mathbb{N}^{\prime})}}}{\mathchoice{{\textstyle\prod_{(n:\mathbb{N}^{\prime})% }}}{\prod_{(n:\mathbb{N}^{\prime})}}{\prod_{(n:\mathbb{N}^{\prime})}}{\prod_{(% n:\mathbb{N}^{\prime})}}}E(n)$ has the following computation rules:

•

$\mathsf{rec}_{\mathbb{N}^{\prime}}(E,e_{z},e_{s},0^{\prime})\equiv e_{z}$ ,
•

$\mathsf{rec}_{\mathbb{N}^{\prime}}(E,e_{z},e_{s},\mathsf{succ}^{\prime}(n))% \equiv e_{s}(n,\mathsf{rec}_{\mathbb{N}^{\prime}}(E,e_{z},e_{s},n))$ for any $n:\mathbb{N}^{\prime}$ .

But what is the relation between $\mathbb{N}$ and $\mathbb{N}^{\prime}$ ?

This is not just an academic question, since structures that “look like” the natural numbers can be found in many other places. For instance, we may identify natural numbers with lists over the type with one element (this is arguably the oldest appearance, found on walls of caves), with the non-negative integers, with subsets of the rationals and the reals, and so on. And from a programming point of view, the “unary” representation of our natural numbers is very inefficient, so we might prefer sometimes to use a binary one instead. We would like to be able to identify all of these versions of “the natural numbers” with each other, in order to transfer constructions and results from one to another.

Of course, if two versions of the natural numbers satisfy identical induction principles, then they have identical induced structure. For instance, recall the example of the function $\mathsf{double}$ defined in §1.9 (http://planetmath.org/19thenaturalnumbers). A similar function for our new natural numbers is readily defined by duplication and adding primes:

\mathsf{double}^{\prime}:\!\!\equiv\mathsf{rec}_{\mathbb{N}^{\prime}}(\mathbb{% N}^{\prime},\;0^{\prime},\;{\lambda}n.\,{\lambda}m.\,\mathsf{succ}^{\prime}(% \mathsf{succ}^{\prime}(m))).

Simple as this may seem, it has the obvious drawback of leading to a proliferation of duplicates. Not only functions have to be duplicated, but also all lemmas and their proofs. For example, an easy result such as $\mathchoice{\prod_{n:\mathbb{N}}\,}{\mathchoice{{\textstyle\prod_{(n:\mathbb{N% })}}}{\prod_{(n:\mathbb{N})}}{\prod_{(n:\mathbb{N})}}{\prod_{(n:\mathbb{N})}}}% {\mathchoice{{\textstyle\prod_{(n:\mathbb{N})}}}{\prod_{(n:\mathbb{N})}}{\prod% _{(n:\mathbb{N})}}{\prod_{(n:\mathbb{N})}}}{\mathchoice{{\textstyle\prod_{(n:% \mathbb{N})}}}{\prod_{(n:\mathbb{N})}}{\prod_{(n:\mathbb{N})}}{\prod_{(n:% \mathbb{N})}}}\mathsf{double}(\mathsf{succ}(n))=\mathsf{succ}(\mathsf{succ}(% \mathsf{double}(n)))$ , as well as its proof by induction, also has to be “primed”.

In traditional mathematics, one just proclaims that $\mathbb{N}$ and $\mathbb{N}^{\prime}$ are obviously “the same”, and can be substituted for each other whenever the need arises. This is usually unproblematic, but it sweeps a fair amount under the rug, widening the gap between informal mathematics and its precise description. In homotopy type theory, we can do better.

First observe that we have the following definable maps:

•

$f:\!\!\equiv\mathsf{rec}_{\mathbb{N}}(\mathbb{N},\;0^{\prime},\;{\lambda}n.\,% \mathsf{succ}^{\prime}):\mathbb{N}\to\mathbb{N}^{\prime}$ ,
•

$g:\!\!\equiv\mathsf{rec}_{\mathbb{N}^{\prime}}(\mathbb{N}^{\prime},\;0,\;{% \lambda}n.\,,\mathsf{succ}):\mathbb{N}^{\prime}\to\mathbb{N}$ .

Since the composition of $g$ and $f$ satisfies the same recurrences as the identity function on $\mathbb{N}$ , Theorem 5.1.1 (http://planetmath.org/51introductiontoinductivetypes#Thmprethm1) gives that $\mathchoice{\prod_{n:\mathbb{N}}\,}{\mathchoice{{\textstyle\prod_{(n:\mathbb{N% })}}}{\prod_{(n:\mathbb{N})}}{\prod_{(n:\mathbb{N})}}{\prod_{(n:\mathbb{N})}}}% {\mathchoice{{\textstyle\prod_{(n:\mathbb{N})}}}{\prod_{(n:\mathbb{N})}}{\prod% _{(n:\mathbb{N})}}{\prod_{(n:\mathbb{N})}}}{\mathchoice{{\textstyle\prod_{(n:% \mathbb{N})}}}{\prod_{(n:\mathbb{N})}}{\prod_{(n:\mathbb{N})}}{\prod_{(n:% \mathbb{N})}}}g(f(n))=n$ , and the “primed” version of the same theorem gives $\mathchoice{\prod_{n:\mathbb{N}^{\prime}}\,}{\mathchoice{{\textstyle\prod_{(n:% \mathbb{N}^{\prime})}}}{\prod_{(n:\mathbb{N}^{\prime})}}{\prod_{(n:\mathbb{N}^% {\prime})}}{\prod_{(n:\mathbb{N}^{\prime})}}}{\mathchoice{{\textstyle\prod_{(n% :\mathbb{N}^{\prime})}}}{\prod_{(n:\mathbb{N}^{\prime})}}{\prod_{(n:\mathbb{N}% ^{\prime})}}{\prod_{(n:\mathbb{N}^{\prime})}}}{\mathchoice{{\textstyle\prod_{(% n:\mathbb{N}^{\prime})}}}{\prod_{(n:\mathbb{N}^{\prime})}}{\prod_{(n:\mathbb{N% }^{\prime})}}{\prod_{(n:\mathbb{N}^{\prime})}}}f(g(n))=n$ . Thus, $f$ and $g$ are quasi-inverses, so that $\mathbb{N}\simeq\mathbb{N}^{\prime}$ . We can now transfer functions on $\mathbb{N}$ directly to functions on $\mathbb{N}^{\prime}$ (and vice versa) along this equivalence, e.g.

\mathsf{double}^{\prime}:\!\!\equiv{\lambda}n.\,f(\mathsf{double}(g(n))).

It is an easy exercise to show that this version of $\mathsf{double}^{\prime}$ is equal to the earlier one.

Of course, there is nothing surprising about this; such an isomorphism is exactly how a mathematician will envision “identifying” $\mathbb{N}$ with $\mathbb{N}^{\prime}$ . However, the mechanism of “transfer” across an isomorphism depends on the thing being transferred; it is not always as simple as pre- and post-composing a single function with $f$ and $g$ . Consider, for instance, a simple lemma such as

\mathchoice{\prod_{n:\mathbb{N}^{\prime}}\,}{\mathchoice{{\textstyle\prod_{(n:% \mathbb{N}^{\prime})}}}{\prod_{(n:\mathbb{N}^{\prime})}}{\prod_{(n:\mathbb{N}^% {\prime})}}{\prod_{(n:\mathbb{N}^{\prime})}}}{\mathchoice{{\textstyle\prod_{(n% :\mathbb{N}^{\prime})}}}{\prod_{(n:\mathbb{N}^{\prime})}}{\prod_{(n:\mathbb{N}% ^{\prime})}}{\prod_{(n:\mathbb{N}^{\prime})}}}{\mathchoice{{\textstyle\prod_{(% n:\mathbb{N}^{\prime})}}}{\prod_{(n:\mathbb{N}^{\prime})}}{\prod_{(n:\mathbb{N% }^{\prime})}}{\prod_{(n:\mathbb{N}^{\prime})}}}\mathsf{double}^{\prime}(% \mathsf{succ}^{\prime}(n))=\mathsf{succ}^{\prime}(\mathsf{succ}^{\prime}(% \mathsf{double}^{\prime}(n))).

Inserting the correct $f$ s and $g$ s is only a little easier than re-proving it by induction on $n:\mathbb{N}^{\prime}$ directly.

Here is where the univalence axiom steps in: since $\mathbb{N}\simeq\mathbb{N}^{\prime}$ , we also have $\mathbb{N}=_{\mathcal{U}}\mathbb{N}^{\prime}$ , i.e. $\mathbb{N}$ and $\mathbb{N}^{\prime}$ are equal as types. Now the induction principle for identity guarantees that any construction or proof relating to $\mathbb{N}$ can automatically be transferred to $\mathbb{N}^{\prime}$ in the same way. We simply consider the type of the function or theorem as a type-indexed family of types $P:\mathcal{U}\to\mathcal{U}$ , with the given object being an element of $P(\mathbb{N})$ , and transport along the path $\mathbb{N}=\mathbb{N}^{\prime}$ . This involves considerably less overhead.

For simplicity, we have described this method in the case of two types $\mathbb{N}$ and $\mathbb{N}^{\prime}$ with identical-looking definitions. However, a more common situation in practice is when the definitions are not literally identical, but nevertheless one induction principle implies the other. Consider, for instance, the type of lists from a one-element type, $\mathsf{List}(\mathbf{1})$ , which is generated by

•

an element $\mathsf{nil}:\mathsf{List}(\mathbf{1})$ , and
•

a function $\mathsf{cons}:\mathbf{1}\times\mathsf{List}(\mathbf{1})\to\mathsf{List}(% \mathbf{1})$ .

This is not identical to the definition of $\mathbb{N}$ , and it does not give rise to an identical induction principle. The induction principle of $\mathsf{List}(\mathbf{1})$ says that for any $E:\mathsf{List}(\mathbf{1})\to\mathcal{U}$ together with recurrence data $e_{\mathsf{nil}}:E(\mathsf{nil})$ and $e_{\mathsf{cons}}:\mathchoice{\prod_{(u:\mathbf{1})}\,}{\mathchoice{{% \textstyle\prod_{(u:\mathbf{1})}}}{\prod_{(u:\mathbf{1})}}{\prod_{(u:\mathbf{1% })}}{\prod_{(u:\mathbf{1})}}}{\mathchoice{{\textstyle\prod_{(u:\mathbf{1})}}}{% \prod_{(u:\mathbf{1})}}{\prod_{(u:\mathbf{1})}}{\prod_{(u:\mathbf{1})}}}{% \mathchoice{{\textstyle\prod_{(u:\mathbf{1})}}}{\prod_{(u:\mathbf{1})}}{\prod_% {(u:\mathbf{1})}}{\prod_{(u:\mathbf{1})}}}\mathchoice{\prod_{(\ell:\mathsf{% List}(\mathbf{1}))}\,}{\mathchoice{{\textstyle\prod_{(\ell:\mathsf{List}(% \mathbf{1}))}}}{\prod_{(\ell:\mathsf{List}(\mathbf{1}))}}{\prod_{(\ell:\mathsf% {List}(\mathbf{1}))}}{\prod_{(\ell:\mathsf{List}(\mathbf{1}))}}}{\mathchoice{{% \textstyle\prod_{(\ell:\mathsf{List}(\mathbf{1}))}}}{\prod_{(\ell:\mathsf{List% }(\mathbf{1}))}}{\prod_{(\ell:\mathsf{List}(\mathbf{1}))}}{\prod_{(\ell:% \mathsf{List}(\mathbf{1}))}}}{\mathchoice{{\textstyle\prod_{(\ell:\mathsf{List% }(\mathbf{1}))}}}{\prod_{(\ell:\mathsf{List}(\mathbf{1}))}}{\prod_{(\ell:% \mathsf{List}(\mathbf{1}))}}{\prod_{(\ell:\mathsf{List}(\mathbf{1}))}}}E(\ell)% \to E(\mathsf{cons}(u,\ell))$ , there exists $f:\mathchoice{\prod_{\ell:\mathsf{List}(\mathbf{1})}\,}{\mathchoice{{% \textstyle\prod_{(\ell:\mathsf{List}(\mathbf{1}))}}}{\prod_{(\ell:\mathsf{List% }(\mathbf{1}))}}{\prod_{(\ell:\mathsf{List}(\mathbf{1}))}}{\prod_{(\ell:% \mathsf{List}(\mathbf{1}))}}}{\mathchoice{{\textstyle\prod_{(\ell:\mathsf{List% }(\mathbf{1}))}}}{\prod_{(\ell:\mathsf{List}(\mathbf{1}))}}{\prod_{(\ell:% \mathsf{List}(\mathbf{1}))}}{\prod_{(\ell:\mathsf{List}(\mathbf{1}))}}}{% \mathchoice{{\textstyle\prod_{(\ell:\mathsf{List}(\mathbf{1}))}}}{\prod_{(\ell% :\mathsf{List}(\mathbf{1}))}}{\prod_{(\ell:\mathsf{List}(\mathbf{1}))}}{\prod_% {(\ell:\mathsf{List}(\mathbf{1}))}}}E(\ell)$ such that $f(\mathsf{nil})\equiv e_{\mathsf{nil}}$ and $f(\mathsf{cons}(u,\ell))\equiv e_{\mathsf{cons}}(u,\ell,f(\ell))$ . (We will see how to derive the induction principle of an inductive definition in §5.6 (http://planetmath.org/56thegeneralsyntaxofinductivedefinitions).)

Now suppose we define $0^{\prime\prime}:\!\!\equiv\mathsf{nil}:\mathsf{List}(\mathbf{1})$ , and $\mathsf{succ}^{\prime\prime}:\mathsf{List}(\mathbf{1})\to\mathsf{List}(\mathbf% {1})$ by $\mathsf{succ}^{\prime\prime}(\ell):\!\!\equiv\mathsf{cons}(\star,\ell)$ . Then for any $E:\mathsf{List}(\mathbf{1})\to\mathcal{U}$ together with $e_{0}:E(0^{\prime\prime})$ and $e_{s}:\mathchoice{\prod_{\ell:\mathsf{List}(\mathbf{1})}\,}{\mathchoice{{% \textstyle\prod_{(\ell:\mathsf{List}(\mathbf{1}))}}}{\prod_{(\ell:\mathsf{List% }(\mathbf{1}))}}{\prod_{(\ell:\mathsf{List}(\mathbf{1}))}}{\prod_{(\ell:% \mathsf{List}(\mathbf{1}))}}}{\mathchoice{{\textstyle\prod_{(\ell:\mathsf{List% }(\mathbf{1}))}}}{\prod_{(\ell:\mathsf{List}(\mathbf{1}))}}{\prod_{(\ell:% \mathsf{List}(\mathbf{1}))}}{\prod_{(\ell:\mathsf{List}(\mathbf{1}))}}}{% \mathchoice{{\textstyle\prod_{(\ell:\mathsf{List}(\mathbf{1}))}}}{\prod_{(\ell% :\mathsf{List}(\mathbf{1}))}}{\prod_{(\ell:\mathsf{List}(\mathbf{1}))}}{\prod_% {(\ell:\mathsf{List}(\mathbf{1}))}}}E(\ell)\to E(\mathsf{succ}^{\prime\prime}(% \ell))$ , we can define

	$\displaystyle e_{\mathsf{nil}}$	$\displaystyle:\!\!\equiv e_{0}$
	$\displaystyle e_{\mathsf{cons}}(\star,\ell,x)$	$\displaystyle:\!\!\equiv e_{s}(\ell,x).$

(In the definition of $e_{\mathsf{cons}}$ we use the induction principle of $\mathbf{1}$ to assume that $u$ is $\star$ .) Now we can apply the induction principle of $\mathsf{List}(\mathbf{1})$ , obtaining $f:\mathchoice{\prod_{\ell:\mathsf{List}(\mathbf{1})}\,}{\mathchoice{{% \textstyle\prod_{(\ell:\mathsf{List}(\mathbf{1}))}}}{\prod_{(\ell:\mathsf{List% }(\mathbf{1}))}}{\prod_{(\ell:\mathsf{List}(\mathbf{1}))}}{\prod_{(\ell:% \mathsf{List}(\mathbf{1}))}}}{\mathchoice{{\textstyle\prod_{(\ell:\mathsf{List% }(\mathbf{1}))}}}{\prod_{(\ell:\mathsf{List}(\mathbf{1}))}}{\prod_{(\ell:% \mathsf{List}(\mathbf{1}))}}{\prod_{(\ell:\mathsf{List}(\mathbf{1}))}}}{% \mathchoice{{\textstyle\prod_{(\ell:\mathsf{List}(\mathbf{1}))}}}{\prod_{(\ell% :\mathsf{List}(\mathbf{1}))}}{\prod_{(\ell:\mathsf{List}(\mathbf{1}))}}{\prod_% {(\ell:\mathsf{List}(\mathbf{1}))}}}E(\ell)$ such that

	$\displaystyle f(0^{\prime\prime})\equiv f(\mathsf{nil})\equiv e_{\mathsf{nil}}% \equiv e_{0}$
	$\displaystyle f(\mathsf{succ}^{\prime\prime}(\ell))\equiv f(\mathsf{cons}(% \star,\ell))\equiv e_{\mathsf{cons}}(\star,\ell,f(\ell))\equiv e_{s}(\ell,f(% \ell)).$

Thus, $\mathsf{List}(\mathbf{1})$ satisfies the same induction principle as $\mathbb{N}$ , and hence (by the same arguments above) is equal to it.

Finally, these conclusions are not confined to the natural numbers: they apply to any inductive type. If we have an inductively defined type $W$ , say, and some other type $W^{\prime}$ which satisfies the same induction principle as $W$ , then it follows that $W\simeq W^{\prime}$ , and hence $W=W^{\prime}$ . We use the derived recursion principles for $W$ and $W^{\prime}$ to construct maps $W\to W^{\prime}$ and $W^{\prime}\to W$ , respectively, and then the induction principles for each to prove that both composites are equal to identities. For instance, in http://planetmath.org/node/87533Chapter 1 we saw that the coproduct $A+B$ could also have been defined as $\mathchoice{\sum_{x:\mathbf{2}}\,}{\mathchoice{{\textstyle\sum_{(x:\mathbf{2})% }}}{\sum_{(x:\mathbf{2})}}{\sum_{(x:\mathbf{2})}}{\sum_{(x:\mathbf{2})}}}{% \mathchoice{{\textstyle\sum_{(x:\mathbf{2})}}}{\sum_{(x:\mathbf{2})}}{\sum_{(x% :\mathbf{2})}}{\sum_{(x:\mathbf{2})}}}{\mathchoice{{\textstyle\sum_{(x:\mathbf% {2})}}}{\sum_{(x:\mathbf{2})}}{\sum_{(x:\mathbf{2})}}{\sum_{(x:\mathbf{2})}}}% \mathsf{rec}_{\mathbf{2}}(\mathcal{U},A,B,x)$ . The latter type satisfies the same induction principle as the former; hence they are canonically equivalent.

This is, of course, very similar to the familiar fact in category theory that if two objects have the same universal property, then they are equivalent. In §5.4 (http://planetmath.org/54inductivetypesareinitialalgebras) we will see that inductive types actually do have a universal property, so that this is a manifestation of that general principle.

Title	5.2 Uniqueness of inductive types
\metatable