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

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.

-
I'm going to guess you're not using Awodey's definition of locally cartesian closed, because his definition makes it a tautology... –  Zhen Lin Aug 25 '11 at 0:46
Indeed, I meant a category where where all slices are cartesian closed :) –  Tilo Wiklund Aug 25 '11 at 9:03

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 $J \to \bigcup_{j \in J} Y_j$?

Let $\mathbf{C}$ be a locally cartesian closed category, in the sense that $\mathbf{C}$ has a terminal object $1$ and every slice category $\mathbf{C} / A$ is cartesian closed. Let $f : A \to B$ be an arrow in $\mathbf{C}$; then it is also an object in $\mathbf{C} / B$. Observe that the slice of $\mathbf{C} / B$ over $f : A \to B$ is equivalent to $\mathbf{C} / A$: indeed, to give an arrow from $q : Y \to B$ to $f : A \to B$ it suffices to give an arrow $h : Y \to A$, since the condition $q = f \circ h$ determines $q$ freely and uniquely. Observe also that $\mathbf{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 $\mathbf{C} / B$.

Now, since $\mathbf{C} / B$ is cartesian closed, we may exponentiate $q : Y \to B$ by $f : A \to B$ to obtain an arrow (in $\mathbf{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 : \mathbf{C}/B \to \mathbf{C} /B$ is a functor, so if we have an arrow $h : Y \to A$ and $q = f \circ h$ (i.e. we have an arrow $h : q \to f$ in $\mathbf{C} / B$), we may obtain an arrow $h^f : Y^f \to A^f$. But $\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. an arrow $s : B \to A^f$ such that $f^f \circ s = \textrm{id}_B$). Now, take the pullback (in $\mathbf{C}$) of $h^f$ and $s$ to obtain $\Pi_f h : \Pi_f Y \to B$.

Finally, we show that $\Pi_f : \mathbf{C}/A \to \mathbf{C}/B$ is the right adjoint of the pullback functor $f^* : \mathbf{C}/B \to \mathbf{C}/A$. So we wish to 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$ and $h : Y \to A$. But, by considering a suitable diagram, we see that $$\textrm{Hom}_A (f^* p, h) \cong \textrm{Hom}_B (p \mathbin{\times_B} f, q)$$ where $q = f \circ h$, and it is clear that $$\textrm{Hom}_B (p, q^f) \cong \textrm{Hom}_B (p, \Pi_f h)$$ by the universal property of pullbacks, and all these are natural in $p$ and $h$. So we are done.

-
Much obliged, that clarified things a lot. Now for some more diagram chasing :) –  Tilo Wiklund Aug 25 '11 at 13:23
I just realised something. Wouldn't $\mathrm{Hom}_B\left(p, q^f\right) \cong \textrm{Hom}_B \left(p, \Pi_f h\right)$ imply that $-^f$ itself was a right adjoint to $f^*$? –  Tilo Wiklund Aug 27 '11 at 16:38
@Tilo: Not quite. We need something functorial in $h$, not $q$. –  Zhen Lin Aug 28 '11 at 1:29
But isn't $q^f$ just the composition of functors $-^f$ and $\Sigma_f$ (i.e. postcomposition by $f$, the left adjoint of the pullback) applied to $h$? –  Tilo Wiklund Aug 28 '11 at 10:12
@Tilo: Ah, then yes. But perhaps there's some subtlety I'm missing here, hmmm. –  Zhen Lin Aug 28 '11 at 10:56