I'm trying to write a constructive proof of the isomorphism ${Z}^{X \times Y} \equiv (Z^Y)^X$ in a category with exponential objects.


I can construct a map $(Z^Y)^X \rightarrow {Z}^{X \times Y}$, but I'm stuck trying to construct the reverse - ${Z}^{X \times Y} \rightarrow (Z^Y)^X$


Here's my inventory so far:


$$\pi\_1 : A \times B \rightarrow A$$
$$\pi\_2 : A \times B \rightarrow B$$
$$swap : A \times B \rightarrow B \times A$$
$$assoc : A \times (B \times C) \rightarrow (A \times B) \times C$$
$$intro(f\_1 : A \rightarrow B, f\_2 : A \rightarrow C) : A \rightarrow B \times C$$
$$apply : Z^Y \times Y \rightarrow Z$$
$$curry(f : X \times Y \rightarrow Z) : X \rightarrow Z^Y$$


The first map, $(Z^Y)^X \rightarrow {Z}^{X \times Y}$, arises as follows:


$$curry(apply \circ intro(apply \circ \pi\_1, \pi\_2) \circ assoc \circ intro(\pi\_2, swap \circ \pi\_2))$$


Any ideas on how to proceed for the second?




---


If anyone is wondering why, it's for [some code I'm writing](https://github.com/LightAndLight/monoidal-lens/blob/serious/src/Monoidal.hs#L130)



Constructive proof of exponential law in a category
There's a systematic way to to this -- it's an exercise in how to "unpack" the Yoneda lemma. After all, the quickest proof of this isomorphism goes like this:


$Hom(A,(Z^Y)^X) \cong Hom(A \times X, Z^Y) \\
\qquad\qquad\qquad\quad \cong Hom((A \times X) \times Y, Z) \\
\qquad\qquad\qquad\quad \cong Hom(A \times (X\times Y), Z) \\
\qquad\qquad\qquad\quad \cong Hom(A, Z^{X \times Y})$


Since the isomorphism is natural in $A$, we have $(Z^Y)^X \cong Z^{X \times Y}$ by the Yoneda lemma.


The nice thing about this proof is that it's easy to write down without getting drowned in syntax. But it seems you really want access to that hidden syntax. Never fear! Once we've written down the proof in this form, it's actually very easy to "unpack" the Yoneda lemma to get an explicit syntactic representation of this isomorphism: all you have to do is take the natural bijection you've written down and apply it to the identity map.


You've already done one direction. In the other direction, we step through the above sequence of natural isomorphisms in reverse order:


$id: Z^{X \times Y} \to Z^{X \times Y}$


$\mapsto curry\_{X \times Y}(id) : Z^{X \times Y} \times (X \times Y) \to Z$


$\mapsto curry\_{X \times Y}(id) \circ assoc^{-1} : (Z^{X \times Y} \times X) \times Y \to Z$


$\mapsto curry\_Y(curry\_{X \times Y}(id) \circ assoc^{-1}): Z^{X \times Y} \times X \to Z^Y$


$\mapsto curry\_X(curry\_Y(curry\_{X \times Y}(id) \circ assoc^{-1}): Z^{X \times Y} \to (Z^Y)^X$


Note that $apply\_{X \times Y}$ is another name for $curry\_{X \times Y}(id)$.


