# 1.12.2 Equivalence of path induction and based path induction

The two induction principles for the identity type introduced above are equivalent. It is easy to see that path induction follows from the based path induction principle. Indeed, let us assume the premises of path induction:

 $\displaystyle C$ $\displaystyle:\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},$ $\displaystyle c$ $\displaystyle:\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}).$

Now, given an element $x:A$, we can instantiate both of the above, obtaining

 $\displaystyle C^{\prime}$ $\displaystyle:\mathchoice{\prod_{y:A}\,}{\mathchoice{{\textstyle\prod_{(y:A)}}% }{\prod_{(y:A)}}{\prod_{(y:A)}}{\prod_{(y:A)}}}{\mathchoice{{\textstyle\prod_{% (y:A)}}}{\prod_{(y:A)}}{\prod_{(y:A)}}{\prod_{(y:A)}}}{\mathchoice{{\textstyle% \prod_{(y:A)}}}{\prod_{(y:A)}}{\prod_{(y:A)}}{\prod_{(y:A)}}}(x=_{A}y)\to% \mathcal{U},$ $\displaystyle C^{\prime}$ $\displaystyle:\!\!\equiv C(x),$ $\displaystyle c^{\prime}$ $\displaystyle:C^{\prime}(x,\mathsf{refl}_{x}),$ $\displaystyle c^{\prime}$ $\displaystyle:\!\!\equiv c(x).$

Clearly, $C^{\prime}$ and $c^{\prime}$ match the premises of based path induction and hence we can construct

 $g:\mathchoice{\prod_{(y:A)}\,}{\mathchoice{{\textstyle\prod_{(y:A)}}}{\prod_{(% y:A)}}{\prod_{(y:A)}}{\prod_{(y:A)}}}{\mathchoice{{\textstyle\prod_{(y:A)}}}{% \prod_{(y:A)}}{\prod_{(y:A)}}{\prod_{(y:A)}}}{\mathchoice{{\textstyle\prod_{(y% :A)}}}{\prod_{(y:A)}}{\prod_{(y:A)}}{\prod_{(y:A)}}}\mathchoice{\prod_{(p:x=y)% }\,}{\mathchoice{{\textstyle\prod_{(p:x=y)}}}{\prod_{(p:x=y)}}{\prod_{(p:x=y)}% }{\prod_{(p:x=y)}}}{\mathchoice{{\textstyle\prod_{(p:x=y)}}}{\prod_{(p:x=y)}}{% \prod_{(p:x=y)}}{\prod_{(p:x=y)}}}{\mathchoice{{\textstyle\prod_{(p:x=y)}}}{% \prod_{(p:x=y)}}{\prod_{(p:x=y)}}{\prod_{(p:x=y)}}}C^{\prime}(y,p)$

with the defining equality

 $g(x,\mathsf{refl}_{x}):\!\!\equiv c^{\prime}.$

Now we observe that $g$βs codomain is equal to $C(x,y,p)$. Thus, discharging our assumption $x:A$, we can derive 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)$

with the required judgmental equality $f(x,x,\mathsf{refl}_{x})\equiv g(x,\mathsf{refl}_{x}):\!\!\equiv c^{\prime}:\!% \!\equiv c(x)$.

Another proof of this fact is to observe that any such $f$ can be obtained as an instance of $\mathsf{ind}_{=_{A}}^{\prime}$ so it suffices to define $\mathsf{ind}_{=_{A}}$ in terms of $\mathsf{ind}_{=_{A}}^{\prime}$ as

 $\mathsf{ind}_{=_{A}}(C,c,x,y,p):\!\!\equiv\mathsf{ind}_{=_{A}}^{\prime}(x,C(x)% ,c(x),y,p).$

