Constructing dependent product (right adjoint to pullback) in a locally cartesian closed category

Question

I've been trying to find a proof that the pullback functors in a locally cartesian closed category have right adjoints (used to model the notion of indexed product inside a category (rather than indexed by a set), or, equivalently, dependent products in models of dependent type theories).

I found a proof in Awodey's book, but I found it utterly incomprehensible (probably due to not having read the rest of the book and therefore missing something considred obvious by that point). Does anyone know of other references for this theorem (would it be worth the effort trying to understand Seely's original paper on models of dependent type theory in locally cartesian closed categories)?

EDIT: I found a neat proof in Sheaves in Geometry and Logic where it is observed that one can add the assumption that the morphism $f : I \to J$ one takes pullbacks along is to a terminal object. First one notes that since a slice of a slice is isomorphic to a slice one can conclude that a slice of locally cartesian closed category is itself locally cartesian closed, with a terminal object given by the identity morphism of the object the slice is taken over.

Now $f$ can be considered a morphism from "itself" $I \; \xrightarrow {\; f} J$ to $J \; \xrightarrow {\textrm{Id}_J} J$ in the slice category $\mathcal{C}/J$. Given that one knows the right adjoint to exist in the case of a terminal object one can thus conclude, since $\textrm{Id}_J$ is terminal in $\mathcal{C}/J$, that pullback along $f$ as a functor $(\mathcal C/J)/\textrm{Id_J} \to (\mathcal C / J)/f$ has a right adjoint. This functor can now be made a functor $\mathcal C /J \to \mathcal C/I$ by noticing that $(\mathcal C/J)/\textrm{Id_J} $ and $(\mathcal C / J)/f$ are isomorphic (essentially by identity) to $\mathcal C/J$ and $\mathcal C / I$, respectively.

Answer 1

This is Awodey's proof, but hopefully it's clearer. The essential idea is to exploit the product–exponential adjunction in the slice category to get the pullback–dependent product adjunction in the whole category. After all, what is an element of $\prod_{j \in J} Y_j$ but a function $t : J \to \sum_{j \in J} Y_j$ such that $t (j) \in Y_j$?

Let $\mathcal{C}$ be a cartesian and locally cartesian closed category, in the sense that $\mathcal{C}$ has a terminal object $1$ and every slice category $\mathcal{C}_{/ A}$ is cartesian closed. Let $f : A \to B$ be a morphism in $\mathcal{C}$ – then it is also an object in $\mathcal{C}_{/ B}$ – and let $h : Y \to A$ be an object in $\mathcal{C}_{/ A}$. Observe that $\mathcal{C}$ has pullbacks: after all, the pullback of $q$ along $f$ is just the product $q \mathbin{\times_B} f : Y \mathbin{\times_B} A \to B$ in the slice category $\mathcal{C}_{/ B}$.

Now, let $q = f \circ h$. (As an object of $\mathcal{C}_{/ B}$, this is $\Sigma_f h$.) Since $\mathcal{C}_{/ B}$ is cartesian closed, we may exponentiate $q : Y \to B$ by $f : A \to B$ to obtain a morphism (in $\mathcal{C}$) $q^f : Y^f \to B$ such that there is an adjunction $$\textrm{Hom}_B(p \mathbin{\times_B} f, q) \cong \textrm{Hom}_B(p, q^f)$$ with counit $\epsilon_q : Y^f \mathbin{\times_B} A \to Y$. (Thus, we see that $Y^f$ is something like a "fibred" exponential object.) But $(-)^f : \mathcal{C}_{/ B} \to \mathcal{C}_{/ B}$ is a functor and we have a morphism $h : q \to f$ in $\mathcal{C}_{/ B}$, so we obtain a morphism $h^f : q^f \to f^f$ in $\mathcal{C}_{/ B}$. Moreover, $\textrm{id}_B \mathbin{\times_B} f \cong f$, so by the product–exponential adjunction $$\textrm{Hom}_B(f, f) \cong \textrm{Hom}_B(\textrm{id}_B, f^f)$$ In particular, $\textrm{id}_f : f \to f$ is mapped to some $s : \textrm{id}_B \to f^f$ (i.e. a morphism $s : B \to A^f$ in $\mathcal{C}$ such that $f^f \circ s = \textrm{id}_B$). Now, take the pullback (in $\mathcal{C}$) of $h^f$ along $s$ to obtain $\Pi_f h : \Pi_f Y \to B$.

Finally, we we show that there is a bijection $$\textrm{Hom}_A (f^* p, h) \cong \textrm{Hom}_B (p, \Pi_f h)$$ which is natural in $p : X \to B$. The left hand side can be identified with morphisms $u : p \times_B f \to q$ in $\mathcal{C}_{/ B}$ satisfying $h \circ u = f^* p$, where $f^* p : p \times_B f \to f$ is the projection. The right hand side can be identified with morphisms $v : p \to q^f$ such that $h^f \circ v = s \circ p$. It is not hard to see that the product–exponential adjunction in $\mathcal{C}_{/ B}$ restricts to a bijection between these two sets, so we are done.

Answer 2

