[proofplan]
We define $\operatorname{happly}(p)$ by identity elimination on the path $p$ between dependent functions. The motive says that a function $h:\prod_{x:A}B(x)$ equal to $f$ is pointwise equal to $f$ at every argument. Path induction reduces the construction to the reflexivity case, where the required pointwise equality is the dependent function sending $x:A$ to $\operatorname{refl}_{f(x)}$.
[/proofplan]
[step:Choose the path-induction motive for pointwise equality]
Let
\begin{align*}
F := \prod_{x:A}B(x)
\end{align*}
denote the dependent function type. Define the type family
\begin{align*}
D:\prod_{h:F}\operatorname{Id}_{F}(f,h)\to\mathsf{Type}
\end{align*}
by
\begin{align*}
D(h,q) := \prod_{x:A}\operatorname{Id}_{B(x)}(f(x),h(x)),
\end{align*}
where $h:F$ and $q:\operatorname{Id}_{F}(f,h)$. This is well-typed because, for each $x:A$, both $f(x)$ and $h(x)$ are terms of the same type $B(x)$.
[guided]
Let
\begin{align*}
F := \prod_{x:A}B(x)
\end{align*}
be the type whose elements are dependent functions assigning to each $x:A$ a term of $B(x)$. We want to eliminate a path
\begin{align*}
p:\operatorname{Id}_{F}(f,g).
\end{align*}
To use path induction, we must specify what we want to prove for an arbitrary endpoint $h:F$ and an arbitrary path from $f$ to that endpoint. Define
\begin{align*}
D:\prod_{h:F}\operatorname{Id}_{F}(f,h)\to\mathsf{Type}
\end{align*}
by
\begin{align*}
D(h,q) := \prod_{x:A}\operatorname{Id}_{B(x)}(f(x),h(x)).
\end{align*}
Thus $D(h,q)$ says: if $h$ is a dependent function path-equal to $f$, then $h$ is pointwise equal to $f$. The variable $q$ is included because path induction eliminates over both the endpoint and the identity proof, although the displayed formula for $D(h,q)$ does not depend computationally on $q$.
For each $x:A$, the terms $f(x)$ and $h(x)$ both lie in $B(x)$, since $f,h:\prod_{x:A}B(x)$. Therefore the identity type
\begin{align*}
\operatorname{Id}_{B(x)}(f(x),h(x))
\end{align*}
is well-formed, and so the dependent product defining $D(h,q)$ is also well-formed.
[/guided]
[/step]
[step:Construct the reflexivity case by pointwise reflexivity]
In the reflexivity case, the endpoint is $f$ and the path is
\begin{align*}
\operatorname{refl}_{f}:\operatorname{Id}_{F}(f,f).
\end{align*}
Define
\begin{align*}
r:\prod_{x:A}\operatorname{Id}_{B(x)}(f(x),f(x))
\end{align*}
by
\begin{align*}
r(x):=\operatorname{refl}_{f(x)}.
\end{align*}
Thus
\begin{align*}
r:D(f,\operatorname{refl}_{f}).
\end{align*}
[/step]
[step:Apply path induction to define $\operatorname{happly}$]
By the [path induction principle](/theorems/9633) [citetheorem:9633] applied to the type $F$, the base point $f:F$, the family $D$, and the reflexivity-case term $r:D(f,\operatorname{refl}_{f})$, for every $h:F$ and every
\begin{align*}
q:\operatorname{Id}_{F}(f,h)
\end{align*}
there is a term
\begin{align*}
\operatorname{pathind}(r,h,q):D(h,q).
\end{align*}
Taking $h:=g$ and $q:=p$, define
\begin{align*}
\operatorname{happly}(p):=\operatorname{pathind}(r,g,p).
\end{align*}
Since $D(g,p)$ is
\begin{align*}
\prod_{x:A}\operatorname{Id}_{B(x)}(f(x),g(x)),
\end{align*}
this gives the required dependent function.
[/step]
