[proofplan]
We prove the principle by deriving it from the identity type eliminator $J$. The key move is to fix the left endpoint $x:A$ and view the given family $D(x,y,p)$ as a family only in the right endpoint $y:A$ and the path $p:\operatorname{Id}_A(x,y)$. The reflexivity datum required by $J$ is then exactly the supplied term $d(x):D(x,x,\operatorname{refl}_x)$. Since the construction is made for an arbitrary $x:A$, it is uniform in the left endpoint, and the computation rule follows from the computation rule for $J$.
[/proofplan]
[step:Fix the left endpoint and form the based identity family]
Let $x:A$ be arbitrary. Define the dependent type family
\begin{align*}
C_x(y,p)\coloneqq D(x,y,p)
\end{align*}
in the context
\begin{align*}
y:A,\ p:\operatorname{Id}_A(x,y).
\end{align*}
This is well formed because $D$ is given in the context
\begin{align*}
x:A,\ y:A,\ p:\operatorname{Id}_A(x,y),
\end{align*}
and the variable $x:A$ has been fixed.
[guided]
We begin by isolating the part of the identity proof that $J$ eliminates. The identity eliminator $J$ is usually applied after fixing one endpoint of the identity type. Therefore let $x:A$ be an arbitrary but fixed element.
With this $x$ fixed, the original family
\begin{align*}
D(x,y,p)\ \mathsf{type}
\end{align*}
depends only on a variable $y:A$ and a path
\begin{align*}
p:\operatorname{Id}_A(x,y).
\end{align*}
So we define a based family
\begin{align*}
C_x(y,p)\coloneqq D(x,y,p)
\end{align*}
in the context
\begin{align*}
y:A,\ p:\operatorname{Id}_A(x,y).
\end{align*}
This definition is legitimate because substituting the fixed variable $x:A$ into the first argument of the already well-formed family $D$ leaves a well-formed family over the remaining variables $y$ and $p$.
[/guided]
[/step]
[step:Use the reflexivity datum as the base case for $J$]
The identity eliminator $J$ applied to the family $C_x$ requires a term of type
\begin{align*}
C_x(x,\operatorname{refl}_x).
\end{align*}
By the definition of $C_x$, this type is
\begin{align*}
D(x,x,\operatorname{refl}_x).
\end{align*}
The hypothesis supplies exactly such a term, namely
\begin{align*}
d(x):D(x,x,\operatorname{refl}_x).
\end{align*}
Thus $d(x)$ is admissible as the reflexivity case for $J$ applied to $C_x$.
[/step]
[step:Define the path induction term by the identity eliminator]
For arbitrary $y:A$ and $p:\operatorname{Id}_A(x,y)$, apply the identity type eliminator $J$ to the family $C_x$ with base term $d(x)$. Define
\begin{align*}
\operatorname{pathind}(d,x,y,p)\coloneqq J_{C_x}(d(x),y,p).
\end{align*}
The conclusion of $J$ gives
\begin{align*}
J_{C_x}(d(x),y,p):C_x(y,p).
\end{align*}
By the definition of $C_x$, this is precisely
\begin{align*}
\operatorname{pathind}(d,x,y,p):D(x,y,p).
\end{align*}
[guided]
Now we use the identity eliminator. For the fixed endpoint $x:A$, the eliminator $J$ says that to construct an element of $C_x(y,p)$ for every $y:A$ and every $p:\operatorname{Id}_A(x,y)$, it is enough to construct an element of the reflexive case
\begin{align*}
C_x(x,\operatorname{refl}_x).
\end{align*}
The previous step verified that the given term $d(x)$ has exactly this type.
Therefore, for arbitrary $y:A$ and $p:\operatorname{Id}_A(x,y)$, define
\begin{align*}
\operatorname{pathind}(d,x,y,p)\coloneqq J_{C_x}(d(x),y,p).
\end{align*}
By the formation and elimination rule for $J$, this term has type
\begin{align*}
C_x(y,p).
\end{align*}
Finally, since $C_x(y,p)$ was defined to be $D(x,y,p)$, the same term has type
\begin{align*}
D(x,y,p).
\end{align*}
This is the desired induction term for the fixed left endpoint $x$.
[/guided]
[/step]
[step:Conclude uniformity in the left endpoint and inherit the computation rule]
The construction above was made with $x:A$ arbitrary. Hence it defines, uniformly in $x$, a term
\begin{align*}
\operatorname{pathind}(d,x,y,p):D(x,y,p)
\end{align*}
for all $x,y:A$ and all $p:\operatorname{Id}_A(x,y)$.
In the reflexive case, the computation rule for $J$ gives
\begin{align*}
J_{C_x}(d(x),x,\operatorname{refl}_x)\equiv d(x):C_x(x,\operatorname{refl}_x).
\end{align*}
Using again the definition $C_x(x,\operatorname{refl}_x)\coloneqq D(x,x,\operatorname{refl}_x)$, this becomes
\begin{align*}
\operatorname{pathind}(d,x,x,\operatorname{refl}_x)\equiv d(x):D(x,x,\operatorname{refl}_x).
\end{align*}
Thus the required term exists for every identity proof, and it satisfies the stated reflexivity computation rule.
[/step]