The other direction is a bit trickier; it is not clear how we can use a particular instance of path induction to derive a particular instance of based path induction. What we can do instead is to construct one instance of path induction which shows all possible instantiations of based path induction at once. Define

 $\displaystyle D$ $\displaystyle:\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},$ $\displaystyle D(x,y,p)$ $\displaystyle:\!\!\equiv\mathchoice{\prod_{C:\mathchoice{\prod_{z:A}\,}{% \mathchoice{{\textstyle\prod_{(z:A)}}}{\prod_{(z:A)}}{\prod_{(z:A)}}{\prod_{(z% :A)}}}{\mathchoice{{\textstyle\prod_{(z:A)}}}{\prod_{(z:A)}}{\prod_{(z:A)}}{% \prod_{(z:A)}}}{\mathchoice{{\textstyle\prod_{(z:A)}}}{\prod_{(z:A)}}{\prod_{(% z:A)}}{\prod_{(z:A)}}}(x=_{A}z)\to\mathcal{U}}\,}{\mathchoice{{\textstyle\prod% _{(C:\mathchoice{\prod_{z:A}\,}{\mathchoice{{\textstyle\prod_{(z:A)}}}{\prod_{% (z:A)}}{\prod_{(z:A)}}{\prod_{(z:A)}}}{\mathchoice{{\textstyle\prod_{(z:A)}}}{% \prod_{(z:A)}}{\prod_{(z:A)}}{\prod_{(z:A)}}}{\mathchoice{{\textstyle\prod_{(z% :A)}}}{\prod_{(z:A)}}{\prod_{(z:A)}}{\prod_{(z:A)}}}(x=_{A}z)\to\mathcal{U})}}% }{\prod_{(C:\mathchoice{\prod_{z:A}\,}{\mathchoice{{\textstyle\prod_{(z:A)}}}{% \prod_{(z:A)}}{\prod_{(z:A)}}{\prod_{(z:A)}}}{\mathchoice{{\textstyle\prod_{(z% :A)}}}{\prod_{(z:A)}}{\prod_{(z:A)}}{\prod_{(z:A)}}}{\mathchoice{{\textstyle% \prod_{(z:A)}}}{\prod_{(z:A)}}{\prod_{(z:A)}}{\prod_{(z:A)}}}(x=_{A}z)\to% \mathcal{U})}}{\prod_{(C:\mathchoice{\prod_{z:A}\,}{\mathchoice{{\textstyle% \prod_{(z:A)}}}{\prod_{(z:A)}}{\prod_{(z:A)}}{\prod_{(z:A)}}}{\mathchoice{{% \textstyle\prod_{(z:A)}}}{\prod_{(z:A)}}{\prod_{(z:A)}}{\prod_{(z:A)}}}{% \mathchoice{{\textstyle\prod_{(z:A)}}}{\prod_{(z:A)}}{\prod_{(z:A)}}{\prod_{(z% :A)}}}(x=_{A}z)\to\mathcal{U})}}{\prod_{(C:\mathchoice{\prod_{z:A}\,}{% \mathchoice{{\textstyle\prod_{(z:A)}}}{\prod_{(z:A)}}{\prod_{(z:A)}}{\prod_{(z% :A)}}}{\mathchoice{{\textstyle\prod_{(z:A)}}}{\prod_{(z:A)}}{\prod_{(z:A)}}{% \prod_{(z:A)}}}{\mathchoice{{\textstyle\prod_{(z:A)}}}{\prod_{(z:A)}}{\prod_{(% z:A)}}{\prod_{(z:A)}}}(x=_{A}z)\to\mathcal{U})}}}{\mathchoice{{\textstyle\prod% _{(C:\mathchoice{\prod_{z:A}\,}{\mathchoice{{\textstyle\prod_{(z:A)}}}{\prod_{% (z:A)}}{\prod_{(z:A)}}{\prod_{(z:A)}}}{\mathchoice{{\textstyle\prod_{(z:A)}}}{% \prod_{(z:A)}}{\prod_{(z:A)}}{\prod_{(z:A)}}}{\mathchoice{{\textstyle\prod_{(z% :A)}}}{\prod_{(z:A)}}{\prod_{(z:A)}}{\prod_{(z:A)}}}(x=_{A}z)\to\mathcal{U})}}% }{\prod_{(C:\mathchoice{\prod_{z:A}\,}{\mathchoice{{\textstyle\prod_{(z:A)}}}{% \prod_{(z:A)}}{\prod_{(z:A)}}{\prod_{(z:A)}}}{\mathchoice{{\textstyle\prod_{(z% :A)}}}{\prod_{(z:A)}}{\prod_{(z:A)}}{\prod_{(z:A)}}}{\mathchoice{{\textstyle% \prod_{(z:A)}}}{\prod_{(z:A)}}{\prod_{(z:A)}}{\prod_{(z:A)}}}(x=_{A}z)\to% \mathcal{U})}}{\prod_{(C:\mathchoice{\prod_{z:A}\,}{\mathchoice{{\textstyle% \prod_{(z:A)}}}{\prod_{(z:A)}}{\prod_{(z:A)}}{\prod_{(z:A)}}}{\mathchoice{{% \textstyle\prod_{(z:A)}}}{\prod_{(z:A)}}{\prod_{(z:A)}}{\prod_{(z:A)}}}{% \mathchoice{{\textstyle\prod_{(z:A)}}}{\prod_{(z:A)}}{\prod_{(z:A)}}{\prod_{(z% :A)}}}(x=_{A}z)\to\mathcal{U})}}{\prod_{(C:\mathchoice{\prod_{z:A}\,}{% \mathchoice{{\textstyle\prod_{(z:A)}}}{\prod_{(z:A)}}{\prod_{(z:A)}}{\prod_{(z% :A)}}}{\mathchoice{{\textstyle\prod_{(z:A)}}}{\prod_{(z:A)}}{\prod_{(z:A)}}{% \prod_{(z:A)}}}{\mathchoice{{\textstyle\prod_{(z:A)}}}{\prod_{(z:A)}}{\prod_{(% z:A)}}{\prod_{(z:A)}}}(x=_{A}z)\to\mathcal{U})}}}{\mathchoice{{\textstyle\prod% _{(C:\mathchoice{\prod_{z:A}\,}{\mathchoice{{\textstyle\prod_{(z:A)}}}{\prod_{% (z:A)}}{\prod_{(z:A)}}{\prod_{(z:A)}}}{\mathchoice{{\textstyle\prod_{(z:A)}}}{% \prod_{(z:A)}}{\prod_{(z:A)}}{\prod_{(z:A)}}}{\mathchoice{{\textstyle\prod_{(z% :A)}}}{\prod_{(z:A)}}{\prod_{(z:A)}}{\prod_{(z:A)}}}(x=_{A}z)\to\mathcal{U})}}% }{\prod_{(C:\mathchoice{\prod_{z:A}\,}{\mathchoice{{\textstyle\prod_{(z:A)}}}{% \prod_{(z:A)}}{\prod_{(z:A)}}{\prod_{(z:A)}}}{\mathchoice{{\textstyle\prod_{(z% :A)}}}{\prod_{(z:A)}}{\prod_{(z:A)}}{\prod_{(z:A)}}}{\mathchoice{{\textstyle% \prod_{(z:A)}}}{\prod_{(z:A)}}{\prod_{(z:A)}}{\prod_{(z:A)}}}(x=_{A}z)\to% \mathcal{U})}}{\prod_{(C:\mathchoice{\prod_{z:A}\,}{\mathchoice{{\textstyle% \prod_{(z:A)}}}{\prod_{(z:A)}}{\prod_{(z:A)}}{\prod_{(z:A)}}}{\mathchoice{{% \textstyle\prod_{(z:A)}}}{\prod_{(z:A)}}{\prod_{(z:A)}}{\prod_{(z:A)}}}{% \mathchoice{{\textstyle\prod_{(z:A)}}}{\prod_{(z:A)}}{\prod_{(z:A)}}{\prod_{(z% :A)}}}(x=_{A}z)\to\mathcal{U})}}{\prod_{(C:\mathchoice{\prod_{z:A}\,}{% \mathchoice{{\textstyle\prod_{(z:A)}}}{\prod_{(z:A)}}{\prod_{(z:A)}}{\prod_{(z% :A)}}}{\mathchoice{{\textstyle\prod_{(z:A)}}}{\prod_{(z:A)}}{\prod_{(z:A)}}{% \prod_{(z:A)}}}{\mathchoice{{\textstyle\prod_{(z:A)}}}{\prod_{(z:A)}}{\prod_{(% z:A)}}{\prod_{(z:A)}}}(x=_{A}z)\to\mathcal{U})}}}C(x,\mathsf{refl}_{x})\to C(y% ,p).$

