todo: fmap of $\prod_X$

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

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

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

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

nLab: Dependent product

Wikipedia: Adjoint functors#Categorical logic (Here I made the left adjunction explicit in ${\bf{Set}}$.)

Functor

Pullback functor