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

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