Then we can construct the function

 $\displaystyle d$ $\displaystyle:\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)}}}D(x,x,\mathsf{% refl}_{x}),$ $\displaystyle d$ $\displaystyle:\!\!\equiv{\lambda}x.\,{\lambda}C.\,{\lambda}(c\,{:}\,C(x,% \mathsf{refl}_{x})).\,c$

and hence using path induction obtain

 $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)}}}D(x,y% ,p)$

with $f(x,x,\mathsf{refl}_{x}):\!\!\equiv d(x)$. Unfolding the definition of $D$, we can expand the type of $f$:

 $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)}}}% \mathchoice{\prod_{(C:\mathchoice{\prod_{z:A}\,}{\mathchoice{{\textstyle\prod_% {(z:A)}}}{\prod_{(z:A)}}{\prod_{(z:A)}}{\prod_{(z:A)}}}{\mathchoice{{% \textstyle\prod_{(z:A)}}}{\prod_{(z:A)}}{\prod_{(z:A)}}{\prod_{(z:A)}}}{% \mathchoice{{\textstyle\prod_{(z:A)}}}{\prod_{(z:A)}}{\prod_{(z:A)}}{\prod_{(z% :A)}}}(x=_{A}z)\to\mathcal{U})}\,}{\mathchoice{{\textstyle\prod_{(C:% \mathchoice{\prod_{z:A}\,}{\mathchoice{{\textstyle\prod_{(z:A)}}}{\prod_{(z:A)% }}{\prod_{(z:A)}}{\prod_{(z:A)}}}{\mathchoice{{\textstyle\prod_{(z:A)}}}{\prod% _{(z:A)}}{\prod_{(z:A)}}{\prod_{(z:A)}}}{\mathchoice{{\textstyle\prod_{(z:A)}}% }{\prod_{(z:A)}}{\prod_{(z:A)}}{\prod_{(z:A)}}}(x=_{A}z)\to\mathcal{U})}}}{% \prod_{(C:\mathchoice{\prod_{z:A}\,}{\mathchoice{{\textstyle\prod_{(z:A)}}}{% \prod_{(z:A)}}{\prod_{(z:A)}}{\prod_{(z:A)}}}{\mathchoice{{\textstyle\prod_{(z% :A)}}}{\prod_{(z:A)}}{\prod_{(z:A)}}{\prod_{(z:A)}}}{\mathchoice{{\textstyle% \prod_{(z:A)}}}{\prod_{(z:A)}}{\prod_{(z:A)}}{\prod_{(z:A)}}}(x=_{A}z)\to% \mathcal{U})}}{\prod_{(C:\mathchoice{\prod_{z:A}\,}{\mathchoice{{\textstyle% \prod_{(z:A)}}}{\prod_{(z:A)}}{\prod_{(z:A)}}{\prod_{(z:A)}}}{\mathchoice{{% \textstyle\prod_{(z:A)}}}{\prod_{(z:A)}}{\prod_{(z:A)}}{\prod_{(z:A)}}}{% \mathchoice{{\textstyle\prod_{(z:A)}}}{\prod_{(z:A)}}{\prod_{(z:A)}}{\prod_{(z% :A)}}}(x=_{A}z)\to\mathcal{U})}}{\prod_{(C:\mathchoice{\prod_{z:A}\,}{% \mathchoice{{\textstyle\prod_{(z:A)}}}{\prod_{(z:A)}}{\prod_{(z:A)}}{\prod_{(z% :A)}}}{\mathchoice{{\textstyle\prod_{(z:A)}}}{\prod_{(z:A)}}{\prod_{(z:A)}}{% \prod_{(z:A)}}}{\mathchoice{{\textstyle\prod_{(z:A)}}}{\prod_{(z:A)}}{\prod_{(% z:A)}}{\prod_{(z:A)}}}(x=_{A}z)\to\mathcal{U})}}}{\mathchoice{{\textstyle\prod% _{(C:\mathchoice{\prod_{z:A}\,}{\mathchoice{{\textstyle\prod_{(z:A)}}}{\prod_{% (z:A)}}{\prod_{(z:A)}}{\prod_{(z:A)}}}{\mathchoice{{\textstyle\prod_{(z:A)}}}{% \prod_{(z:A)}}{\prod_{(z:A)}}{\prod_{(z:A)}}}{\mathchoice{{\textstyle\prod_{(z% :A)}}}{\prod_{(z:A)}}{\prod_{(z:A)}}{\prod_{(z:A)}}}(x=_{A}z)\to\mathcal{U})}}% }{\prod_{(C:\mathchoice{\prod_{z:A}\,}{\mathchoice{{\textstyle\prod_{(z:A)}}}{% \prod_{(z:A)}}{\prod_{(z:A)}}{\prod_{(z:A)}}}{\mathchoice{{\textstyle\prod_{(z% :A)}}}{\prod_{(z:A)}}{\prod_{(z:A)}}{\prod_{(z:A)}}}{\mathchoice{{\textstyle% \prod_{(z:A)}}}{\prod_{(z:A)}}{\prod_{(z:A)}}{\prod_{(z:A)}}}(x=_{A}z)\to% \mathcal{U})}}{\prod_{(C:\mathchoice{\prod_{z:A}\,}{\mathchoice{{\textstyle% \prod_{(z:A)}}}{\prod_{(z:A)}}{\prod_{(z:A)}}{\prod_{(z:A)}}}{\mathchoice{{% \textstyle\prod_{(z:A)}}}{\prod_{(z:A)}}{\prod_{(z:A)}}{\prod_{(z:A)}}}{% \mathchoice{{\textstyle\prod_{(z:A)}}}{\prod_{(z:A)}}{\prod_{(z:A)}}{\prod_{(z% :A)}}}(x=_{A}z)\to\mathcal{U})}}{\prod_{(C:\mathchoice{\prod_{z:A}\,}{% \mathchoice{{\textstyle\prod_{(z:A)}}}{\prod_{(z:A)}}{\prod_{(z:A)}}{\prod_{(z% :A)}}}{\mathchoice{{\textstyle\prod_{(z:A)}}}{\prod_{(z:A)}}{\prod_{(z:A)}}{% \prod_{(z:A)}}}{\mathchoice{{\textstyle\prod_{(z:A)}}}{\prod_{(z:A)}}{\prod_{(% z:A)}}{\prod_{(z:A)}}}(x=_{A}z)\to\mathcal{U})}}}{\mathchoice{{\textstyle\prod% _{(C:\mathchoice{\prod_{z:A}\,}{\mathchoice{{\textstyle\prod_{(z:A)}}}{\prod_{% (z:A)}}{\prod_{(z:A)}}{\prod_{(z:A)}}}{\mathchoice{{\textstyle\prod_{(z:A)}}}{% \prod_{(z:A)}}{\prod_{(z:A)}}{\prod_{(z:A)}}}{\mathchoice{{\textstyle\prod_{(z% :A)}}}{\prod_{(z:A)}}{\prod_{(z:A)}}{\prod_{(z:A)}}}(x=_{A}z)\to\mathcal{U})}}% }{\prod_{(C:\mathchoice{\prod_{z:A}\,}{\mathchoice{{\textstyle\prod_{(z:A)}}}{% \prod_{(z:A)}}{\prod_{(z:A)}}{\prod_{(z:A)}}}{\mathchoice{{\textstyle\prod_{(z% :A)}}}{\prod_{(z:A)}}{\prod_{(z:A)}}{\prod_{(z:A)}}}{\mathchoice{{\textstyle% \prod_{(z:A)}}}{\prod_{(z:A)}}{\prod_{(z:A)}}{\prod_{(z:A)}}}(x=_{A}z)\to% \mathcal{U})}}{\prod_{(C:\mathchoice{\prod_{z:A}\,}{\mathchoice{{\textstyle% \prod_{(z:A)}}}{\prod_{(z:A)}}{\prod_{(z:A)}}{\prod_{(z:A)}}}{\mathchoice{{% \textstyle\prod_{(z:A)}}}{\prod_{(z:A)}}{\prod_{(z:A)}}{\prod_{(z:A)}}}{% \mathchoice{{\textstyle\prod_{(z:A)}}}{\prod_{(z:A)}}{\prod_{(z:A)}}{\prod_{(z% :A)}}}(x=_{A}z)\to\mathcal{U})}}{\prod_{(C:\mathchoice{\prod_{z:A}\,}{% \mathchoice{{\textstyle\prod_{(z:A)}}}{\prod_{(z:A)}}{\prod_{(z:A)}}{\prod_{(z% :A)}}}{\mathchoice{{\textstyle\prod_{(z:A)}}}{\prod_{(z:A)}}{\prod_{(z:A)}}{% \prod_{(z:A)}}}{\mathchoice{{\textstyle\prod_{(z:A)}}}{\prod_{(z:A)}}{\prod_{(% z:A)}}{\prod_{(z:A)}}}(x=_{A}z)\to\mathcal{U})}}}C(x,\mathsf{refl}_{x})\to C(y% ,p).$

