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 ${\mathrm{\pi \x9d\x97\x8b\pi \x9d\x96\u038e\pi \x9d\x96\u038f\pi \x9d\x97\x85}}_{x}:x=x$.
 Path induction:

Given a family
$$C:\underset{x,y:A}{\beta \x88\x8f}(x{=}_{A}y)\beta \x86\x92\mathrm{\pi \x9d\x92\xb0}$$ and a function
$$c:\underset{x:A}{\beta \x88\x8f}C\beta \x81\u2019(x,x,{\mathrm{\pi \x9d\x97\x8b\pi \x9d\x96\u038e\pi \x9d\x96\u038f\pi \x9d\x97\x85}}_{x}),$$ there is a function
$$f:\underset{(x,y:A)}{\beta \x88\x8f}\underset{(p:x{=}_{A}y)}{\beta \x88\x8f}C\beta \x81\u2019(x,y,p)$$ such that
$$f(x,x,{\mathrm{\pi \x9d\x97\x8b\pi \x9d\x96\u038e\pi \x9d\x96\u038f\pi \x9d\x97\x85}}_{x}):\beta \x89\u2018c(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:\mathrm{\beta \x84\x95}\beta \x86\x92C$ defined by recursion from ${c}_{0}:C$ and ${c}_{s}:\mathrm{\beta \x84\x95}\beta \x86\x92C\beta \x86\x92C$, which moreover satisfies $f\beta \x81\u2019(0)\beta \x89\u2018{c}_{0}$ and $f\beta \x81\u2019(\mathrm{\pi \x9d\x97\x8c\pi \x9d\x97\x8e\pi \x9d\x96\u038c\pi \x9d\x96\u038c}\beta \x81\u2019(n))\beta \x89\u2018{c}_{s}\beta \x81\u2019(n,f\beta \x81\u2019(n))$, we have the function $f:{\beta \x88\x8f}_{(x,y:A)}{\beta \x88\x8f}_{(p:x{=}_{A}y)}C\beta \x81\u2019(x,y,p)$ defined by path induction from $c:{\beta \x88\x8f}_{(x:A)}C\beta \x81\u2019(x,x,{\mathrm{\pi \x9d\x97\x8b\pi \x9d\x96\u038e\pi \x9d\x96\u038f\pi \x9d\x97\x85}}_{x})$, which moreover satisfies $f\beta \x81\u2019(x,x,{\mathrm{\pi \x9d\x97\x8b\pi \x9d\x96\u038e\pi \x9d\x96\u038f\pi \x9d\x97\x85}}_{x})\beta \x89\u2018c\beta \x81\u2019(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\beta \x86\x92A\beta \x86\x92\mathrm{\pi \x9d\x92\xb0}$, which we may regard as a predicate^{} depending on two elements of $A$. We are interested in knowing when the proposition^{} $C\beta \x81\u2019(x,y)$ holds for some pair of elements $x,y:A$. In this case, the hypothesis^{} of path induction says that we know $C\beta \x81\u2019(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\beta \x81\u2019(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 ${\mathrm{\pi \x9d\x97\x8b\pi \x9d\x96\u038e\pi \x9d\x96\u038f\pi \x9d\x97\x85}}_{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:
$${\mathrm{\pi \x9d\x97\x82\pi \x9d\x97\x87\pi \x9d\x96\xbd}}_{{=}_{A}}:\underset{(C:{\beta \x88\x8f}_{(x,y:A)}(x{=}_{A}y)\beta \x86\x92\mathrm{\pi \x9d\x92\xb0})}{\beta \x88\x8f}\left({\beta \x88\x8f}_{(x:A)}C\beta \x81\u2019(x,x,{\mathrm{\pi \x9d\x97\x8b\pi \x9d\x96\u038e\pi \x9d\x96\u038f\pi \x9d\x97\x85}}_{x})\right)\beta \x86\x92\underset{(x,y:A)}{\beta \x88\x8f}\underset{(p:x{=}_{A}y)}{\beta \x88\x8f}C\beta \x81\u2019(x,y,p)$$ 
with the equality
$${\mathrm{\pi \x9d\x97\x82\pi \x9d\x97\x87\pi \x9d\x96\xbd}}_{{=}_{A}}(C,c,x,x,{\mathrm{\pi \x9d\x97\x8b\pi \x9d\x96\u038e\pi \x9d\x96\u038f\pi \x9d\x97\x85}}_{x}):\beta \x89\u2018c(x).$$ 
The function ${\mathrm{\pi \x9d\x97\x82\pi \x9d\x97\x87\pi \x9d\x96\xbd}}_{{=}_{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 ${\mathrm{\pi \x9d\x97\x8b\pi \x9d\x96\u038e\pi \x9d\x96\u038f\pi \x9d\x97\x85}}_{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:\underset{x:A}{\beta \x88\x8f}(a{=}_{A}x)\beta \x86\x92\mathrm{\pi \x9d\x92\xb0}$$ and an element
$$c:C\beta \x81\u2019(a,{\mathrm{\pi \x9d\x97\x8b\pi \x9d\x96\u038e\pi \x9d\x96\u038f\pi \x9d\x97\x85}}_{a}).$$ Then we obtain a function
$$f:\underset{(x:A)}{\beta \x88\x8f}\underset{(p:a=x)}{\beta \x88\x8f}C\beta \x81\u2019(x,p)$$ such that
$$f(a,{\mathrm{\pi \x9d\x97\x8b\pi \x9d\x96\u038e\pi \x9d\x96\u038f\pi \x9d\x97\x85}}_{a}):\beta \x89\u2018c.$$
Here, $C\beta \x81\u2019(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 ${\mathrm{\pi \x9d\x97\x8b\pi \x9d\x96\u038e\pi \x9d\x96\u038f\pi \x9d\x97\x85}}_{a}:a=a$.
Packaged as a function, based path induction becomes:
${\mathrm{\pi \x9d\x97\x82\pi \x9d\x97\x87\pi \x9d\x96\xbd}}_{{=}_{A}}^{\beta \x80\xb2}:{\displaystyle \underset{(a:A)}{\beta \x88\x8f}}{\displaystyle \underset{(C:{\beta \x88\x8f}_{(x:A)}(a{=}_{A}x)\beta \x86\x92\mathrm{\pi \x9d\x92\xb0})}{\beta \x88\x8f}}C\beta \x81\u2019(a,{\mathrm{\pi \x9d\x97\x8b\pi \x9d\x96\u038e\pi \x9d\x96\u038f\pi \x9d\x97\x85}}_{a})\beta \x86\x92{\displaystyle \underset{(x:A)}{\beta \x88\x8f}}{\displaystyle \underset{(p:a{=}_{A}x)}{\beta \x88\x8f}}C\beta \x81\u2019(x,p)$ 
with the equality
$${\mathrm{\pi \x9d\x97\x82\pi \x9d\x97\x87\pi \x9d\x96\xbd}}_{{=}_{A}}^{\beta \x80\xb2}(a,C,c,a,{\mathrm{\pi \x9d\x97\x8b\pi \x9d\x96\u038e\pi \x9d\x96\u038f\pi \x9d\x97\x85}}_{a}):\beta \x89\u2018c.$$ 
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 $\mathrm{0}$ and $\mathrm{succ}\mathit{\beta \x81\u2019}\mathrm{(}n\mathrm{)}$, 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 $\mathrm{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 $\mathrm{(}x{\mathrm{=}}_{A}y\mathrm{)}$, as $x\mathrm{,}y$ vary over all elements of $A$, is inductively defined by the elements of the form ${\mathrm{refl}}_{x}$. This means that to give an element of any other family $C\mathit{\beta \x81\u2019}\mathrm{(}x\mathrm{,}y\mathrm{,}p\mathrm{)}$ dependent on a generic^{} element $\mathrm{(}x\mathrm{,}y\mathrm{,}p\mathrm{)}$ of the identity family, it suffices to consider the cases of the form $\mathrm{(}x\mathrm{,}x\mathrm{,}{\mathrm{refl}}_{x}\mathrm{)}$. In the homotopy interpretation, this says that the type of triples $\mathrm{(}x\mathrm{,}y\mathrm{,}p\mathrm{)}$, where $x$ and $y$ are the endpoints of the path $p$ (in other words, the $\mathrm{\Xi \pounds}$type ${\mathrm{\beta \x88\x91}}_{\mathrm{(}x\mathrm{,}y\mathrm{:}A\mathrm{)}}\mathrm{(}x\mathrm{=}y\mathrm{)}$), is inductively generated by the constant loops at each point $x$. In homotopy theory, the space corresponding to ${\mathrm{\beta \x88\x91}}_{\mathrm{(}x\mathrm{,}y\mathrm{:}A\mathrm{)}}\mathrm{(}x\mathrm{=}y\mathrm{)}$ 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\mathrm{:}A$, the family of types $\mathrm{(}a{\mathrm{=}}_{A}y\mathrm{)}$, as $y$ varies over all elements of $A$, is inductively defined by the element ${\mathrm{refl}}_{a}$. Thus, to give an element of any other family $C\mathit{\beta \x81\u2019}\mathrm{(}y\mathrm{,}p\mathrm{)}$ dependent on a generic element $\mathrm{(}y\mathrm{,}p\mathrm{)}$ of this family, it suffices to consider the case $\mathrm{(}a\mathrm{,}{\mathrm{refl}}_{a}\mathrm{)}$. Homotopically, this expresses the fact that the space of paths starting at some chosen point (the based path space at that point, which typetheoretically is ${\mathrm{\beta \x88\x91}}_{\mathrm{(}y\mathrm{:}A\mathrm{)}}\mathrm{(}a\mathrm{=}y\mathrm{)}$) is contractible to the constant loop on the chosen point. Note that according to propositionsastypes, the type ${\mathrm{\beta \x88\x91}}_{\mathrm{(}y\mathrm{:}A\mathrm{)}}\mathrm{(}a\mathrm{=}y\mathrm{)}$ can be regarded as βthe type of all elements of $A$ which are equal to $a$β, a typetheoretic version of the βsingleton subsetβ $\mathrm{\{}a\mathrm{\}}$.
Neither of these two principles provides a way to give an element of a family $C\mathit{\beta \x81\u2019}\mathrm{(}p\mathrm{)}$ where $p$ has two fixed endpoints $a$ and $b$. In particular, for a family $C\mathrm{(}p\mathrm{:}a{\mathrm{=}}_{A}a\mathrm{)}$ dependent on a loop, we cannot apply path induction and consider only the case for $C\mathit{\beta \x81\u2019}\mathrm{(}{\mathrm{refl}}_{a}\mathrm{)}$, and consequently, we cannot prove that all loops are reflexivity. Thus, inductively defining the identity family does not prohibit nonreflexivity paths in specific instances of the identity type. In other words, a path $p\mathrm{:}x\mathrm{=}x$ may be not equal to reflexivity as an element of $\mathrm{(}x\mathrm{=}x\mathrm{)}$, but the pair $\mathrm{(}x\mathrm{,}p\mathrm{)}$ will nevertheless be equal to the pair $\mathrm{(}x\mathrm{,}{\mathrm{refl}}_{x}\mathrm{)}$ as elements of ${\mathrm{\beta \x88\x91}}_{\mathrm{(}y\mathrm{:}A\mathrm{)}}\mathrm{(}x\mathrm{=}y\mathrm{)}$.
Title  1.12.1 Path Induction 

\metatable 