5.1 Introduction to inductive types

An inductive type $X$ can be intuitively understood as a type “freely generated” by a certain finite collection of constructors, each of which is a function (of some number of arguments) with codomain $X$ . This includes functions of zero arguments, which are simply elements of $X$ .

When describing a particular inductive type, we list the constructors with bullets. For instance, the type $\mathbf{2}$ from §1.8 (http://planetmath.org/18thetypeofbooleans) is inductively generated by the following constructors:

•

${0_{\mathbf{2}}}:\mathbf{2}$
•

${1_{\mathbf{2}}}:\mathbf{2}$

Similarly, $\mathbf{1}$ is inductively generated by the constructor:

•

$\star:\mathbf{1}$

while $\mathbf{0}$ is inductively generated by no constructors at all. An example where the constructor functions take arguments is the coproduct $A+B$ , which is generated by the two constructors

•

${\mathsf{inl}}:A\to A+B$
•

${\mathsf{inr}}:B\to A+B$ .

And an example with a constructor taking multiple arguments is the cartesian product $A\times B$ , which is generated by one constructor

•

${\mathopen{}(\mathord{\hskip 1.0pt\text{--}\hskip 1.0pt},\mathord{\hskip 1.0pt% \text{--}\hskip 1.0pt})\mathclose{}}:A\to B\to A\times B$ .

Crucially, we also allow constructors of inductive types that take arguments from the inductive type being defined. For instance, the type $\mathbb{N}$ of natural numbers has constructors

•

$0:\mathbb{N}$
•

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

Another useful example is the type $\mathsf{List}(A)$ of finite lists of elements of some type $A$ , which has constructors

•

$\mathsf{nil}:\mathsf{List}(A)$
•

$\mathsf{cons}:A\to\mathsf{List}(A)\to\mathsf{List}(A)$ .

Intuitively, we should understand an inductive type as being freely generated by its constructors. That is, the elements of an inductive type are exactly what can be obtained by starting from nothing and applying the constructors repeatedly. (We will see in §5.8 (http://planetmath.org/58identitytypesandidentitysystems),http://planetmath.org/node/87579Chapter 6 that this conception has to be modified slightly for more general kinds of inductive definitions, but for now it is sufficient.) For instance, in the case of $\mathbf{2}$ , we should expect that the only elements are ${0_{\mathbf{2}}}$ and ${1_{\mathbf{2}}}$ . Similarly, in the case of $\mathbb{N}$ , we should expect that every element is either $0$ or obtained by applying $\mathsf{succ}$ to some “previously constructed” natural number.

Rather than assert properties such as this directly, however, we express them by means of an induction principle, also called a (dependent) elimination rule. We have seen these principles already in http://planetmath.org/node/87533Chapter 1. For instance, the induction principle for $\mathbf{2}$ is:

•

When proving a statement $E:\mathbf{2}\to\mathcal{U}$ about all inhabitants of $\mathbf{2}$ , it suffices to prove it for ${0_{\mathbf{2}}}$ and ${1_{\mathbf{2}}}$ , i.e., to give proofs $e_{0}:E({0_{\mathbf{2}}})$ and $e_{1}:E({1_{\mathbf{2}}})$ .

Furthermore, the resulting proof $\mathsf{ind}_{\mathbf{2}}(E,e_{0},e_{1}):\mathchoice{\prod_{b:\mathbf{2}}\,}{% \mathchoice{{\textstyle\prod_{(b:\mathbf{2})}}}{\prod_{(b:\mathbf{2})}}{\prod_% {(b:\mathbf{2})}}{\prod_{(b:\mathbf{2})}}}{\mathchoice{{\textstyle\prod_{(b:% \mathbf{2})}}}{\prod_{(b:\mathbf{2})}}{\prod_{(b:\mathbf{2})}}{\prod_{(b:% \mathbf{2})}}}{\mathchoice{{\textstyle\prod_{(b:\mathbf{2})}}}{\prod_{(b:% \mathbf{2})}}{\prod_{(b:\mathbf{2})}}{\prod_{(b:\mathbf{2})}}}E(b)$ behaves as expected when applied to the constructors ${0_{\mathbf{2}}}$ and ${1_{\mathbf{2}}}$ ; this principle is expressed by the computation rules:

•

We have $\mathsf{ind}_{\mathbf{2}}(E,e_{0},e_{1},{0_{\mathbf{2}}})\equiv e_{0}$ .
•

We have $\mathsf{ind}_{\mathbf{2}}(E,e_{0},e_{1},{1_{\mathbf{2}}})\equiv e_{1}$ .

Thus, the induction principle for the type $\mathbf{2}$ of booleans allow us to reason by case analysis. Since neither of the two constructors takes any arguments, this is all we need for booleans.

For natural numbers, however, case analysis is generally not sufficient: in the case corresponding to the inductive step $\mathsf{succ}(n)$ , we also want to presume that the statement being proven has already been shown for $n$ . This gives us the following induction principle:

•

When proving a statement $E:\mathbb{N}\to\mathcal{U}$ about all natural numbers, it suffices to prove it for $0$ and for $\mathsf{succ}(n)$ , assuming it holds for $n$ , i.e., we construct $e_{z}:E(0)$ and $e_{s}:\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})}}}\mathchoice{\prod_{(y:E(n))}\,}{\mathchoice{{% \textstyle\prod_{(y:E(n))}}}{\prod_{(y:E(n))}}{\prod_{(y:E(n))}}{\prod_{(y:E(n% ))}}}{\mathchoice{{\textstyle\prod_{(y:E(n))}}}{\prod_{(y:E(n))}}{\prod_{(y:E(% n))}}{\prod_{(y:E(n))}}}{\mathchoice{{\textstyle\prod_{(y:E(n))}}}{\prod_{(y:E% (n))}}{\prod_{(y:E(n))}}{\prod_{(y:E(n))}}}E(\mathsf{succ}(n))$ .

