[proofplan]
We unpack the set-valued family model by representing a type family over a context $Y$ as a map $p:E\to Y$ and a term as a section of this map. A substitution $f:X\to Y$ changes the base context, so the correct family over $X$ is the pullback of $p$ along $f$. We then compute the fibers of this pullback and check directly that a section $s:Y\to E$ pulls back to the section $x\mapsto (x,s(f(x)))$ over $X$.
[/proofplan]
[step:Form the pullback family over the substituted context]
Let $X$ and $Y$ be the sets interpreting the two contexts, let $f:X\to Y$ be the function interpreting the context morphism, and let $p:E\to Y$ be the function interpreting the type family over $Y$. Define
\begin{align*}
f^\ast E:=\{(x,e)\in X\times E:p(e)=f(x)\}.
\end{align*}
Define the projection map
\begin{align*}
p_f:f^\ast E\to X
\end{align*}
by
\begin{align*}
p_f(x,e)=x.
\end{align*}
This is well-defined because every element of $f^\ast E$ is, by definition, an ordered pair $(x,e)$ with $x\in X$ and $e\in E$ satisfying $p(e)=f(x)$. Thus $p_f:f^\ast E\to X$ is a family of sets over the substituted context $X$.
[/step]
[step:Identify each substituted fiber with the original fiber over the substituted point]
Fix $x\in X$. The fiber of $p_f:f^\ast E\to X$ over $x$ is
\begin{align*}
p_f^{-1}(\{x\})=\{(x',e)\in f^\ast E:x'=x\}.
\end{align*}
Using the defining condition for membership in $f^\ast E$, this becomes
\begin{align*}
p_f^{-1}(\{x\})=\{(x,e)\in X\times E:p(e)=f(x)\}.
\end{align*}
Define
\begin{align*}
\Phi_x:p_f^{-1}(\{x\})\to p^{-1}(\{f(x)\})
\end{align*}
by $\Phi_x(x,e)=e$. Define
\begin{align*}
\Psi_x:p^{-1}(\{f(x)\})\to p_f^{-1}(\{x\})
\end{align*}
by $\Psi_x(e)=(x,e)$. If $e\in p^{-1}(\{f(x)\})$, then $p(e)=f(x)$, so $(x,e)\in f^\ast E$ and $\Psi_x(e)$ is well-defined. The composites satisfy $\Phi_x(\Psi_x(e))=e$ for all $e\in p^{-1}(\{f(x)\})$ and $\Psi_x(\Phi_x(x,e))=(x,e)$ for all $(x,e)\in p_f^{-1}(\{x\})$. Hence the fiber of the substituted family over $x$ is canonically identified with the original fiber over $f(x)$.
[guided]
The purpose of the pullback is to make the family live over the new context $X$ while preserving the old fibers. To see this precisely, fix an element $x\in X$. The elements of the fiber of $p_f:f^\ast E\to X$ over $x$ are exactly those elements of $f^\ast E$ whose first coordinate is $x$:
\begin{align*}
p_f^{-1}(\{x\})=\{(x',e)\in f^\ast E:x'=x\}.
\end{align*}
Now substitute the definition of $f^\ast E$. An ordered pair $(x',e)$ lies in $f^\ast E$ exactly when $p(e)=f(x')$. Imposing $x'=x$ gives
\begin{align*}
p_f^{-1}(\{x\})=\{(x,e)\in X\times E:p(e)=f(x)\}.
\end{align*}
Thus choosing an element in the new fiber over $x$ is the same as choosing an element $e\in E$ whose old base point is $f(x)$.
We make that equivalence into explicit maps. Define
\begin{align*}
\Phi_x:p_f^{-1}(\{x\})\to p^{-1}(\{f(x)\})
\end{align*}
by $\Phi_x(x,e)=e$. This is well-defined because membership of $(x,e)$ in $f^\ast E$ includes the condition $p(e)=f(x)$. Conversely, define
\begin{align*}
\Psi_x:p^{-1}(\{f(x)\})\to p_f^{-1}(\{x\})
\end{align*}
by $\Psi_x(e)=(x,e)$. This is well-defined because if $e\in p^{-1}(\{f(x)\})$, then $p(e)=f(x)$, which is exactly the pullback condition needed for $(x,e)\in f^\ast E$.
Finally, the two maps undo each other:
\begin{align*}
\Phi_x(\Psi_x(e))=e
\end{align*}
for every $e\in p^{-1}(\{f(x)\})$, and
\begin{align*}
\Psi_x(\Phi_x(x,e))=(x,e)
\end{align*}
for every $(x,e)\in p_f^{-1}(\{x\})$. Therefore the substituted family has, over $x$, precisely the old fiber over $f(x)$. This is the set-valued meaning of substituting the expression $f(x)$ into a type family over $Y$.
[/guided]
[/step]
[step:Pull back a section to interpret substitution of a term]
Let $s:Y\to E$ be a section of $p:E\to Y$, so
\begin{align*}
p\circ s=\operatorname{id}_Y.
\end{align*}
Define
\begin{align*}
f^\ast s:X\to f^\ast E
\end{align*}
by
\begin{align*}
f^\ast s(x)=(x,s(f(x))).
\end{align*}
For each $x\in X$, the section condition for $s$ gives
\begin{align*}
p(s(f(x)))=f(x).
\end{align*}
Therefore $(x,s(f(x)))\in f^\ast E$, so $f^\ast s$ is well-defined as a map from $X$ to $f^\ast E$.
[/step]
[step:Verify that the pulled-back term is a section]
For every $x\in X$, using the definition of $p_f$ and the definition of $f^\ast s$, we compute
\begin{align*}
(p_f\circ f^\ast s)(x)=p_f(x,s(f(x)))=x.
\end{align*}
Hence
\begin{align*}
p_f\circ f^\ast s=\operatorname{id}_X.
\end{align*}
Thus $f^\ast s:X\to f^\ast E$ is a section of the pullback family $p_f:f^\ast E\to X$. Consequently, in the set-valued family model, substitution of a type family is interpreted by pullback along the context morphism, and substitution of a term is interpreted by pulling back its section.
[/step]
