$ \newcommand{\Hom}{\mathrm{Hom}} $I am an undergraduate math student, and while studying cartesian closed categories i encountered a problem i could not solve:
Suppose we have a (locally small) cartesian closed category $C$, and let us denote the exponential of $a, b$ as $b^a$ and the terminal object as $1$. Since we know $C$ is a c.c.c., there is a bijection between the hom-sets $\Hom(a \times b, c)$ and $\Hom(a, c^b)$; in particular if we set $a = 1$, we can denote elements of the hom-set $\Hom(1, c^b)$ as $[f]$ for some $f$ in the hom-set $\Hom(b, c)$.
The definition of exponential object in $C$ also gives us a map $\lambda :\Hom(a \times b, c) \to \Hom(a, c^b)$. The evaluation morphism actually is the image under this map of the identity morphism, fixing of course $a = b^c$. The source and target hom-sets have an "analogue" in some objects of $C$, respectively $c^{a \times b}$ and ${c^b}^a = ({c^b})^a$.
My question is this: does the map $\lambda$ have an "analogue" in some morphism in the hom-set $\Hom(c^{a \times b}, {c^b}^a)$?
In the same way, as $C$ is cartesian closed, we have a map $$\times: \Hom(c, a) \times \Hom(c, b) \to \Hom(c, a \times b)$$ which sends $(f, g)$ to $f \times g$; the source and target sets for this map have an "analogue" in $b^c \times a^c$ and $(a \times b)^c$; does this map have an "analogue" too, in the corresponding hom-set?
edit: i am aware of and sorry about the horror that comes with the last formula: i used $\times$ as the name of the map, to denote the cartesian product in $\mathbf{Set}$ of the two hom-sets and for the internal product of the category $C$. But not "abusing" the $\times$ symbol would hide the point i'm trying to make here, so please accept my apology about that. The formula could be written as $$\psi: \Hom(c, a) \times \Hom(c, b) \to \Hom(c, a \times_C b)$$ and $\psi$ is the map i'm asking about.
edit 2: after a bit of "diagram chaising" in set, i think i came up with a solution (thanks to Omar Antolìn-Camarena for pointing out a very easy way to solve the problem for the curryfication map, $\lambda$) for both the curryfication and the product maps. The base idea i am following is to use the Yoneda lemma for proving that, if the hom-functors $\Hom(-, a) \cong \Hom(-, b)$ are isomorphic (that is to say that the hom-sets $\Hom(x, a) \cong \Hom(x, b)$ are isomorphic in $Set$, naturally in $x$) the isomorphism must raise from an isomorphism in $C$. (Is this actually a consequence of the Yoneda lemma, or have i misunderstood this important result?) As a consequence, we can show that $$\Hom(w, z^{x \times y}) \cong \Hom(w \times (x \times y), z) \cong \Hom((w \times x) \times y, z) \cong \Hom(w \times x, z^y) \cong \Hom(w, {z^y}^x)$$ and the isomorphism between the first and last hom-sets must raise from an isomorphism in $C$ in $\Hom(z^{x \times y}, {z^y}^x)$
In the same way, we can show that (using the universal property of the product) $$\Hom(w, y^x \times z^x) \cong \Hom(w, y^x) \times \Hom(w, z^x) \cong \Hom(w \times x, y) \times \Hom(w \times x, z) \cong \Hom(w \times x, y \times z) \cong \Hom(w, (y \times z)^x)$$
again, we conclude that there must be an isomorphism in $C$ from which the isomorphism in $Set$ between the first and last hom-sets must have risen, as dictated by the Yoneda lemma.
Is this wrong, and if so why? Any help will be greatly appreciated. Also, it seems to me that the very clean and intuitive solution given by Omar Antolìn-Camarena does not work for finding the second isomorphism; but, i have no clue how to (dis)prove this claim of mine.
edit 3: corrected the typos in the argument for $y^x \times z^x$.
It took me quite a bit trying to prove the naturality of the isomorphisms; since it seems to me that the proof is not totally straightforward i'll try to summarize the key points, in order to help whoever might come across this post having this same problem and to check if i got something wrong:
the naturality for the exponential follows directly from the equality $\lambda_{x}^{-1}(f) = \mathrm{Eval} \circ (f \times \mathrm{Id}_x)$
the naturality for the product follows directly from the equality $\times^{-1}(f) = (\pi_1 \circ f, \pi_2 \circ f)$
the bijection between natural isomorphisms in $\mathrm{Nat}(\Hom(-, a), \Hom(-, b))$ and isomorphisms in $\Hom(a, b)$ is obtained by chaising the identity in a naturality square built on a morphism $f : b \to a$ and applying the properties of natural isomorphisms.
From these 3 facts we can conclude that such morphisms exist, are isomorphisms and are the image under the natural isomorphisms of the identity morphism.