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. $\newcommand{\C}{\mathbf{C}}\newcommand{\hC}{\hat\C}$

Theorem. Given any small category $\C$, the presheaf category $\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 $\renewcommand{\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

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

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

So we make an educated guess and define

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

That’s to say, for any $\newcommand{\naturalto}{\overset{\bullet}{\longrightarrow}} \eta : y(D)\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:

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

while going around the bottom left side of the square gives

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 $\DeclareMathOperator{\Nat}{Nat}\{ e_{P,C} : \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)$,

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

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:

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

while going around the bottom left gives us

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)$,

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

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

So the obvious candidate is:

Let’s check commutativity:

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!