===== Dependent sum functor =====
==== Functor ====
| @#55CCEE: context     | @#55CCEE: ${\bf C}$ ... Cartesian closed category with all limits |
| @#BBDDEE: let         | @#BBDDEE: $\sum_f$ ... left adjoint to the pullback functor $f^*$, where $f$ is an arrow in ${\bf C}$ |
| @#55CCEE: context     | @#55CCEE: $!_X:X\to *$ ... terminal morphisms for $X\in{\bf C}$ |
| @#FF9944: definition  | @#FF9944: $\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$.

-----
=== Elaboration ===
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.

=== Equivalent definitions ===
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$.

== Proof ==

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$

=== Example ===
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$.

=== Reference ===
nLab: [[http://ncatlab.org/nlab/show/dependent+sum|dependent sum]]

Wikipedia: 
[[http://en.wikipedia.org/wiki/Adjoint_functors#Categorical_logic|Adjoint functors#Categorical logic]] 
(Here I made the left adjunction explicit in ${\bf{Set}}$.)

----
=== Element of ===
[[Functor]]
=== Requirements ===
[[Pullback functor]]
=== Related ===
[[Dependent product functor]]