[proofplan]
We define transport by path induction on the identity proof $p:\operatorname{Id}_A(a,b)$. The motive says that a path from $a$ to a point $x:A$ should produce a function from the fibre $B(a)$ to the fibre $B(x)$. In the reflexive case this function is the identity map on $B(a)$, and the computation rule for identity elimination gives the displayed judgemental equality.
[/proofplan]
[step:Choose the motive for identity elimination]
Fix a type $A$, a dependent type family $B:A\to\mathsf{Type}$, and an element $a:A$. Define the dependent motive
\begin{align*}
C:\prod_{x:A}\operatorname{Id}_A(a,x)\to\mathsf{Type}
\end{align*}
by
\begin{align*}
C(x,q)\coloneqq B(a)\to B(x)
\end{align*}
for $x:A$ and $q:\operatorname{Id}_A(a,x)$.
For the reflexive path $\operatorname{refl}_a:\operatorname{Id}_A(a,a)$, we have
\begin{align*}
C(a,\operatorname{refl}_a)\equiv B(a)\to B(a).
\end{align*}
Let
\begin{align*}
\operatorname{id}_{B(a)}:B(a)\to B(a)
\end{align*}
denote the identity function on the fibre $B(a)$.
[guided]
The goal is to turn a path $q:\operatorname{Id}_A(a,x)$ into a map between fibres. Since the target fibre depends on the endpoint $x$, the correct object to define by identity elimination is not directly an element of $B(x)$, but a function
\begin{align*}
B(a)\to B(x).
\end{align*}
Thus we define the motive
\begin{align*}
C:\prod_{x:A}\operatorname{Id}_A(a,x)\to\mathsf{Type}
\end{align*}
by
\begin{align*}
C(x,q)\coloneqq B(a)\to B(x).
\end{align*}
Here $x:A$ is the variable endpoint of the path and $q:\operatorname{Id}_A(a,x)$ is the path from the fixed base point $a$ to $x$.
Identity elimination requires a term in the reflexive case. When $x$ is $a$ and $q$ is $\operatorname{refl}_a$, the motive becomes
\begin{align*}
C(a,\operatorname{refl}_a)\equiv B(a)\to B(a).
\end{align*}
The required function is therefore the identity map
\begin{align*}
\operatorname{id}_{B(a)}:B(a)\to B(a).
\end{align*}
This is the defining choice that makes transport along a reflexivity path compute judgementally to the original element.
[/guided]
[/step]
[step:Apply path induction to define the transport function]
By the identity eliminator, equivalently the [[Path Induction Principle](/theorems/9633)][citetheorem:9633], applied to the motive $C$ and to the reflexive-case term $\operatorname{id}_{B(a)}:C(a,\operatorname{refl}_a)$, for every $b:A$ and every $p:\operatorname{Id}_A(a,b)$ there is a term
\begin{align*}
J_C(\operatorname{id}_{B(a)},b,p):C(b,p).
\end{align*}
Using the definition of $C$, this term has type
\begin{align*}
J_C(\operatorname{id}_{B(a)},b,p):B(a)\to B(b).
\end{align*}
Define
\begin{align*}
\operatorname{transport}^{B}(p)\coloneqq J_C(\operatorname{id}_{B(a)},b,p).
\end{align*}
Thus
\begin{align*}
\operatorname{transport}^{B}(p):B(a)\to B(b).
\end{align*}
In particular, for each $u:B(a)$, application gives the canonical transported term
\begin{align*}
\operatorname{transport}^{B}(p)(u):B(b).
\end{align*}
[/step]
[step:Use the computation rule in the reflexive case]
The computation rule for identity elimination says that, when the path argument is $\operatorname{refl}_a$, the eliminator returns the specified reflexive-case term judgementally:
\begin{align*}
J_C(\operatorname{id}_{B(a)},a,\operatorname{refl}_a)\equiv \operatorname{id}_{B(a)}.
\end{align*}
Therefore
\begin{align*}
\operatorname{transport}^{B}(\operatorname{refl}_a)\equiv \operatorname{id}_{B(a)}.
\end{align*}
Applying both sides to an arbitrary $u:B(a)$ and using the defining computation rule for the identity function gives
\begin{align*}
\operatorname{transport}^{B}(\operatorname{refl}_a)(u)\equiv u.
\end{align*}
This proves both the existence of the transport map along an arbitrary identity path and its judgemental computation rule along reflexivity.
[/step]
