$$\gdef{\Hom}{\mathsf{Hom}}$$ $$\gdef{\C}{\mathbf{C}}$$ $$\gdef{\hC}{\hat\C}$$

As I’ve been working through “Sheaves in Geometry and Logic”, I’ve been skimming proofs and attempting to rederive them. I normally end up with a better understanding of the material, but sometimes I get stuck. Here’s one case where I’ve gotten stuck: can anybody tell me why the counit for the exponential is universal? In particular, I can’t manage to show the uniqueness of $$\phi'$$ at the end of the proof. I started this entry back in April, and figured I should finally finish it off and ask for help.

Theorem. Given any small category $$\C$$, the presheaf $$\hC$$ is Cartesian closed.

Proof. We must show that $$\hC$$ has a terminal object $$1$$, finite products, and exponentials.

The terminal $$1 : \C^{op} \to \mathbf{Sets}$$ is given by the constant functor onto $$1$$ in $$\mathbf{Sets}$$.

The product $$P \times Q : \C^{op} \to \mathbf{Sets}$$ of $$P, Q : \C^{op} \to \mathbf{Sets}$$ is given pointwise, that is, $$(P \times Q)(C) = P(C) \times Q(C)$$.

So it remains to find an exponential $$Q^P$$. Recall that, by analogy with the motivating example in $$\gdef{\S}{\mathbf{Sets}}\S$$, we define exponentiation to be right adjoint to the right product, explicitly, $$({-}) \times Q \dashv ({-})^Q$$. In particular, for all $$P, Q, R$$, we want

$$\tag{*}\Hom(P\times Q,R) \simeq Hom(P, R^Q)$$

natural in $$P$$ and $$Q$$.

A first guess of $$R^Q(C) = \Hom(Q(C), R(C))$$ fails to work in any sensible functorial way (it’s not at all clear what $$R^Q(f)$$ should be).

Suppose now that $$P$$ is representable. Then there exists a $$C$$ such that $$P \simeq \Hom(-, C) = y(C)$$. Then (*) becomes

$$\Hom(y(C)\times Q, R) \simeq \Hom(y(C), R^Q).$$

But by the Yoneda lemma, assuming $$R^Q$$ exists,

$$\Hom(y(C), R^Q) \simeq R^Q(C)$$

So we make an educated guess and define

$$R^Q(C) = \Hom(y(C) \times Q, R)$$

and for $$f : C \to D$$, let $$R^Q(f) : R^Q(D) \to R^Q(C)$$ be given by

$$R^Q(f) = \Hom(y(f) \times Q, R).$$

That’s to say, for any $$\gdef{\naturalto}{\Rightarrow} \eta : y(D)\times Q \naturalto R$$,

$$R^Q(f)(\eta) = \eta \circ (y(f) \times Id_Q) : y(C)\times Q \naturalto R.$$

So we’ve defined $$(-)^Q$$ on objects. Now we must define $$\xi^Q : P^Q \to R^Q$$ for arrows $$\xi : P \to Q$$ of $$\hC$$. What we need is a natural transformation $${ (\xi^Q)_C : P^Q(C) \to R^Q(C) }_C$$, that is, a family $${ (\xi^Q)_C : Hom(y(C) \times Q, P) \naturalto Hom(y(C) \times Q, R) }_C$$ of arrows of $$\S$$. Here, we make use of our intuition from $$\S$$ and define:

$$(\xi^Q)_C(\gamma : y(C) \times Q \naturalto P) = (\xi \circ \gamma) : y(C) \times Q \naturalto R.$$

It is straightforward to check that $$\xi^Q$$ is a natural transformation, that is, for each $$f : D \to C$$ in $$\C$$, we have

Indeed, given a $$\gamma : y(C) \times Q \naturalto P$$, going around the top right side of the square gives

\begin{aligned} &R^Q(f)((\xi^Q)_C \gamma)\\ &= R^Q(f)(\xi \circ \gamma)\\ &= \xi \circ \gamma \circ (y(f) \times Id_Q), R^Q(f)((\xi^Q)_C \gamma) \end{aligned}

while going around the bottom left side of the square gives

\begin{aligned} &(\xi^Q)_D (P^Q(f)(\gamma))\\ &= (\xi^Q)_D(\gamma \circ (y(f) \times Id_Q))\\ &= \xi \circ \gamma \circ (y(f) \times Id_Q). \end{aligned}

Now that we have a candidate for $$(-)^Q$$, we need to show that it is actually an exponential, that’s to say, that for all $$Q$$, we have the adjunction $${-} \times Q \dashv ({-})^Q$$. We do so by means of a counit $$e : (-)^Q \times Q \naturalto I$$. Observe that in $$\S$$, this counit is exactly function evaluation, i.e., $$e_R : \Hom(Q, R)\times Q \to R$$ is given by $$(f, q) \mapsto f(q)$$. Hence why we call the counit $$e$$ “evaluation”.

Recall that a counit $$\epsilon$$ for an adjunction $$F \dashv G$$ is a “natural transformation $$\epsilon : FG \naturalto I$$ such that each arrow $$\epsilon_a$$ is universal from $$a$$ to $$F$$ while each $$g : x \to Ga$$ has left adjunct $$\epsilon_a \circ Fg : Fx \to a$$” [CWM].

So to show that $$e$$ is a counit for $${-} \times Q \dashv (-)^Q$$, we must show that it is a natural transformation $$(-)^Q\times Q \naturalto I$$ such that $$e_P$$ is universal from $$(-) \times Q$$ to $$P$$. That’s to say, for every $$\phi : S\times Q \naturalto P$$, we must have a unique $$\phi' : S \naturalto P^Q$$ such that the following triangle commutes:

