| context | ${\bf C}$ … Cartesian closed category with all limits |
| let | $\sum_f$ … left adjoint to the pullback functor $f^*$, where $f$ is an arrow in ${\bf C}$ |
| context | $!_X:X\to *$ … terminal morphisms for $X\in{\bf C}$ |
| definition | $\sum_X p := {\mathrm{dom}}\sum_{!_X} p$ |
todo: fmap of $\sum_X$
Here $f^*$ is the pullback functor from ${\bf C}/Y$ to ${\bf C}/X$.
The dependent sum functor is dually defined as the left adjoint to the pullback functor along the terminal morphism $!_X:X\to *$.
The dependent product functor is defined as its right adjoint and the Elaboration section there is relevant.
Because the pullback concerns arrows into ${\mathrm{dom}}\ f^*g$, the object map of the functor $\sum_fp$ always reduces to $f\circ p$ and the dependent sum is hence given by
$\sum_X p := {\mathrm{dom}}\ p$.
Fix a $f:{\bf C}[X,Y]$. The left adjoint $\sum_f:{\bf C}/X\longrightarrow{\bf C}/Y$ to the pullback functor $f^*:{\bf C}/Y\longrightarrow{\bf C}/X$ is characterized by an isomorphism
$${\bf C}/X[p,f^*g]\cong{\bf C}/Y[\sum_f p,g].$$
The claim is that $\sum_fp:=f\circ p$ works.
Take any $p,g$ with codomain $X$ resp. $Y$, and consider the following diagram: $$ \require{AMScd} \begin{CD} {\mathrm{dom}}\ p @. ({\mathrm{dom}}\ g)\times_Y X @>{\pi_1}>> {\mathrm{dom}}\ g @. {\mathrm{dom}}\ p \\ @V{p}VV @V{f^*g}VV @V{g}VV @V{f\circ p}VV \\ X @= X @>>{f}> Y @= Y \end{CD} $$
Any $\theta:{\bf C}/X[p,f^*g]$ (closing the left side of the diagram) corresponds to a ${\bf C}$-arrow. As the central square commutes, we have can consider $\pi_1\circ\theta$ to be an arrow in $\cong{\bf C}/Y[f\circ p,g]$ and we're done.
Conversely, any ${\bf C}/Y$-arrow from $f\circ p$ to $g$ (closing the right side of the diagram) corresponds to a ${\bf C}$-arrow from ${\mathrm{dom}}\ p$ to ${\mathrm{dom}}\ g$. By the defining property of the pullback, it induces a unique arrow from ${\mathrm{dom}}\ p$ to the pullback object $({\mathrm{dom}}\ g)\times_Y X$ that makes everything commute. This is equivalently a ${\bf C}/X$ arrow from $p$ to $f^*g$.
todo: why is this actually an iso?
Lastly, $\sum_fp:=f\circ p$ implies ${\mathrm{dom}}\sum_fp={\mathrm{dom}}\ p$ and in particular
$\sum_X p := {\mathrm{dom}}\sum_{!_X} p = {\mathrm{dom}}\ p$
The pullback functor $!_X{}^*$ maps arrows to $*$ to arrows to $X$. If $!_Y:Y\to *$ is the terminal morphism, then $!_X{}^*!_Y:Y\times X\to X$ is the right projection out of the product and so
$\sum_X (!_X{}^*!_Y) = Y\times X$.
nLab: dependent sum
Wikipedia: Adjoint functors#Categorical logic (Here I made the left adjunction explicit in ${\bf{Set}}$.)