[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.[/step]

[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: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*}[/step]

[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: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]