===== Dependent product functor =====
==== Functor ====
| @#55CCEE: context     | @#55CCEE: ${\bf C}$ ... Cartesian closed category with all limits |
| @#BBDDEE: let         | @#BBDDEE: $\prod_f$ ... right 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: $\prod_X p := {\mathrm{dom}}\prod_{!_X} p$ |

>todo: fmap of $\prod_X$

Here $f^*$ is the pullback functor from ${\bf C}/Y$ to ${\bf C}/X$.

-----
=== Elaboration ===
We use $Y=*$ and so $\prod_{!_X} p$ is an object in ${{\bf C}/*}$ and then $\prod_X p$ is an object in ${\bf C}$. Note that the slice category ${{\bf C}/*}$ is equivalent to ${\bf C}$, by identifying terminal morphisms $!_B:B\to{*}$ with their domains $B$. We force this identification on the objects via the map ${\mathrm{dom}}$.

=== Discussion ===
Let $p:E\to X$ define a fibration. 

$$
\require{AMScd}

\begin{CD}          
E               
\\ 
@V{p}VV 
\\                
X
\end{CD}
$$

We want to characterize the space of sections $\prod_X p$. In terms of sets or any type theory, sections are like functions $s$ that fulfill $p\circ s=1_X$, except the fibres over points in $X$ may vary. For sets, the condition is $s(x)\in p^{-1}(x)$.

== Explanation starting from the exp-hom adjunction ==
A function space $Y^X$ can be characterized by the isomorphism $(A\to Y^X)\cong((A\times X)\to Y)$. 
Let us moreover identify $(A\times X)\to Y$ with the space of function from that $(A\times X)\to (Y\times X)$ with the additional requirement that the second component is mapped to itself, i.e. according to the scheme 
$\theta'(\langle a,x\rangle):=\langle \theta(a),x\rangle$.

Again, in diagrams: Functions in
$$
\require{AMScd}

\begin{CD}          
A @>>> Y^X               
\end{CD}
$$
are in bijection to functions in
$$
\require{AMScd}

\begin{CD}          
A\times X @>>> Y        
\end{CD}
$$
which which in turn also correspond to functions from $(A\times X)\to(Y\times X)$ that fulfill projection-condition expressed int the following diagram
$$
\require{AMScd}

\begin{CD}          
A\times X  @>>> Y\times X                 
\\ 
@V{\pi_2}VV      @V{\pi_2}VV
\\                
X @= X
\end{CD}
$$
Essentially, we get the section space $\prod_X p$ that we are after, if we just replace the projection $\pi_2:X\times Y\to X$ with the more general $p$. The function space we obtain need the not just be $Y^X$, but can be some more general so called section space. A section of this space must in general then not map an $x$ in $X$ to $x$ in $Y\times X$, but instead merely map it somehow into $p^{-1}(x)$. 

So for an auxiliary object $A$, consider the projection $\pi_2:(A\times X)\to X$, formally defined as the arrow obtained by pulling back $!_A:A\to*$ along $!_X:X\to*$, i.e. $\pi_2:=!_X{}^*!_A$. This definition is appearent from the commuting square defining the product: 

$$
\require{AMScd}

\begin{CD}          
A\times X  @>>>      A                   
\\ 
@V{\pi_2}VV      @V{!_A}VV   
\\                
X  @>>{!_X}>      *
\end{CD}
$$

The slice category ${\bf{C}}/X$ is the category with objects being ${\bf{C}}$-arrows into $X$ and arrows given by commuting triangles for those. As $\pi_2:(A\times X)\to X$ and $p$ are objects in ${\bf{C}}/X$, one such triangle is 

$$
\require{AMScd}

\begin{CD}          
A\times X @>>> E    
\\ 
@V{\pi_2}VV      @V{p}VV
\\                
X @= X
\end{CD}
$$

The point is that an arrow $\theta:\pi_2\to p$ in ${\bf{C}}/X$ exactly fulfills our condition by definition. A right adjoint $\prod_{!_X}$ to the pullback functor $!_X^*$ is defined as an isomorphism 

$${\bf{C}}/X[!_X{}^*!_A,p]\cong{\bf{C}}/*[!_A,\prod_{!_X}p]$$

I.e. this provides an isomorphism of the above triangle to

$$
\require{AMScd}

\begin{CD}          
A @>>> \prod_Xp    
\\ 
@V{!_A}VV      @V{\prod_{!_X}p}VV
\\                
* @= *
\end{CD}
$$

The domain $\prod_Xp\in{\bf{C}}$ is usually called the dependent product.

The case $E=Y\times X$ and $p=\pi_2$ gives again $\prod_X\pi_2=Y^X$.

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

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]]