Base change. How to induce functor $f_*$ 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.)
 A: 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} $$