The variable $y$ represents our inductive hypothesis. As in the case of booleans, we also have the associated computation rules for the function $\mathsf{ind}_{\mathbb{N}}(E,e_{z},e_{s}):\mathchoice{\prod_{x:\mathbb{N}}\,}{% \mathchoice{{\textstyle\prod_{(x:\mathbb{N})}}}{\prod_{(x:\mathbb{N})}}{\prod_% {(x:\mathbb{N})}}{\prod_{(x:\mathbb{N})}}}{\mathchoice{{\textstyle\prod_{(x:% \mathbb{N})}}}{\prod_{(x:\mathbb{N})}}{\prod_{(x:\mathbb{N})}}{\prod_{(x:% \mathbb{N})}}}{\mathchoice{{\textstyle\prod_{(x:\mathbb{N})}}}{\prod_{(x:% \mathbb{N})}}{\prod_{(x:\mathbb{N})}}{\prod_{(x:\mathbb{N})}}}E(x)$ :

•

$\mathsf{ind}_{\mathbb{N}}(E,e_{z},e_{s},0)\equiv e_{z}$ .
•

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

The dependent function $\mathsf{ind}_{\mathbb{N}}(E,e_{z},e_{s})$ can thus be understood as being defined recursively on the argument $x:\mathbb{N}$ , via the functions $e_{z}$ and $e_{s}$ which we call the recurrences. When $x$ is zero, the function simply returns $e_{z}$ . When $x$ is the successor of another natural number $n$ , the result is obtained by taking the recurrence $e_{s}$ and substituting the specific predecessor $n$ and the recursive call value $\mathsf{ind}_{\mathbb{N}}(E,e_{z},e_{s},n)$ .

