Working in a Cartesian closed category we have have an exponential object $X^Y$ for object $X$ and $Y$. There are isomorphisms $1^X \cong 1$, $X^Y \times X^Z \cong X^{Y + Z}$, $X^1 \cong X$ and a few others, just like with sets. Now nlab claims they can be proven by the usual Yoneda arguments. I don't understand how to do this. See also this related question. I don't understand how this works. Let us look at that answer first.

By definition of a power object, there is a bijection between $\operatorname{Hom}(x, a^1)$ and $\operatorname{Hom}(x \times a, 1)$. Since $\operatorname{Hom}(x \times a, 1)$ contains just one element, there is a bijection $\operatorname{Hom}(x \times a, 1) \cong \operatorname{Hom}(x, a)$ as well, so $\operatorname{Hom}(x, a^1) \cong \operatorname{Hom}(x, a)$. I don't see how we can apply Yoneda to conclude there is an isomorphism between $a$ and $a^1$.


1 Answer 1


By Yoneda, we know that if $x,y \in \mathsf{C}$ are objects in some locally small category, then $x \simeq y$ if and only if the functors represented by these objects are naturally isomorphic (that is, either $\mathsf{C}(x,-) \simeq \mathsf{C}(y,-)$ or $\mathsf{C}(-,x) \simeq \mathsf{C}(-,y)$).

Let's apply that to prove that $a^1 \simeq a$. By Yoneda, it suffices to note that

$$ \mathsf{C}(x,a^1) \simeq \mathsf{C}(x \times 1,a) \simeq \mathsf{C}(x,a) $$

for any $x$, and these isomorphisms assemble into a natural isomorphism

$$ \mathsf{C}(-,a^1) \simeq \mathsf{C}(-,a) $$

which shows that $a^1 \simeq a$.

Likewise we have a natural isomorpshim given by the bijections

$$ \begin{align} \mathsf{C}(c,x^y \times x^z) &\simeq \mathsf{C}(c,x^y) \times \mathsf{C}(c,x^z) \simeq \mathsf{C}(c \times y,x) \times \mathsf{C}(c \times z,x)\\ &\simeq \mathsf{C}(c \times y \sqcup c \times z,x) \simeq \mathsf{C}(c \times (y \sqcup z),x)\\ &\simeq \mathsf{C}(c,x^{y \ \sqcup \ z}). \end{align} $$

for each $c \in \mathsf{C}$, and so $x^y \times x^z \simeq x^{y \ \sqcup \ z}$.

You can prove the rest in a similar fashion.

  • $\begingroup$ Thanks, I completely forgot about the naturality requirement of the Yoneda lemma. $\endgroup$ Oct 14, 2019 at 16:39

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.