# Proof that $B^{A \times A'}$ is isomorphic to $(B^A)^{A'}$ in a CCC

How can I go about proving that $B^{A \times A'} \cong (B^A)^{A'}$ where $A$, $B$ and $A'$ are objects in a closed cartesian category.

The problem is, I can't even find a morphism from $B^{A \times A'}$ to $(B^A)^{A'}$.

I've found an arrow that goes the otherway around, it is: $curry(ev \circ(ev \times Id_A))$, where $curry(g)$ is a curried version of $g$ (I've seen it also denoted as $\hat{g}$) and $ev$ is an eval arrow.

Thanks.

Disclamer: This is a question from a textbook/tutorial "Basic Category Theory for Computer Scientists" by B. Pierce. I am working through that book on my own, so this question is not a part of my homework

The universal property of exponentiation says that to give a morphism $X\times Y \to Z$ is equivalent to giving a morphism $X \to Z^Y$. We just use this in reverse twice, first to give a morphism

$B^{A \times A'} \to (B^A)^{A'}$

is equivalent to giving a morphism

$B^{A \times A'} \times A' \to B^A$

(use $X = B^{A \times A'}$, $Y = A'$, and $Z = B^A$). But giving that morphism is equivalent to giving a morphism

$B^{A \times A'} \times A' \times A \to B$

and this final morphism can be given using an eval.

• Thanks! When I wrote everything down in a diagram it all made sense, the arrow is $curry(curry(ev))$. However, I still have a minor question: how would I go about proving that the composition of those arrows is an identity arrow? Previously, I was able to present such proofs using commutative diagrams, but in this case I only have diagrams with $(B^A)^{A'} \times A \times A'$ and not $(B^A)^{A'}$ – Daniil Jan 29 '13 at 20:13
• The universal property says that arrows $X \times Y \to Z$ are uniquely associated to arrows $X \to Z^Y$. The identity map $B^{A \times A'} \to B^{A \times A'}$ gets associated to the eval map $B^{A \times A'} \times A \times A' \to B$ so show that the composition $B^{A \times A'} \to (B^A)^{A'} \to B^{A \times A'}$ of your two arrows is also associated to this eval map. – Jim Jan 29 '13 at 20:59

\begin{align} \hom(X,B^{A\times C}) & \cong \hom(X\times A\times C,B) \\ & \cong \hom(X\times A,B^C) \\ & \cong \hom(X,(B^C)^A) \end{align} Now (with a smart application of Yoneda Lemma: see below Zhen Lin's comment) $B^{A\times C}\cong (B^C)^A$. []
• $\textrm{Hom}(X, -)$ doesn't reflect isomorphisms in general, but the collection of all $\textrm{Hom}(X, -)$ jointly reflect isomorphisms. – Zhen Lin Jan 30 '13 at 9:36