We see that our choices are heavily constrained by the types at hand. For every $$P$$, we need a natural transformation $$e_P : P^Q \times Q \naturalto P$$, i.e., a family $${ e_{P,C} : P^Q(C) \times Q(C) \to P(C) }_C$$, i.e., a family of morphisms $${ e_{P,C} : \mathsf{Nat}(y(C) \times Q, P) \times Q(C) \to P(C) }_C$$ in $$\S$$. So each $$e_{P,C}$$ receives a pair $$(\eta, q)$$,

\begin{aligned} \eta &: \Hom(-, C)\times Q \naturalto P\\ q &\in Q(C) \end{aligned}

and must produce an $$e_{P,C}(\eta, q) \in P(C)$$. The only arrow into $$C$$ we know must exist is the identity $$1_C : C \to C$$. Observe also that $$\eta_C : Hom(C, C)\times Q(C) \to P(C)$$. So we take

$$e_{P,C}(\eta, q) = \eta_C(1_C, q).$$

Though we were in a sense “forced” to make this definition by the types, we must still check that $$e_P$$ is a natural transformation. Let $$f : D \to C$$ be arbitrary in $$C$$. We must show that

To see why $$(Pf \circ \eta_C)(1_C, q) = (\eta\circ(y(f) \times Id))_D(1_D, Q(f)(q))$$, first observe:

\begin{aligned} &(\eta\circ(y(f) \times Id))_D(1_D,Q(f)(q))\\ &= \eta_D(y(f)(1_D), Q(f)(q))\\ &= \eta_D(f, Q(f)(q)). \end{aligned}

But $$\eta : \Hom(-, C)\times Q(C) \naturalto P$$ is natural, so we have $$P(f) \circ \eta_C = \eta_D \circ (\Hom(f, C) \times Q(f))$$, in particular, that $$(P(f) \circ \eta_C)(1_C, q) = (\eta\circ(y(f) \times Id))_D(1_D,Q(f)(q)) = \eta_D(f, Q(f)(q))$$. So by transitivity, we have the desired equality in the bottom right corner of the naturality diagram. So we conclude that $$e_P$$ is a natural transformation and is thus eligible to be component of the (candidate) natural transformation $$e : (-)^Q \times Q \naturalto I$$. (There is no confusion here: because the morphisms of $$\hC$$ are natural transformations, the components $$e_P$$ of $$e$$, being arrows of $$\hC$$, are natural transformations. To the best of my understanding, this is an instance of a 2-category.) We must now show that $$e$$ is a natural transformation between the functors $$(-)^Q \times Q : \hC \to \hC$$ and $$I : \hC \to \hC$$. Let $$P$$ and $$R$$ be arbitrary objects (functors) in $$\hC$$ and let $$\xi : P \naturalto R$$ be an arbitrary morphism (natural transformation) between them. Then we want to show that the following diagram commutes:

This diagram commutes if and only if for every object $$C$$ in $$\C$$, the following diagram commutes in $$\S$$:

Given a pair $$(\eta : y(C) \times Q \naturalto P, q \in Q(C))$$, going around the top right corner of the square gives us

\begin{aligned} &\xi_C(e_{P,C}(\eta, q)\\ &= \xi_C(\eta_C(1_C, q))\\ &= (\xi \circ \eta)_C (1_C, q), \end{aligned}

while going around the bottom left gives us

\begin{aligned} &e_{R,C}((\xi^Q)_C\; \eta, q)\\ &=e_{R,C}(\xi \circ \eta, q)\\ &= (\xi \circ \eta)_C(1_C, q). \end{aligned}

So we can finally conclude that $$e : (-)^Q \times Q \naturalto I$$ is a natural transformation.

Let’s briefly recap what we’ve accomplished so far and where we’re trying to go. We’re trying to show that $$\hC$$ has exponents, that’s to say, a right adjoint $${-}\times Q \dashv (-)^Q$$. We’ve found a candidate functor $$(-)^Q : \hC \to \hC$$, as well as a natural transformation $$e : (-)^Q \times Q \naturalto I$$. All that remains is to show that $$e : (-)^Q \times Q \naturalto I$$ is a counit for the adjunction. This involves finding for every $$\phi : S \times Q \naturalto P$$ a unique $$\phi' : S \naturalto P^Q$$ such that the above-given triangle commutes.

So we need for all $$C$$, $$s \in S(C)$$, $$q \in Q(C)$$,

$$\phi_c(s, q) = e_{P,C}(\phi'_C (s), q) = (\phi'_C (s))_C(1_C, q),$$

where $$\phi'_C(s) : y(C)\times Q \naturalto P$$ is a natural transformation. So we must find a family of maps

$$\{ (\phi'_C (s))_D : \Hom(D, C)\times Q(D) \to P(D) \}_D$$

natural in $$D$$. Let’s draw inspiration from the types at hand: again they will force our hand.

\begin{aligned} \phi_D &: S(D) \times Q(D) \to P(D)\\ S(f) &: S(C) \to S(D) \text{ for } f \in \Hom(D, C)\\ s &\in S(C)\\ q &\in Q(D)\\ \end{aligned}

So the obvious candidate is:

$$(\phi'_C(s))_D(f,q) = \phi_D(S(f)(s), q).$$

Let’s check commutativity:

\begin{aligned} e_{P,C}(\phi'_C(s), q) &= (\phi'_C(s))_C(1_C, q)\\ &= \phi_C(S(1_C)(s), q)\\ &= \phi_C(s, q). \end{aligned}

So the triangle commutes as desired.

Checking naturality is straightforward.

All that remains is to show the uniqueness of $$\phi'$$. And this, dear reader, is where I’m stuck. Any hints would be greatly appreciated, please comment below!