# 1.12.2 Equivalence of path induction and based 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