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 B \to A$ as representing a type $B$ that depends on $A$. This means that whenever we have a context containing a variable of type $B$, we can form a term of type $A$. Type theoretically, we might write this as $a : A, b : B(a) \vdash a \colon A$ (or possibly leaving $a : A$ in the context implicit).

The base change functor $f^*$ therefore sends a morphism $t \colon \Gamma \to A$, understood as a term $\Gamma \vdash t : A$, to the projection morphism $f^* t \colon \Gamma \times_A B \to B$ from the pullback, which is understood to represent the term $\Gamma, b : B(t) \vdash b : B(t)$. (This is the mantra "pullback is substitution", or more specifically, "pullback is term-in-type substitution".)