[proofplan]
We construct the action of $f$ on identity proofs by identity elimination. With $a : A$ fixed, the motive sends a point $x : A$ and a path $q : \operatorname{Id}_A(a,x)$ to the type $\operatorname{Id}_B(f(a),f(x))$. The reflexive case is supplied by $\operatorname{refl}_{f(a)}$, and the judgmental computation rule for identity elimination gives the stated reduction on $\operatorname{refl}_a$.
[/proofplan]
[step:Define the identity-elimination motive for paths starting at $a$]
Fix the types $A$ and $B$, the function $f : A \to B$, and the point $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 \operatorname{Id}_B(f(a),f(x)),
\end{align*}
for $x : A$ and $q : \operatorname{Id}_A(a,x)$.
In the reflexive case $x \coloneqq a$ and $q \coloneqq \operatorname{refl}_a$, the required type is
\begin{align*}
C(a,\operatorname{refl}_a) \equiv \operatorname{Id}_B(f(a),f(a)).
\end{align*}
Thus the reflexivity term
\begin{align*}
d \coloneqq \operatorname{refl}_{f(a)}
\end{align*}
has type $C(a,\operatorname{refl}_a)$.
[/step]
[step:Apply identity elimination to construct $\operatorname{ap}_f(p)$]
By the [path induction principle](/theorems/9633) [citetheorem:9633], applied to the motive $C$ and the base term $d : C(a,\operatorname{refl}_a)$, for every $b : A$ and every $p : \operatorname{Id}_A(a,b)$ there is a term
\begin{align*}
\operatorname{pathind}(d,a,b,p) : C(b,p).
\end{align*}
Since $C(b,p) \equiv \operatorname{Id}_B(f(a),f(b))$, define
\begin{align*}
\operatorname{ap}_f(p) \coloneqq \operatorname{pathind}(d,a,b,p).
\end{align*}
Therefore
\begin{align*}
\operatorname{ap}_f(p) : \operatorname{Id}_B(f(a),f(b)).
\end{align*}
[guided]
The goal is to turn a path in $A$ from $a$ to $b$ into a path in $B$ from $f(a)$ to $f(b)$. Since the only data relating $a$ and $b$ is the identity proof $p : \operatorname{Id}_A(a,b)$, the appropriate tool is identity elimination, or path induction [citetheorem:9633].
We use the motive
\begin{align*}
C(x,q) \coloneqq \operatorname{Id}_B(f(a),f(x)),
\end{align*}
where $x : A$ and $q : \operatorname{Id}_A(a,x)$. This motive asks: if $x$ is connected to $a$ by an identity proof, can we produce an identity proof between $f(a)$ and $f(x)$?
Identity elimination reduces this question to the reflexive case. When $x$ is $a$ and $q$ is $\operatorname{refl}_a$, the target type becomes
\begin{align*}
C(a,\operatorname{refl}_a) \equiv \operatorname{Id}_B(f(a),f(a)).
\end{align*}
This type is inhabited by reflexivity, so define
\begin{align*}
d \coloneqq \operatorname{refl}_{f(a)}.
\end{align*}
Thus $d : C(a,\operatorname{refl}_a)$.
Now the path induction principle [citetheorem:9633] applied to $C$ and $d$ gives, for every $b : A$ and $p : \operatorname{Id}_A(a,b)$, a term
\begin{align*}
\operatorname{pathind}(d,a,b,p) : C(b,p).
\end{align*}
By the definition of $C$, this is precisely a term of
\begin{align*}
\operatorname{Id}_B(f(a),f(b)).
\end{align*}
We therefore define the action of $f$ on the identity proof $p$ by
\begin{align*}
\operatorname{ap}_f(p) \coloneqq \operatorname{pathind}(d,a,b,p).
\end{align*}
This gives the required term
\begin{align*}
\operatorname{ap}_f(p) : \operatorname{Id}_B(f(a),f(b)).
\end{align*}
[/guided]
[/step]
[step:Compute the construction on reflexivity]
It remains to verify the displayed judgmental computation rule. By the judgmental computation rule for path induction, the eliminator reduces on the reflexivity constructor as
\begin{align*}
\operatorname{pathind}(d,a,a,\operatorname{refl}_a) \equiv d.
\end{align*}
Using the definitions of $\operatorname{ap}_f$ and $d$, this gives
\begin{align*}
\operatorname{ap}_f(\operatorname{refl}_a) \equiv \operatorname{refl}_{f(a)}.
\end{align*}
This is exactly the asserted computation rule, completing the proof.
[/step]
