Constructive proof of exponential law in a category 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
 A: 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$$
A: 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)$.
A: $$\def\curry{\mathsf{curry}\,}$$
$$\def\apply{\mathsf{apply}\,}$$
$$\def\Id{\mathsf{Id}}$$
$$\def\assoc{\mathsf{assoc}}$$
Recall the
$$\text{Exponential Characterisation:} \qquad\qquad 
  k = \curry{f} \quad\equiv\quad f = \apply ∘ (k × \Id) $$
and the typings
$$ \curry \;:\;  (X × Y → Z) \;⟶\; (X → Z^Y)$$
$$ \apply  \;:\; Z^Y × Y → Z$$
From these, we can find the desired morphism by investigating the types:
\begin{align*}
  &   k : Z^{X × Y} → (Z ^ Y) ^ X
\\ ⇐ \quad & k = \curry f \;\land\; f : Z^{X × Y} × X → Z ^ Y
\\ ⇐ \quad & f = \curry g \;\land\; g : (Z^{X × Y} × X) × Y → Z
\\ ⇐ \quad & g = h \circ \assoc⁻¹ \;\land\; h : Z^{X × Y} × (X × Y) → Z
\\ ⇐ \quad & h = \apply
\end{align*}
Hence, $$k = \curry f = \curry (\curry g) = \curry (\curry (\apply \circ \assoc⁻¹))$$
I've avoided the position-switching of $X$ and $Y$ for simplicity; for that case you should be able to come up with
 yourExpCurry = curry (curry (apply ∘ ⟨ fst , swap ∘ snd ⟩ ∘ assocr))


Associated code along with a partially complete proof of the inverse laws can be found here: https://github.com/alhassy/RandomProgramming/blob/master/Agda/Exponentials.agda
