mjhjmtu

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

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) \
qquadqquadqquadquad cong Hom((A times X) times Y, Z) \
qquadqquadqquadquad cong Hom(A times (Xtimes Y), Z) \
qquadqquadqquadquad 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^Xtimes Ytimes Xtimes Y to Z$$ and apply $curry$ to arrive at $$Z^Xtimes Ytimes Xto Z^Y$$ Then $curry$ again to get $$Z^Xtimes Yto (Z^Y)^X$$

$$defcurrymathsfcurry,$$
$$defapplymathsfapply,$$
$$defIdmathsfId$$
$$defassocmathsfassoc$$

Recall the
$$textExponential Characterisation: qquadqquad
k = curryf quadequivquad 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:
beginalign*
& 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
endalign*

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