Return to Answer

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 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".)

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 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".)

If $B$ does not depend on a type $A$, then the display map is the unique morphism $! \colon B \to 1$, as in your example. So your interpretation is correct when there is no type dependency, but you need to be more careful when dealing with dependent types.

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$.

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 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".)

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 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".)

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$.