1.12.1 Path Induction

The induction principle for the identity type is called path induction, in view of the homotopical interpretation to be explained in the introduction to http://planetmath.org/node/87569Chapter 2. It can be seen as stating that the family of identity types is freely generated by the elements of the form $\mathsf{refl}_{x}:x=x$ .

Path induction:

Given a family

C:\mathchoice{\prod_{x,y:A}\,}{\mathchoice{{\textstyle\prod_{(x,y:A)}}}{\prod_% {(x,y:A)}}{\prod_{(x,y:A)}}{\prod_{(x,y:A)}}}{\mathchoice{{\textstyle\prod_{(x% ,y:A)}}}{\prod_{(x,y:A)}}{\prod_{(x,y:A)}}{\prod_{(x,y:A)}}}{\mathchoice{{% \textstyle\prod_{(x,y:A)}}}{\prod_{(x,y:A)}}{\prod_{(x,y:A)}}{\prod_{(x,y:A)}}% }(x=_{A}y)\to\mathcal{U}

and a function

c:\mathchoice{\prod_{x:A}\,}{\mathchoice{{\textstyle\prod_{(x:A)}}}{\prod_{(x:% A)}}{\prod_{(x:A)}}{\prod_{(x:A)}}}{\mathchoice{{\textstyle\prod_{(x:A)}}}{% \prod_{(x:A)}}{\prod_{(x:A)}}{\prod_{(x:A)}}}{\mathchoice{{\textstyle\prod_{(x% :A)}}}{\prod_{(x:A)}}{\prod_{(x:A)}}{\prod_{(x:A)}}}C(x,x,\mathsf{refl}_{x}),

there is a function

f:\mathchoice{\prod_{(x,y:A)}\,}{\mathchoice{{\textstyle\prod_{(x,y:A)}}}{% \prod_{(x,y:A)}}{\prod_{(x,y:A)}}{\prod_{(x,y:A)}}}{\mathchoice{{\textstyle% \prod_{(x,y:A)}}}{\prod_{(x,y:A)}}{\prod_{(x,y:A)}}{\prod_{(x,y:A)}}}{% \mathchoice{{\textstyle\prod_{(x,y:A)}}}{\prod_{(x,y:A)}}{\prod_{(x,y:A)}}{% \prod_{(x,y:A)}}}\mathchoice{\prod_{(p:x=_{A}y)}\,}{\mathchoice{{\textstyle% \prod_{(p:x=_{A}y)}}}{\prod_{(p:x=_{A}y)}}{\prod_{(p:x=_{A}y)}}{\prod_{(p:x=_{% A}y)}}}{\mathchoice{{\textstyle\prod_{(p:x=_{A}y)}}}{\prod_{(p:x=_{A}y)}}{% \prod_{(p:x=_{A}y)}}{\prod_{(p:x=_{A}y)}}}{\mathchoice{{\textstyle\prod_{(p:x=% _{A}y)}}}{\prod_{(p:x=_{A}y)}}{\prod_{(p:x=_{A}y)}}{\prod_{(p:x=_{A}y)}}}C(x,y% ,p)

such that

f(x,x,\mathsf{refl}_{x}):\!\!\equiv c(x).

Note that just like the induction principles for products, coproducts, natural numbers, and so on, path induction allows us to define specified functions which exhibit appropriate computational behavior. Just as we have the function $f:\mathbb{N}\to C$ defined by recursion from $c_{0}:C$ and $c_{s}:\mathbb{N}\to C\to C$ , which moreover satisfies $f(0)\equiv c_{0}$ and $f(\mathsf{succ}(n))\equiv c_{s}(n,f(n))$ , we have the function $f:\prod_{(x,y:A)}\,\prod_{(p:x=_{A}y)}\,C(x,y,p)$ defined by path induction from $c:\mathchoice{\prod_{x:A}\,}{\mathchoice{{\textstyle\prod_{(x:A)}}}{\prod_{(x:% A)}}{\prod_{(x:A)}}{\prod_{(x:A)}}}{\mathchoice{{\textstyle\prod_{(x:A)}}}{% \prod_{(x:A)}}{\prod_{(x:A)}}{\prod_{(x:A)}}}{\mathchoice{{\textstyle\prod_{(x% :A)}}}{\prod_{(x:A)}}{\prod_{(x:A)}}{\prod_{(x:A)}}}C(x,x,\mathsf{refl}_{x})$ , which moreover satisfies $f(x,x,\mathsf{refl}_{x})\equiv c(x)$ .

