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}}$.)

Functor

Pullback functor

Dependent product functor