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

Not the full formula (I left out some stuff involving $swap$, $intro$, etc...) but you should be able to derive it from the following sketch wich contains the idea:

Take the map $$apply:Z^{X\times Y}\times X\times Y \to Z$$ and apply $curry$ to arrive at $$Z^{X\times Y}\times X\to Z^Y$$ Then $curry$ again to get $$Z^{X\times Y}\to (Z^Y)^X$$