To understand the meaning of this principle, consider first the simpler case when $C$ does not depend on $p$ . Then we have $C:A\to A\to\mathcal{U}$ , which we may regard as a predicate depending on two elements of $A$ . We are interested in knowing when the proposition $C(x,y)$ holds for some pair of elements $x, y : A$ . In this case, the hypothesis of path induction says that we know $C(x,x)$ holds for all $x : A$ , i.e. that if we evaluate $C$ at the pair $x, x$ , we get a true proposition — so $C$ is a reflexive relation. The conclusion then tells us that $C(x,y)$ holds whenever $x=y$ . This is exactly the more general recursion principle for reflexive relations mentioned above.

The general, inductive form of the rule allows $C$ to also depend on the witness $p:x=y$ to the identity between $x$ and $y$ . In the premise, we not only replace $x, y$ by $x, x$ , but also simultaneously replace $p$ by reflexivity: to prove a property for all elements $x, y$ and paths $p:x=y$ between them, it suffices to consider all the cases where the elements are $x, x$ and the path is $\mathsf{refl}_{x}:x=x$ . If we were viewing types just as sets, it would be unclear what this buys us, but since there may be many different identifications $p:x=y$ between $x$ and $y$ , it makes sense to keep track of them in considering families over the type $x=_{A}y$ . In http://planetmath.org/node/87569Chapter 2 we will see that this is very important to the homotopy interpretation.

If we package up path induction into a single function, it takes the form:

\mathsf{ind}_{=_{A}}:\prod_{(C:\mathchoice{\prod_{x,y:A}\,}{\mathchoice{{% \textstyle\prod_{(x,y:A)}}}{\prod_{(x,y:A)}}{\prod_{(x,y:A)}}{\prod_{(x,y:A)}}% }{\mathchoice{{\textstyle\prod_{(x,y:A)}}}{\prod_{(x,y:A)}}{\prod_{(x,y:A)}}{% \prod_{(x,y:A)}}}{\mathchoice{{\textstyle\prod_{(x,y:A)}}}{\prod_{(x,y:A)}}{% \prod_{(x,y:A)}}{\prod_{(x,y:A)}}}(x=_{A}y)\to\mathcal{U})}\,\Bigl{(}% \mathchoice{{\textstyle\prod_{(x:A)}}}{\prod_{(x:A)}}{\prod_{(x:A)}}{\prod_{(x% :A)}}C(x,x,\mathsf{refl}_{x})\Bigr{)}\to\prod_{(x,y:A)}\,\prod_{(p:x=_{A}y)}\,% C(x,y,p)

with the equality

\mathsf{ind}_{=_{A}}(C,c,x,x,\mathsf{refl}_{x}):\!\!\equiv c(x).

The function $\mathsf{ind}_{=_{A}}$ is traditionally called $J$ . We leave it as an easy exercise to show that indiscernability of identicals follows from path induction.

Given a proof $p:a=b$ , path induction requires us to replace both $a$ and $b$ with the same unknown element $x$ ; thus in order to define an element of a family $C$ , for all pairs of elements of $A$ , it suffices to define it on the diagonal. In some proofs, however, it is simpler to make use of an equation $p:a=b$ by replacing all occurrences of $b$ with $a$ (or vice versa), because it is sometimes easier to do the remainder of the proof for the specific element $a$ mentioned in the equality than for a general unknown $x$ . This motivates a second induction principle for identity types, which says that the family of types $a=_{A}x$ is generated by the element $\mathsf{refl}_{a}:a=a$ . As we show below, this second principle is equivalent to the first; it is just sometimes a more convenient formulation.

Based path induction:

Fix an element $a : A$ , and suppose given a family

C:\mathchoice{\prod_{x:A}\,}{\mathchoice{{\textstyle\prod_{(x:A)}}}{\prod_{(x:% A)}}{\prod_{(x:A)}}{\prod_{(x:A)}}}{\mathchoice{{\textstyle\prod_{(x:A)}}}{% \prod_{(x:A)}}{\prod_{(x:A)}}{\prod_{(x:A)}}}{\mathchoice{{\textstyle\prod_{(x% :A)}}}{\prod_{(x:A)}}{\prod_{(x:A)}}{\prod_{(x:A)}}}(a=_{A}x)\to\mathcal{U}

and an element

c:C(a,\mathsf{refl}_{a}).

Then we obtain a function

