The nLab article on the Syntactic category states that if our dependent type theory has dependent product types, then its syntactic category $C(T)$ is locally cartesian closed.
I see that this is true when we just consider pullbacks along canonical projections (a.k.a display maps). That is, I see that, given dependent products, any pullback functor along a projection context morphism $\Gamma, x:A \to \Gamma$ in $C(T)$ has a right adjoint.
But for pullback functors along arbitrary context morphisms, I'm not sure how to verify the existence of right adjoints. In fact, I'm not sure what general pullback squares look like in $C(T)$. Could someone explain how the proof of this goes or point me to a reference that spells it out?
Update: A different nLab article (https://ncatlab.org/nlab/show/pullback#in_type_theory) states that an arbitrary pullback $P$ is given by $$P = \sum_{a : A} \sum_{b : B} (f(a) = g(b)),$$ which suggests that $C(T)$ must also have dependent sums to be locally cartesian closed. This seems to go against the first article. Any ideas?