This seems to be one of those situations where instead of trying to follow someone else's proof and someone else's notation, it's easier just to sit down and work out the proof by oneself, by considering first the case $\mathcal{C} = Set$ just to get one's bearing on what the construction should be, and then following one's nose.

So I'm not sure the following will help, but for anyone trying to follow: taking $\mathcal{C} = Set$ and a function $f: X \to Y$, the functor $\prod_f: Set/X \to Set/Y$ should intuitively take an object $p: E \to X$ to the object in $Set/Y$ whose fiber over an element $y \in Y$ is given by the formula

$$\prod_f(E \stackrel{p}{\to} X)_y := \prod_{f(x) = y} p^{-1}(x)$$

where the object on the right is the set of partial sections of $p$ over the subset $f^{-1}(y)$. Pulling back $p$ along the subset $f^{-1}(y) \hookrightarrow Y$, this is the set of sections $s$ of the obvious map $(f \circ p)^{-1}(y) \to f^{-1}(y)$ given by restriction of $p$; this set of sections is a pullback

$$\begin{array}{&&} P_y & \to & (f \circ p)^{-1}(y))^{f^{-1}(y)} \\ \downarrow & & \downarrow p^{f^{-1}(y)} \\ 1 & \stackrel{[id]}{\to} & f^{-1}(y)^{f^{-1}(y)} \end{array} $$

where $[id]$ here names the identity arrow $f^{-1}(y) \to f^{-1}(y)$. Collecting the fibers over all the $y$ together, we are led to an evident pullback diagram in $Set/Y$

$$\begin{array}{&&} (P \to Y) & \to & (E \stackrel{f \circ p}{\to} Y)^{(X \stackrel{f}{\to} Y)} \\ \downarrow & & \downarrow p^{(X \stackrel{f}{\to} Y)} \\ (Y \stackrel{1_Y}{\to} Y) & \stackrel{I}{\to} & (X \stackrel{f}{\to} Y)^{(X \stackrel{f}{\to} Y)} \end{array}$$

where all the exponentials are computed in $Set/Y$. Generalizing now from $Set$ to any $\mathcal{C}$ whose slices are cartesian closed, we assert this pullback gives the correct formula for $\prod_f (E \stackrel{p}{\to} X)$.

The proof this is correct is easy: a map from $(Q \stackrel{q}{\to} Y)$ into this pullback is tantamount to a commutative diagram

$$\begin{array}{&&} (Q \stackrel{q}{\to} Y) & \stackrel{\phi}{\to} & (E \stackrel{f \circ p}{\to} Y)^{(X \stackrel{f}{\to} Y)} \\ \pi \downarrow & & \downarrow p^{(X \stackrel{f}{\to} Y)} \\ (Y \stackrel{1_Y}{\to} Y) & \stackrel{I}{\to} & (X \stackrel{f}{\to} Y)^{(X \stackrel{f}{\to} Y)} \end{array}$$

which by the $\times-\hom$ adjunction in $\mathcal{C}/Y$ is tantamount to a commutative diagram in $\mathcal{C}/Y$

$$\begin{array}{&&} (Q \stackrel{q}{\to} Y) \times (X \stackrel{f}{\to} Y) & \stackrel{\psi}{\to} & (E \stackrel{f \circ p}{\to} Y) \\ \pi \times id_f \downarrow & & \downarrow p \\ (Y \stackrel{1_Y}{\to} Y) \times (X \stackrel{f}{\to} Y) & \stackrel{proj}{\to} & (X \stackrel{f}{\to} Y) \end{array}$$

where of course all products here are given by fiber products in $\mathcal{C}$, and the bottom arrow $proj$ may as well be taken to be the identity on $(X \stackrel{f}{\to} Y)$ since $(Y \stackrel{1_Y}{\to} Y)$ is terminal in $\mathcal{C}/Y$. So the last commutative square boils down to a commutative triangle

$$\begin{array}{&&} (Q \stackrel{q}{\to} Y) \times (X \stackrel{f}{\to} Y) & \stackrel{\psi}{\to} & (E \stackrel{f \circ p}{\to} Y) \\ & \pi \searrow & \downarrow p \\ & & (X \stackrel{f}{\to} Y) \end{array}$$

whereby this morphism $\psi$ may be interpreted as a morphism in the slice of the slice $(\mathcal{C}/Y)/f$. Under the canonical equivalence $(\mathcal{C}/Y)/f \simeq \mathcal{C}/X$, the datum $\psi$ corresponds precisely an arrow of the form

$$\psi: (f^{\ast} q) \to (E \stackrel{p}{\to} X)$$

in $\mathcal{C}/X$, and that's exactly what we want: we have established a natural bijection between arrows $\phi: (Q \stackrel{q}{\to} Y) \to \prod_f (E \stackrel{p}{\to} X)$ in $\mathcal{C}/Y$ and arrows $\psi: (f^{\ast} q) \to (E \stackrel{p}{\to} X)$ in $\mathcal{C}/X$.

[Perhaps this is exactly what Awodey says; I don't know, because I haven't seen his proof or have forgotten it if I had.]