f:\mathchoice{\prod_{(x:A)}\,}{\mathchoice{{\textstyle\prod_{(x:A)}}}{\prod_{(% x:A)}}{\prod_{(x:A)}}{\prod_{(x:A)}}}{\mathchoice{{\textstyle\prod_{(x:A)}}}{% \prod_{(x:A)}}{\prod_{(x:A)}}{\prod_{(x:A)}}}{\mathchoice{{\textstyle\prod_{(x% :A)}}}{\prod_{(x:A)}}{\prod_{(x:A)}}{\prod_{(x:A)}}}\mathchoice{\prod_{(p:a=x)% }\,}{\mathchoice{{\textstyle\prod_{(p:a=x)}}}{\prod_{(p:a=x)}}{\prod_{(p:a=x)}% }{\prod_{(p:a=x)}}}{\mathchoice{{\textstyle\prod_{(p:a=x)}}}{\prod_{(p:a=x)}}{% \prod_{(p:a=x)}}{\prod_{(p:a=x)}}}{\mathchoice{{\textstyle\prod_{(p:a=x)}}}{% \prod_{(p:a=x)}}{\prod_{(p:a=x)}}{\prod_{(p:a=x)}}}C(x,p)

such that

f(a,\mathsf{refl}_{a}):\!\!\equiv c.

Here, $C(x,p)$ is a family of types, where $x$ is an element of $A$ and $p$ is an element of the identity type $a=_{A}x$ , for fixed $a$ in $A$ . The based path induction principle says that to define an element of this family for all $x$ and $p$ , it suffices to consider just the case where $x$ is $a$ and $p$ is $\mathsf{refl}_{a}:a=a$ .

Packaged as a function, based path induction becomes:

\displaystyle\mathsf{ind}_{=_{A}}^{\prime}:\prod_{(a:A)}\,\prod_{(C:% \mathchoice{\prod_{x:A}\,}{\mathchoice{{\textstyle\prod_{(x:A)}}}{\prod_{(x:A)% }}{\prod_{(x:A)}}{\prod_{(x:A)}}}{\mathchoice{{\textstyle\prod_{(x:A)}}}{\prod% _{(x:A)}}{\prod_{(x:A)}}{\prod_{(x:A)}}}{\mathchoice{{\textstyle\prod_{(x:A)}}% }{\prod_{(x:A)}}{\prod_{(x:A)}}{\prod_{(x:A)}}}(a=_{A}x)\to\mathcal{U})}\,C(a,% \mathsf{refl}_{a})\to\prod_{(x:A)}\,\prod_{(p:a=_{A}x)}\,C(x,p)

with the equality

\mathsf{ind}_{=_{A}}^{\prime}(a,C,c,a,\mathsf{refl}_{a}):\!\!\equiv c.

Below, we show that path induction and based path induction are equivalent. Because of this, we will sometimes be sloppy and also refer to based path induction simply as “path induction,” relying on the reader to infer which principle is meant from the form of the proof.

Remark 1.

Intuitively, the induction principle for the natural numbers expresses the fact that the only natural numbers are $0$ and $\mathsf{succ}(n)$ , so if we prove a property for these cases, then we have proved it for all natural numbers. Applying this same reading to path induction, we might loosely say that path induction expresses the fact that the only path is $\mathsf{refl}$ , so if we prove a property for reflexivity, then we have proved it for all paths. However, this reading is quite confusing in the context of the homotopy interpretation of paths, where there may be many different ways in which two elements $a$ and $b$ can be identified, and therefore many different elements of the identity type! How can there be many different paths, but at the same time we have an induction principle asserting that the only path is reflexivity?

