Categorically, the right adjoint $\Pi_f$ exists when $f$ is [exponentiable](https://ncatlab.org/nlab/show/exponential+object). In the categorical semantics of type theory, exponentiable maps correspond to the [display maps](https://ncatlab.org/nlab/show/display+map). There are several ways one can think of display maps, but a simple way is to view a display map $f \colon C \to B$ as representing a type $C$ that depends on $B$. This means that whenever we have a context containing a variable of type $C$, we can form a term of type $B$. Type theoretically, we might write this as $b : B, c : C(b) \vdash b \colon B$ (or possibly leaving $b : B$ in the context implicit).

Supposing that $B$ is not a dependent type, the base change functor $f^*$ therefore sends a morphism $t \colon \Gamma \to B$, understood as a term $\Gamma \vdash t : B$, to the projection morphism $f^* t \colon \Gamma \times_B C \to C$ from the pullback, which is understood to represent the term $\Gamma, c : C(t) \vdash c : C(t)$. (This is the mantra "pullback is substitution", or more specifically, "pullback is term-in-type substitution".)

More generally, if $B$ is itself a dependent type (i.e. there is some display map $B \to A$), a term $\Gamma \vdash t : B$ is represented by a morphism $t \colon \Gamma \to \Gamma \times_A B$ in the slice category $\mathscr C/\Gamma$.