The induction principles for all the examples mentioned above share this family resemblance. In §5.6 (http://planetmath.org/56thegeneralsyntaxofinductivedefinitions) we will discuss a general notion of “inductive definition” and how to derive an appropriate induction principle for it, but first we investigate various commonalities between inductive definitions.

For instance, we have remarked in every case in http://planetmath.org/node/87533Chapter 1 that from the induction principle we can derive a recursion principle in which the codomain is a simple type (rather than a family). Both induction and recursion principles may seem odd, since they yield only the existence of a function without seeming to characterize it uniquely. However, in fact the induction principle is strong enough also to prove its own uniqueness principle, as in the following theorem.

Theorem 5.1.1.

Let $f,g:\mathchoice{\prod_{x:\mathbb{N}}\,}{\mathchoice{{\textstyle\prod_{(x:% \mathbb{N})}}}{\prod_{(x:\mathbb{N})}}{\prod_{(x:\mathbb{N})}}{\prod_{(x:% \mathbb{N})}}}{\mathchoice{{\textstyle\prod_{(x:\mathbb{N})}}}{\prod_{(x:% \mathbb{N})}}{\prod_{(x:\mathbb{N})}}{\prod_{(x:\mathbb{N})}}}{\mathchoice{{% \textstyle\prod_{(x:\mathbb{N})}}}{\prod_{(x:\mathbb{N})}}{\prod_{(x:\mathbb{N% })}}{\prod_{(x:\mathbb{N})}}}E(x)$ be two functions which satisfy the recurrences

$e_{z}:E(0)\qquad\text{and}\qquad e_{s}:\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})}}}\mathchoice{% \prod_{(y:E(n))}\,}{\mathchoice{{\textstyle\prod_{(y:E(n))}}}{\prod_{(y:E(n))}% }{\prod_{(y:E(n))}}{\prod_{(y:E(n))}}}{\mathchoice{{\textstyle\prod_{(y:E(n))}% }}{\prod_{(y:E(n))}}{\prod_{(y:E(n))}}{\prod_{(y:E(n))}}}{\mathchoice{{% \textstyle\prod_{(y:E(n))}}}{\prod_{(y:E(n))}}{\prod_{(y:E(n))}}{\prod_{(y:E(n% ))}}}E(\mathsf{succ}(n))$

up to propositional equality, i.e., such that

$f(0)=e_{z}\qquad\text{and}\qquad g(0)=e_{z}$

as well as

	$\displaystyle\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})}}}f(\mathsf{succ}(n))=e_{s}(n,f(n)),$
	$\displaystyle\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(\mathsf{succ}(n))=e_{s}(n,g(n)).$

Then $f$ and $g$ are equal.

Proof.

We use induction on the type family $D(x):\!\!\equiv f(x)=g(x)$ . For the base case, we have

$f(0)=e_{z}=g(0)$

For the inductive case, assume $n:\mathbb{N}$ such that $f(n)=g(n)$ . Then

$f(\mathsf{succ}(n))=e_{s}(n,f(n))=e_{s}(n,g(n))=g(\mathsf{succ}(n))$

The first and last equality follow from the assumptions on $f$ and $g$ . The middle equality follows from the inductive hypothesis and the fact that application preserves equality. This gives us pointwise equality between $f$ and $g$ ; invoking function extensionality finishes the proof. ∎

Note that the uniqueness principle applies even to functions that only satisfy the recurrences up to propositional equality, i.e. a path. Of course, the particular function obtained from the induction principle satisfies these recurrences judgmentally; we will return to this point in §5.5 (http://planetmath.org/55homotopyinductivetypes). On the other hand, the theorem itself only asserts a propositional equality between functions (see also http://planetmath.org/node/87832Exercise 5.2). From a homotopical viewpoint it is natural to ask whether this path is coherent, i.e. whether the equality $f=g$ is unique up to higher paths; in §5.4 (http://planetmath.org/54inductivetypesareinitialalgebras) we will see that this is in fact the case.

Of course, similar uniqueness theorems for functions can generally be formulated and shown for other inductive types as well. In the next section, we show how this uniqueness property, together with univalence, implies that an inductive type such as the natural numbers is completely characterized by its introduction, elimination, and computation rules.

Title	5.1 Introduction to inductive types
\metatable