The key observation is that it is not the identity type that is inductively defined, but the identity family. In particular, path induction says that the family of types $(x=_{A}y)$ , as $x, y$ vary over all elements of $A$ , is inductively defined by the elements of the form $\mathsf{refl}_{x}$ . This means that to give an element of any other family $C(x,y,p)$ dependent on a generic element $(x,y,p)$ of the identity family, it suffices to consider the cases of the form $(x,x,\mathsf{refl}_{x})$ . In the homotopy interpretation, this says that the type of triples $(x,y,p)$ , where $x$ and $y$ are the endpoints of the path $p$ (in other words, the $\Sigma$ -type $\mathchoice{\sum_{x,y:A}\,}{\mathchoice{{\textstyle\sum_{(x,y:A)}}}{\sum_{(x,y% :A)}}{\sum_{(x,y:A)}}{\sum_{(x,y:A)}}}{\mathchoice{{\textstyle\sum_{(x,y:A)}}}% {\sum_{(x,y:A)}}{\sum_{(x,y:A)}}{\sum_{(x,y:A)}}}{\mathchoice{{\textstyle\sum_% {(x,y:A)}}}{\sum_{(x,y:A)}}{\sum_{(x,y:A)}}{\sum_{(x,y:A)}}}(x=y)$ ), is inductively generated by the constant loops at each point $x$ . In homotopy theory, the space corresponding to $\mathchoice{\sum_{x,y:A}\,}{\mathchoice{{\textstyle\sum_{(x,y:A)}}}{\sum_{(x,y% :A)}}{\sum_{(x,y:A)}}{\sum_{(x,y:A)}}}{\mathchoice{{\textstyle\sum_{(x,y:A)}}}% {\sum_{(x,y:A)}}{\sum_{(x,y:A)}}{\sum_{(x,y:A)}}}{\mathchoice{{\textstyle\sum_% {(x,y:A)}}}{\sum_{(x,y:A)}}{\sum_{(x,y:A)}}{\sum_{(x,y:A)}}}(x=y)$ is the free path space — the space of paths in $A$ whose endpoints may vary — and it is in fact the case that any point of this space is homotopic to the constant loop at some point, since we can simply retract one of its endpoints along the given path.

Similarly, based path induction says that for a fixed $a : A$ , the family of types $(a=_{A}y)$ , as $y$ varies over all elements of $A$ , is inductively defined by the element $\mathsf{refl}_{a}$ . Thus, to give an element of any other family $C(y,p)$ dependent on a generic element $(y,p)$ of this family, it suffices to consider the case $(a,\mathsf{refl}_{a})$ . Homotopically, this expresses the fact that the space of paths starting at some chosen point (the based path space at that point, which type-theoretically is $\mathchoice{\sum_{y:A}\,}{\mathchoice{{\textstyle\sum_{(y:A)}}}{\sum_{(y:A)}}{% \sum_{(y:A)}}{\sum_{(y:A)}}}{\mathchoice{{\textstyle\sum_{(y:A)}}}{\sum_{(y:A)% }}{\sum_{(y:A)}}{\sum_{(y:A)}}}{\mathchoice{{\textstyle\sum_{(y:A)}}}{\sum_{(y% :A)}}{\sum_{(y:A)}}{\sum_{(y:A)}}}(a=y)$ ) is contractible to the constant loop on the chosen point. Note that according to propositions-as-types, the type $\mathchoice{\sum_{y:A}\,}{\mathchoice{{\textstyle\sum_{(y:A)}}}{\sum_{(y:A)}}{% \sum_{(y:A)}}{\sum_{(y:A)}}}{\mathchoice{{\textstyle\sum_{(y:A)}}}{\sum_{(y:A)% }}{\sum_{(y:A)}}{\sum_{(y:A)}}}{\mathchoice{{\textstyle\sum_{(y:A)}}}{\sum_{(y% :A)}}{\sum_{(y:A)}}{\sum_{(y:A)}}}(a=y)$ can be regarded as “the type of all elements of $A$ which are equal to $a$ ”, a type-theoretic version of the “singleton subset” $\{a\}$ .

Neither of these two principles provides a way to give an element of a family $C(p)$ where $p$ has two fixed endpoints $a$ and $b$ . In particular, for a family $C(p:a=_{A}a)$ dependent on a loop, we cannot apply path induction and consider only the case for $C(\mathsf{refl}_{a})$ , and consequently, we cannot prove that all loops are reflexivity. Thus, inductively defining the identity family does not prohibit non-reflexivity paths in specific instances of the identity type. In other words, a path $p:x=x$ may be not equal to reflexivity as an element of $(x=x)$ , but the pair $(x,p)$ will nevertheless be equal to the pair $(x,\mathsf{refl}_{x})$ as elements of $\mathchoice{\sum_{y:A}\,}{\mathchoice{{\textstyle\sum_{(y:A)}}}{\sum_{(y:A)}}{% \sum_{(y:A)}}{\sum_{(y:A)}}}{\mathchoice{{\textstyle\sum_{(y:A)}}}{\sum_{(y:A)% }}{\sum_{(y:A)}}{\sum_{(y:A)}}}{\mathchoice{{\textstyle\sum_{(y:A)}}}{\sum_{(y% :A)}}{\sum_{(y:A)}}{\sum_{(y:A)}}}(x=y)$ .

Title	1.12.1 Path Induction
\metatable