# Transposition of arrows in toposes (or cartesian closed categories)

Suppose $\mathcal{E}$ is an elementary topos (take as a definition that of Mac Lane and Moerdijk "Sheaves in Geometry and Logic"). I have a problem with a fact concerning the cartesian closure of $\mathcal{E}$: suppose we have two arrows $f:A \to B, g:B \to C$. By considering $1\times A \simeq A, 1\times B \simeq B$ we can transpose these two arrows obtaining $\hat f:1 \to B^A, \ \hat g:1 \to C^B$.

What I want to show is that $ev_B \circ (\hat g \times f)=g \circ f \circ \pi_A:1 \times A \to C$, where $ev_B:C^B \times B \to C$ is the $B$-component of the counit of the adjunction $-\times B \dashv (-)^B$. This it obviously true for $\mathcal{E}:= Sets$, but I can't find the right diagram to prove it in full generality (obviously it will be true for any cartesian closed category).

Recall that there is a hom-set bijection $$\mathrm{Hom}(X \times Y, Z) \cong \mathrm{Hom}(X, Z^Y)$$ that is natural in $X$, $Y$, and $Z$. That implies there is a natural morphism $\mathrm{ev}_{Y,Z} : Z^Y \times Y \to Z$ inducing this bijection, with the right-to-left bijection being $\hat{g} \mapsto \mathrm{ev}_{Y,Z} \circ (\hat{g} \times \mathrm{id}_Y)$. In particular, $$\mathrm{ev}_{Y,Z} \circ (\hat{g} \times f) = \mathrm{ev}_{Y,Z} \circ (\hat{g} \times \mathrm{id}_Y) \circ (\mathrm{id}_X \times f)= g \circ (\mathrm{id}_X \times f)$$ and taking $X = 1$ and using the naturality of the canonical isomorphism $1 \times T \cong T$, we may deduce the required equation.