I am trying to understand topic about base change. https://ncatlab.org/nlab/show/base+change https://ncatlab.org/nlab/show/essential+geometric+morphism
Given a morphism $f:X\rightarrow Y$ in topos $C$. It is clear how to define functors $f^*:C/Y\rightarrow C/X$ (pullback along f) and $f_!:C/X \rightarrow C/Y$ (precomposition with f). But I do not understand how to define $f_*:C/X \rightarrow C/Y$ which is right adjoint to $f^*$.
How topos induces $f_*$?
p.s. I also appreciate clarifying connection beween the $f_!$ (the synonym: $\Sigma_f$) and dependent sum $\Sigma(x:X).P(x)$ from computer science. (must be somewhere in Sheaves in geometry and logic: a first introduction to topos theory Saunders MacLane, Ieke Moerdijk. I'll search in it when it is available to me.)
Since $C/X$ is equivalent to the slice category of $C/Y$ given by the object $f:X \to Y$, we can assume without loss of generality that $Y=1$.
The general mechanism of interpreting dependent types in categories is to view an arrow $p:E \to X$ as an "$X$-indexed family of objects"; to each generalized element $x : U \to X$, the dependent type $E(x)$ is the pullback
$$ \begin{matrix} E(x) &\to& E \\ \downarrow & & \ \ \downarrow {\Tiny p} \\ U &\xrightarrow{x}& X \end{matrix} $$
Note that, if you wanted to, in a topos you can transpose this to $X \xrightarrow{\{ \cdot \}} P(X) \xrightarrow{p^{-1}} P(E)$, to more literally get a map from $X$ to subsets of $E$.
Since $E$ is the total set containing everything in the family, the dependent sum simply forgets the indexing, so $f_!(p) = E$.
The right adjoint $f_*$ is the dependent product; in the internal language, it is the set of all sections of $p$ (i.e. functions with $s(x) \in E(x)$, but $a \in E(x)$ means $p(a) = x$): $$ f_*(p) = \{ s : X \to E \mid p \circ s = 1_X \} $$ which you can express as a pullback diagram $$ \begin{matrix} f_*(p) &\to& E^X \\ \downarrow & & \quad \downarrow {\Tiny p \circ -} \\ 1 &\xrightarrow{`1_X{}'}& X^X \end{matrix} $$