# Reduction under the exponential transpose

Consider the evident isomorphism between $(A^B)^C$ and $A^{B\times C}$. Awodey gives this to be given by $g=\lambda(\epsilon\circ (\epsilon\times 1)\circ \alpha_{(A^B)^C})$ and $g^{-1}=\lambda\lambda (\epsilon\circ \alpha^{-1}_{A^{B\times C}})$, where $\alpha_Z : (Z\times B) \times C \rightarrow Z\times (C\times B)$ is the evident isomorphism from commutativity and associativity.

However, I have been unable to verify that $g\circ g^{-1}=1$ or $g^{-1}\circ g=1$. I do not see any way to apply the equations of the exponential to either expression. How can I reduce these expressions to obtain the desired identity? Or does verifying the isomorphism require some other mechanism?

-
I do not think it is productive to try to write out this isomorphism using one-dimensional notation. There may be a better two-dimensional notation. –  Qiaochu Yuan Dec 22 '12 at 8:25
I'm not sure I agree. Two-dimensional notion tends to sweep coherence isomorphisms such as this one under the rug. –  Zhen Lin Dec 22 '12 at 9:14
@Zhen: then perhaps there is a three-dimensional notation which describes those coherence isomorphisms...? –  Qiaochu Yuan Dec 22 '12 at 9:44
Schematically, the isomorphism arises by applying the Yoneda lemma to the following chain of natural bijections: \begin{align} \textrm{Hom}(D, (A^B)^C) & \cong \textrm{Hom}(D \times C, A^B) \\ & \cong \textrm{Hom}((D \times C) \times B, A) \\ & \cong \textrm{Hom}(D \times (C \times B), A) \\ & \cong \textrm{Hom}(D \times (B \times C), A) \\ & \cong \textrm{Hom}(D, A^{B \times C}) \end{align} Substituting $D = (A^B)^C$ and $D = A^{B \times C}$ and chasing the bijections will give the required equations. If you are unfamiliar with this technique, here is one calculation. Let $D = A^{B \times C}$. The isomorphism $A^{B \times C} \to (A^B)^C$ is given by the formula $$c = ((\epsilon_{B \times C, A} \circ (\textrm{id}_D \times \gamma_{C, B}) \circ \alpha_{D, C, B})^B \circ \lambda_{D \times C, B})^C \circ \lambda_{D, C}$$ where $\epsilon_{B \times C, A} : A^{B \times C} \times (B \times C) \to A$ is evaluation, $\gamma_{C, B} : C \times B \to B \times C$ is the symmetry isomorphism, $\alpha_{D,C,B} : (D \times C) \times B \to D \times (C \times B)$ is the associativity isomorphism, and $\lambda_{D \times C, B} : D \times C \to ((D \times C) \times B)^B$ and $\lambda_{D, C} : D \to (D \times C)^C$ are the components of the units of the respective adjunctions. With similar notation, writing $E = (A^B)^C$, the isomorphism $(A^B)^C \to A^{B \times C}$ is: $$u = (\epsilon_{B, A} \circ (\epsilon_{C, A^B} \times \textrm{id}_B) \circ \alpha^{-1}_{E,B,C} \circ (\textrm{id}_E \times \gamma^{-1}_{C, B}))^{B \times C} \circ \lambda_{E, B \times C}$$ Now, $\lambda_{D, C}$ is natural in $D$, so $$\lambda_{D, C} \circ u = (u \times \textrm{id}_C)^C \circ \lambda_{E, C}$$ and therefore $$c \circ u = ((\epsilon_{B \times C, A} \circ (\textrm{id}_D \times \gamma_{C, B}) \circ \alpha_{D, C, B})^B \circ \lambda_{D \times C, B} \circ (u \times \textrm{id}_C))^C \circ \lambda_{E, C}$$ and similarly, $\lambda_{D \times C, B}$ is natural in $D \times C$, so $$\lambda_{D \times C, B} \circ (u \times \textrm{id}_C) = ((u \times \textrm{id}_C) \times \textrm{id}_B)^B \circ \lambda_{E \times C, B}$$ hence: \begin{align} c \circ u & = ((\epsilon_{B \times C, A} \circ (\textrm{id}_D \times \gamma_{C, B}) \circ \alpha_{D, C, B} \circ ((u \times \textrm{id}_C) \times \textrm{id}_B))^B \circ \lambda_{E \times C, B})^C \circ \lambda_{E, C} \\ & = ((\epsilon_{B \times C, A} \circ (\textrm{id}_D \times \gamma_{C, B}) \circ (u \times \textrm{id}_{C \times B}) \circ \alpha_{E, C, B})^B \circ \lambda_{E \times C, B})^C \circ \lambda_{E, C} \\ & = ((\epsilon_{B \times C, A} \circ (u \times \textrm{id}_{B \times C}) \circ (\textrm{id}_E \times \gamma_{C, B}) \circ \alpha_{E, C, B})^B \circ \lambda_{E \times C, B})^C \circ \lambda_{E, C} \end{align} Now, $\epsilon_{B \times C, A}$ is natural in $A$, so expanding even more: \begin{align} \epsilon_{B \times C, A} \circ (u \times \textrm{id}_{B \times C}) & = \epsilon_{B \times C, A} \circ (((\epsilon_{B, A} \circ (\epsilon_{C, A^B} \times \textrm{id}_B) \circ \alpha^{-1}_{E,B,C} \circ (\textrm{id}_E \times \gamma^{-1}_{C, B}))^{B \times C} \circ \lambda_{E, B \times C}) \times \textrm{id}_{B \times C}) \\ & = \epsilon_{B, A} \circ (\epsilon_{C, A^B} \times \textrm{id}_B) \circ \alpha^{-1}_{E,B,C} \circ (\textrm{id}_E \times \gamma^{-1}_{C, B}) \circ \epsilon_{B \times C, E \times (B \times C)} \circ (\lambda_{E, B \times C} \times \textrm{id}_{B \times C}) \end{align} and fortunately for us, $\epsilon_{B \times C, E \times (B \times C)} \circ (\lambda_{E, B \times C} \times \textrm{id}_{B \times C}) = \textrm{id}_{E \times (B \times C)}$ by the triangle identity, so $$\epsilon_{B \times C, A} \circ (u \times \textrm{id}_{B \times C}) = \epsilon_{B, A} \circ (\epsilon_{C, A^B} \times \textrm{id}_B) \circ \alpha^{-1}_{E,B,C} \circ (\textrm{id}_E \times \gamma^{-1}_{C, B})$$ and putting this back in yields: \begin{align} c \circ u & = ((\epsilon_{B, A} \circ (\epsilon_{C, A^B} \times \textrm{id}_B) \circ \alpha^{-1}_{E,B,C} \circ (\textrm{id}_E \times \gamma^{-1}_{C, B}) \circ (\textrm{id}_E \times \gamma_{C, B}) \circ \alpha_{E, C, B})^B \circ \lambda_{E \times C, B})^C \circ \lambda_{E, C} \\ & = ((\epsilon_{B, A} \circ (\epsilon_{C, A^B} \times \textrm{id}_B))^B \circ \lambda_{E \times C, B})^C \circ \lambda_{E, C} \\ & = ((\epsilon_{B, A})^B \circ \lambda_{A^B, B} \circ \epsilon_{C, A^B})^C \circ \lambda_{E, C} \\ & = (\epsilon_{C, A^B})^C \circ \lambda_{E, C} \\ & = \textrm{id}_E \end{align} by the triangle identities and the naturality of $\lambda_{E \times C, B}$ in $E \times C$.