[proofplan]
Define the weak dependent sum of a type $B$ over the extended context $\Gamma.A$ to be the chosen left adjoint value $\Sigma_{\theta_A}B$ in the fiber over $\Gamma$. The adjunction $\Sigma_{\theta_A}\dashv\theta_A^*$ gives exactly the universal property of maps out of a dependent pair: a map from $\Sigma_{\theta_A}B$ into $C$ is equivalently a map from $B$ into the pullback $\theta_A^*C$. The unit and counit of the adjunction supply weak introduction, elimination, computation, and uniqueness. Finally, the assumed Beck-Chevalley isomorphism identifies the result of forming the dependent sum after substitution with the substitution of the already-formed dependent sum.
[/proofplan]
[step:Define the weak dependent sum using the chosen left adjoint]
Fix a context $\Gamma\in\mathcal C$, a type $A\in\typeE_\Gamma$, and a type $B\in\typeE_{\Gamma.A}$. Let
\begin{align*}
\theta_A:\Gamma.A\to\Gamma
\end{align*}
denote the display map associated to context extension by $A$. By hypothesis, the reindexing functor
\begin{align*}
\theta_A^*:\typeE_\Gamma\to\typeE_{\Gamma.A}
\end{align*}
has a chosen left adjoint
\begin{align*}
\Sigma_{\theta_A}:\typeE_{\Gamma.A}\to\typeE_\Gamma.
\end{align*}
Define
\begin{align*}
\Sigma_A B:=\Sigma_{\theta_A}B.
\end{align*}
This is a type in the fiber $\typeE_\Gamma$, so it is a type over the original context $\Gamma$.
[/step]
[step:Extract the dependent-pair universal property from the adjunction]
Let $C\in\typeE_\Gamma$ be any type over $\Gamma$. Since $\Sigma_{\theta_A}$ is left adjoint to $\theta_A^*$, there is a natural bijection
\begin{align*}
\Phi_{B,C}:\operatorname{Hom}_{\typeE_\Gamma}(\Sigma_{\theta_A}B,C)\to\operatorname{Hom}_{\typeE_{\Gamma.A}}(B,\theta_A^*C).
\end{align*}
For a morphism
\begin{align*}
h:\Sigma_{\theta_A}B\to C
\end{align*}
in $\typeE_\Gamma$, the corresponding morphism in $\typeE_{\Gamma.A}$ is
\begin{align*}
\Phi_{B,C}(h)=\theta_A^*h\circ\eta_B,
\end{align*}
where
\begin{align*}
\eta_B:B\to\theta_A^*\Sigma_{\theta_A}B
\end{align*}
is the unit of the adjunction at $B$.
Conversely, for a morphism
\begin{align*}
d:B\to\theta_A^*C
\end{align*}
in $\typeE_{\Gamma.A}$, its transpose is the morphism
\begin{align*}
\overline d:\Sigma_{\theta_A}B\to C
\end{align*}
defined by
\begin{align*}
\overline d:=\varepsilon_C\circ\Sigma_{\theta_A}d,
\end{align*}
where
\begin{align*}
\varepsilon_C:\Sigma_{\theta_A}\theta_A^*C\to C
\end{align*}
is the counit of the adjunction at $C$.
The triangle identities for the adjunction imply
\begin{align*}
\theta_A^*\overline d\circ\eta_B=d.
\end{align*}
They also imply uniqueness: if $h:\Sigma_{\theta_A}B\to C$ satisfies
\begin{align*}
\theta_A^*h\circ\eta_B=d,
\end{align*}
then $h=\overline d$. Thus maps out of $\Sigma_A B$ are exactly maps defined after pulling the target back to the extended context and giving a map from $B$ there. This is the weak dependent-pair elimination and uniqueness property.
[guided]
We want to show that $\Sigma_A B$ behaves like a dependent sum. In categorical terms, that means that to define a map out of $\Sigma_A B$ into a type $C$ over $\Gamma$, it should be equivalent to defining a map out of $B$ after the context has been extended by $A$.
The available structure is the adjunction
\begin{align*}
\Sigma_{\theta_A}\dashv\theta_A^*.
\end{align*}
Here
\begin{align*}
\Sigma_{\theta_A}:\typeE_{\Gamma.A}\to\typeE_\Gamma
\end{align*}
moves a type over the extended context $\Gamma.A$ back to a type over $\Gamma$, while
\begin{align*}
\theta_A^*:\typeE_\Gamma\to\typeE_{\Gamma.A}
\end{align*}
pulls a type over $\Gamma$ into the extended context. Applying the adjunction to the object $B\in\typeE_{\Gamma.A}$ and the object $C\in\typeE_\Gamma$ gives a natural bijection
\begin{align*}
\Phi_{B,C}:\operatorname{Hom}_{\typeE_\Gamma}(\Sigma_{\theta_A}B,C)\to\operatorname{Hom}_{\typeE_{\Gamma.A}}(B,\theta_A^*C).
\end{align*}
This bijection is precisely the weak elimination principle. A morphism
\begin{align*}
h:\Sigma_{\theta_A}B\to C
\end{align*}
is a map out of the proposed dependent sum. Its adjunct is obtained by first using the unit
\begin{align*}
\eta_B:B\to\theta_A^*\Sigma_{\theta_A}B
\end{align*}
and then pulling $h$ back along $\theta_A$, giving
\begin{align*}
\Phi_{B,C}(h)=\theta_A^*h\circ\eta_B.
\end{align*}
This says that a map out of the dependent sum determines a map from the unpacked dependent data $B$ to the pulled-back target $\theta_A^*C$.
Conversely, suppose we are given a morphism
\begin{align*}
d:B\to\theta_A^*C
\end{align*}
in the fiber over $\Gamma.A$. The adjunction transposes $d$ to a morphism
\begin{align*}
\overline d:\Sigma_{\theta_A}B\to C
\end{align*}
in the fiber over $\Gamma$. Explicitly, this transpose is
\begin{align*}
\overline d:=\varepsilon_C\circ\Sigma_{\theta_A}d,
\end{align*}
where
\begin{align*}
\varepsilon_C:\Sigma_{\theta_A}\theta_A^*C\to C
\end{align*}
is the counit of the adjunction.
The computation law is not an extra assumption. It is one of the triangle identities of the adjunction written in this notation. Substituting the definition of $\overline d$ into the adjunct operation gives
\begin{align*}
\theta_A^*\overline d\circ\eta_B=d.
\end{align*}
Thus eliminating the introduced dependent pair recovers the original map $d$ in the extended context.
The uniqueness law is also part of the adjunction. If another morphism
\begin{align*}
h:\Sigma_{\theta_A}B\to C
\end{align*}
satisfies
\begin{align*}
\theta_A^*h\circ\eta_B=d,
\end{align*}
then $h$ and $\overline d$ have the same image under the adjunction bijection $\Phi_{B,C}$. Since $\Phi_{B,C}$ is a bijection, $h=\overline d$. Therefore $\Sigma_A B=\Sigma_{\theta_A}B$ has the weak dependent-pair universal property.
[/guided]
[/step]
[step:Identify introduction and weak computation with the unit and triangle identities]
The morphism
\begin{align*}
\eta_B:B\to\theta_A^*\Sigma_A B
\end{align*}
is the weak pairing or introduction map. It lives in the fiber $\typeE_{\Gamma.A}$, so it represents the operation of forming a dependent pair after unpacking the base component $A$ and the dependent component $B$.
For every $C\in\typeE_\Gamma$ and every eliminator datum
\begin{align*}
d:B\to\theta_A^*C,
\end{align*}
the induced eliminator is its adjunct
\begin{align*}
\overline d:\Sigma_A B\to C.
\end{align*}
The equation
\begin{align*}
\theta_A^*\overline d\circ\eta_B=d
\end{align*}
is the weak computation rule, and the uniqueness of $\overline d$ among morphisms satisfying this equation is the weak uniqueness rule. Both statements follow from the two triangle identities for the adjunction
\begin{align*}
\Sigma_{\theta_A}\dashv\theta_A^*.
\end{align*}
[/step]
[step:Use Beck-Chevalley to prove stability under substitution]
Let
\begin{align*}
f:\Delta\to\Gamma
\end{align*}
be a context morphism. Pulling the display map $\theta_A:\Gamma.A\to\Gamma$ back along $f$ gives the display map
\begin{align*}
\theta_{f^*A}:\Delta.f^*A\to\Delta
\end{align*}
and the induced morphism
\begin{align*}
f_A:\Delta.f^*A\to\Gamma.A.
\end{align*}
By the Beck-Chevalley hypothesis, for every $B\in\typeE_{\Gamma.A}$ there is a natural isomorphism
\begin{align*}
\beta_{f,A,B}:\Sigma_{\theta_{f^*A}}(f_A^*B)\to f^*(\Sigma_{\theta_A}B)
\end{align*}
in $\typeE_\Delta$.
Using the definition of the weak dependent sum on both sides, this is the isomorphism
\begin{align*}
\beta_{f,A,B}:\Sigma_{f^*A}(f_A^*B)\to f^*(\Sigma_A B).
\end{align*}
Hence forming the dependent sum after substituting $f$ is naturally isomorphic to substituting $f$ after forming the dependent sum. If the Beck-Chevalley comparison is stated in the opposite direction by convention, the inverse isomorphism $\beta_{f,A,B}^{-1}$ gives the same stability assertion.
[/step]
[step:Conclude that the comprehension category has stable weak dependent sums]
For each context $\Gamma$, each $A\in\typeE_\Gamma$, and each $B\in\typeE_{\Gamma.A}$, the object
\begin{align*}
\Sigma_A B=\Sigma_{\theta_A}B
\end{align*}
is a type over $\Gamma$. The adjunction
\begin{align*}
\Sigma_{\theta_A}\dashv\theta_A^*
\end{align*}
gives the natural hom-set bijection
\begin{align*}
\operatorname{Hom}_{\typeE_\Gamma}(\Sigma_A B,C)\cong\operatorname{Hom}_{\typeE_{\Gamma.A}}(B,\theta_A^*C)
\end{align*}
for every $C\in\typeE_\Gamma$, together with the associated weak introduction, elimination, computation, and uniqueness structure. The Beck-Chevalley isomorphisms give the substitution stability
\begin{align*}
\Sigma_{f^*A}(f_A^*B)\cong f^*(\Sigma_A B)
\end{align*}
naturally in $B$ and in the substitution data. Therefore $\baseC$ supports substitution-stable weak dependent sum types along context extensions.
[/step]
