[proofplan]
Fix a context extension display map $\theta:\rho\to\tau$ and a type $B$ over the extended context $\rho$. We define the semantic dependent product of $B$ along $\theta$ to be the object $\Pi_{\theta}B$ in the fiber over $\tau$. The adjunction $\theta^{*}\dashv\Pi_{\theta}$ gives the transposition bijection that interprets lambda abstraction, while its counit gives application. The beta and eta laws are precisely the two triangle identities of the adjunction, and Beck-Chevalley says that this construction commutes with substitution of the base context.
[/proofplan]
[step:Define the dependent product type by the right adjoint]
Let $\theta:\rho\to\tau$ be a display map arising from context extension, and let $B\in\typeE_{\rho}$ be a type over the extended context $\rho$. By hypothesis, the reindexing functor
\begin{align*}
\theta^{*}:\typeE_{\tau}\to\typeE_{\rho}
\end{align*}
has a chosen right adjoint
\begin{align*}
\Pi_{\theta}:\typeE_{\rho}\to\typeE_{\tau}.
\end{align*}
Define the dependent function type of $B$ along $\theta$ to be
\begin{align*}
\Pi_{\theta}B\in\typeE_{\tau}.
\end{align*}
Thus the formation rule for dependent products is interpreted by applying the right adjoint $\Pi_{\theta}$ to the type $B$ over the extended context.
[guided]
A dependent function type is formed from a type $B$ living in an extended context. Categorically, the context extension is represented by a display map
\begin{align*}
\theta:\rho\to\tau.
\end{align*}
The fiber category $\typeE_{\rho}$ contains the types over the extended context $\rho$, and the fiber category $\typeE_{\tau}$ contains the types over the base context $\tau$.
The theorem assumes that the substitution functor along $\theta$,
\begin{align*}
\theta^{*}:\typeE_{\tau}\to\typeE_{\rho},
\end{align*}
has a right adjoint
\begin{align*}
\Pi_{\theta}:\typeE_{\rho}\to\typeE_{\tau}.
\end{align*}
Since $B$ is an object of $\typeE_{\rho}$, applying this right adjoint produces an object
\begin{align*}
\Pi_{\theta}B\in\typeE_{\tau}.
\end{align*}
This object is the categorical interpretation of the type-theoretic expression $\prod_{x:A}B(x)$, where $\theta$ is the context projection from $\tau,x:A$ to $\tau$. The reason the construction lands in $\typeE_{\tau}$ is exactly that a dependent product over the variable introduced by $\theta$ is again a type in the original context $\tau$.
[/guided]
[/step]
[step:Use the adjunction bijection to interpret lambda abstraction]
Let $C\in\typeE_{\tau}$ be any type over the base context. Since $\Pi_{\theta}$ is right adjoint to $\theta^{*}$, there is a natural bijection
\begin{align*}
\Phi_{C,B}:\operatorname{Hom}_{\typeE_{\rho}}(\theta^{*}C,B)\to\operatorname{Hom}_{\typeE_{\tau}}(C,\Pi_{\theta}B).
\end{align*}
For a morphism
\begin{align*}
b:\theta^{*}C\to B
\end{align*}
in $\typeE_{\rho}$, define its lambda abstraction to be its adjoint transpose
\begin{align*}
\lambda(b):=\Phi_{C,B}(b):C\to\Pi_{\theta}B.
\end{align*}
In particular, when $C$ is the terminal object $1_{\tau}$ of the fiber $\typeE_{\tau}$, a term of $B$ in the extended context is a morphism
\begin{align*}
b:\theta^{*}1_{\tau}\to B
\end{align*}
in $\typeE_{\rho}$, and its abstraction is the morphism
\begin{align*}
\lambda(b):1_{\tau}\to\Pi_{\theta}B.
\end{align*}
This is exactly the semantic introduction rule for dependent function types.
[/step]
[step:Use the counit to interpret application]
Let
\begin{align*}
\varepsilon_B:\theta^{*}\Pi_{\theta}B\to B
\end{align*}
denote the counit component of the adjunction $\theta^{*}\dashv\Pi_{\theta}$ at the object $B\in\typeE_{\rho}$. This morphism is the semantic evaluation map.
Given a morphism
\begin{align*}
f:C\to\Pi_{\theta}B
\end{align*}
in $\typeE_{\tau}$, define its application in the extended context by the composite
\begin{align*}
\operatorname{app}(f):=\varepsilon_B\circ\theta^{*}f:\theta^{*}C\to B.
\end{align*}
Here $\theta^{*}f:\theta^{*}C\to\theta^{*}\Pi_{\theta}B$ is obtained by functoriality of reindexing. Therefore the elimination rule for dependent function types is interpreted by reindexing a dependent function to the extended context and then evaluating it against the generic variable represented by the display map $\theta$.
[/step]
[step:Derive beta and eta from the triangle identities]
Let
\begin{align*}
\eta_C:C\to\Pi_{\theta}\theta^{*}C
\end{align*}
denote the unit component of the adjunction at $C\in\typeE_{\tau}$, and let
\begin{align*}
\varepsilon_B:\theta^{*}\Pi_{\theta}B\to B
\end{align*}
denote the counit component at $B\in\typeE_{\rho}$.
For a morphism
\begin{align*}
b:\theta^{*}C\to B,
\end{align*}
the adjoint transpose is
\begin{align*}
\lambda(b)=\Pi_{\theta}(b)\circ\eta_C.
\end{align*}
Applying the semantic application operation gives
\begin{align*}
\operatorname{app}(\lambda(b))=\varepsilon_B\circ\theta^{*}(\Pi_{\theta}(b)\circ\eta_C).
\end{align*}
By functoriality of $\theta^{*}$ and naturality of the counit, this equals
\begin{align*}
b\circ\varepsilon_{\theta^{*}C}\circ\theta^{*}\eta_C.
\end{align*}
The first triangle identity for the adjunction states that
\begin{align*}
\varepsilon_{\theta^{*}C}\circ\theta^{*}\eta_C=\operatorname{id}_{\theta^{*}C}.
\end{align*}
Hence
\begin{align*}
\operatorname{app}(\lambda(b))=b.
\end{align*}
This is the beta law.
Conversely, let
\begin{align*}
f:C\to\Pi_{\theta}B
\end{align*}
be a morphism in $\typeE_{\tau}$. Its application is
\begin{align*}
\operatorname{app}(f)=\varepsilon_B\circ\theta^{*}f.
\end{align*}
Taking the adjoint transpose gives
\begin{align*}
\lambda(\operatorname{app}(f))=\Pi_{\theta}(\varepsilon_B\circ\theta^{*}f)\circ\eta_C.
\end{align*}
By functoriality of $\Pi_{\theta}$ and naturality of the unit, this equals
\begin{align*}
\Pi_{\theta}(\varepsilon_B)\circ\eta_{\Pi_{\theta}B}\circ f.
\end{align*}
The second triangle identity for the adjunction states that
\begin{align*}
\Pi_{\theta}(\varepsilon_B)\circ\eta_{\Pi_{\theta}B}=\operatorname{id}_{\Pi_{\theta}B}.
\end{align*}
Therefore
\begin{align*}
\lambda(\operatorname{app}(f))=f.
\end{align*}
This is the eta law.
[guided]
The beta and eta laws are not additional structure here; they are the two triangle identities of the adjunction.
First take a morphism
\begin{align*}
b:\theta^{*}C\to B
\end{align*}
in the fiber $\typeE_{\rho}$. Its lambda abstraction is its adjoint transpose. Written using the unit
\begin{align*}
\eta_C:C\to\Pi_{\theta}\theta^{*}C,
\end{align*}
that transpose is
\begin{align*}
\lambda(b)=\Pi_{\theta}(b)\circ\eta_C.
\end{align*}
Now apply the semantic application operation, which means reindex along $\theta$ and then compose with the counit
\begin{align*}
\varepsilon_B:\theta^{*}\Pi_{\theta}B\to B.
\end{align*}
Thus
\begin{align*}
\operatorname{app}(\lambda(b))=\varepsilon_B\circ\theta^{*}(\Pi_{\theta}(b)\circ\eta_C).
\end{align*}
Functoriality of $\theta^{*}$ expands the reindexed composite, and naturality of $\varepsilon$ moves $b$ past the counit. The result is
\begin{align*}
\operatorname{app}(\lambda(b))=b\circ\varepsilon_{\theta^{*}C}\circ\theta^{*}\eta_C.
\end{align*}
The first triangle identity says
\begin{align*}
\varepsilon_{\theta^{*}C}\circ\theta^{*}\eta_C=\operatorname{id}_{\theta^{*}C}.
\end{align*}
Substituting this identity gives
\begin{align*}
\operatorname{app}(\lambda(b))=b.
\end{align*}
This is the categorical form of beta reduction: applying the function obtained by abstracting $b$ recovers $b$.
For eta, start with a morphism
\begin{align*}
f:C\to\Pi_{\theta}B
\end{align*}
in $\typeE_{\tau}$. Application gives
\begin{align*}
\operatorname{app}(f)=\varepsilon_B\circ\theta^{*}f.
\end{align*}
Now abstract this morphism again. By the formula for adjoint transposition,
\begin{align*}
\lambda(\operatorname{app}(f))=\Pi_{\theta}(\varepsilon_B\circ\theta^{*}f)\circ\eta_C.
\end{align*}
Functoriality of $\Pi_{\theta}$ and naturality of the unit identify this composite with
\begin{align*}
\lambda(\operatorname{app}(f))=\Pi_{\theta}(\varepsilon_B)\circ\eta_{\Pi_{\theta}B}\circ f.
\end{align*}
The second triangle identity says
\begin{align*}
\Pi_{\theta}(\varepsilon_B)\circ\eta_{\Pi_{\theta}B}=\operatorname{id}_{\Pi_{\theta}B}.
\end{align*}
Therefore
\begin{align*}
\lambda(\operatorname{app}(f))=f.
\end{align*}
This is the categorical form of the eta principle: a dependent function is recovered from its action on the generic argument.
[/guided]
[/step]
[step:Use Beck-Chevalley to obtain stability under substitution]
Let
\begin{align*}
\sigma:\tau'\to\tau
\end{align*}
be a context morphism, and form the pullback of the display map $\theta:\rho\to\tau$ along $\sigma$. Write
\begin{align*}
\rho':=\tau'\times_{\tau}\rho
\end{align*}
for the pulled-back context, write
\begin{align*}
\theta':\rho'\to\tau'
\end{align*}
for the pulled-back display map, and write
\begin{align*}
\sigma':\rho'\to\rho
\end{align*}
for the induced morphism over $\sigma$. The square with sides $\theta'$, $\theta$, $\sigma'$, and $\sigma$ is a pullback square obtained by substituting the display map $\theta$ along $\sigma$.
For a type $B\in\typeE_{\rho}$, the Beck-Chevalley condition gives the specified comparison isomorphism
\begin{align*}
\sigma^{*}(\Pi_{\theta}B)\cong\Pi_{\theta'}((\sigma')^{*}B)
\end{align*}
in $\typeE_{\tau'}$; in a strict split presentation, this comparison is an equality. Hence forming the dependent product and then substituting along $\sigma$ agrees with first substituting the family $B$ to the pulled-back extended context and then forming the dependent product along $\theta'$.
The same comparison isomorphism is natural in $B$ and is compatible with the adjunction units and counits. Therefore the transposition bijections used for lambda abstraction and the counit maps used for application are preserved by substitution. Consequently the formation, introduction, elimination, beta, and eta structures described above are stable under substitution of contexts.
[/step]
[step:Conclude that the comprehension category interprets dependent function types]
For every context extension display map $\theta:\rho\to\tau$ and every type $B\in\typeE_{\rho}$, we have constructed an object $\Pi_{\theta}B\in\typeE_{\tau}$. The adjunction bijection
\begin{align*}
\operatorname{Hom}_{\typeE_{\rho}}(\theta^{*}C,B)\cong\operatorname{Hom}_{\typeE_{\tau}}(C,\Pi_{\theta}B)
\end{align*}
interprets lambda abstraction, the counit
\begin{align*}
\varepsilon_B:\theta^{*}\Pi_{\theta}B\to B
\end{align*}
interprets application, the triangle identities give beta and eta, and Beck-Chevalley gives substitution stability. These are exactly the categorical semantic clauses for dependent function types in a comprehension category. Therefore the chosen right adjoints $\Pi_{\theta}$ interpret dependent function types.
[/step]