Now given $x:A$ and $p:a=_{A}x$, we can derive the conclusion of based path induction:

 $f(a,x,p,C,c):C(x,p).$

Notice that we also obtain the correct definitional equality.

Another proof is to observe that any use of based path induction is an instance of $\mathsf{ind}_{=_{A}}^{\prime}$ and to define

 \mathsf{ind}_{=_{A}}^{\prime}(a,C,c,x,p):\!\!\equiv\mathsf{ind}_{=_{A}}\begin{% aligned} \displaystyle\big{(}&\displaystyle\big{(}{\lambda}x,y.\,{\lambda}p.\,% \mathchoice{{\textstyle\prod_{(C:\mathchoice{\prod_{z:A}\,}{\mathchoice{{% \textstyle\prod_{(z:A)}}}{\prod_{(z:A)}}{\prod_{(z:A)}}{\prod_{(z:A)}}}{% \mathchoice{{\textstyle\prod_{(z:A)}}}{\prod_{(z:A)}}{\prod_{(z:A)}}{\prod_{(z% :A)}}}{\mathchoice{{\textstyle\prod_{(z:A)}}}{\prod_{(z:A)}}{\prod_{(z:A)}}{% \prod_{(z:A)}}}(x=_{A}z)\to\mathcal{U})}}}{\prod_{(C:\mathchoice{\prod_{z:A}\,% }{\mathchoice{{\textstyle\prod_{(z:A)}}}{\prod_{(z:A)}}{\prod_{(z:A)}}{\prod_{% (z:A)}}}{\mathchoice{{\textstyle\prod_{(z:A)}}}{\prod_{(z:A)}}{\prod_{(z:A)}}{% \prod_{(z:A)}}}{\mathchoice{{\textstyle\prod_{(z:A)}}}{\prod_{(z:A)}}{\prod_{(% z:A)}}{\prod_{(z:A)}}}(x=_{A}z)\to\mathcal{U})}}{\prod_{(C:\mathchoice{\prod_{% z:A}\,}{\mathchoice{{\textstyle\prod_{(z:A)}}}{\prod_{(z:A)}}{\prod_{(z:A)}}{% \prod_{(z:A)}}}{\mathchoice{{\textstyle\prod_{(z:A)}}}{\prod_{(z:A)}}{\prod_{(% z:A)}}{\prod_{(z:A)}}}{\mathchoice{{\textstyle\prod_{(z:A)}}}{\prod_{(z:A)}}{% \prod_{(z:A)}}{\prod_{(z:A)}}}(x=_{A}z)\to\mathcal{U})}}{\prod_{(C:\mathchoice% {\prod_{z:A}\,}{\mathchoice{{\textstyle\prod_{(z:A)}}}{\prod_{(z:A)}}{\prod_{(% z:A)}}{\prod_{(z:A)}}}{\mathchoice{{\textstyle\prod_{(z:A)}}}{\prod_{(z:A)}}{% \prod_{(z:A)}}{\prod_{(z:A)}}}{\mathchoice{{\textstyle\prod_{(z:A)}}}{\prod_{(% z:A)}}{\prod_{(z:A)}}{\prod_{(z:A)}}}(x=_{A}z)\to\mathcal{U})}}C(x,\mathsf{% refl}_{x})\to C(y,p)\big{)},\\ &\displaystyle({\lambda}x.\,{\lambda}C.\,{\lambda}d.\,d),a,x,p,C,c\big{)}\end{aligned}

Note that the construction given above uses universes. That is, if we want to model $\mathsf{ind}_{=_{A}}^{\prime}$ with $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}_{i}$, we need to use $\mathsf{ind}_{=_{A}}$ with

 $D:\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}_{i+1}$

since $D$ quantifies over all $C$ of the given type. While this is compatible with our definition of universes, it is also possible to derive $\mathsf{ind}_{=_{A}}^{\prime}$ without using universes: we can show that $\mathsf{ind}_{=_{A}}$ entails Lemma 1 (http://planetmath.org/23typefamiliesarefibrations#Thmlem1),Lemma 3.11.8 (http://planetmath.org/311contractibility#Thmprelem5), and that these two principles imply $\mathsf{ind}_{=_{A}}^{\prime}$ directly. We leave the details to the reader as http://planetmath.org/node/87560Exercise 1.7.

We can use either of the foregoing formulations of identity types to establish that equality is an equivalence relation, that every function preserves equality and that every family respects equality. We leave the details to the next chapter, where this will be derived and explained in the context of homotopy type theory.

 Title 1.12.2 Equivalence of path induction and based path induction \metatable