Skip to main content
2 of 4
added 287 characters in body; added 8 characters in body
varkor
  • 10.7k
  • 29
  • 72

Categorically, the right adjoint $\Pi_f$ exists when $f$ is exponentiable. In the categorical semantics of type theory, exponentiable maps correspond to the display maps. 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$.

varkor
  • 10.7k
  • 29
  • 72