I have to prove that a category is cartesian closed. I proved it has finite limits, equalizer and terminal object and I need to make the exponential object.
The problem is that I cannot understand how to make it. For example in Set I can only see $X^Y$ as the set of maps from Y to X. But how can I prove it is the right exponential object to take? How can I prove the natural bijection between $\textbf{Hom}(A\times Y, X)$ and $\textbf{Hom}(A, X^Y)$?
I read about curring operator and Yoneda lemma but I have not understood how to use them.
Thank you all!
Best Answer
Here are the two bijections, I will leave the proofs to you :
$\hom(A\times Y, X)\to \hom (A, X^Y) : f\mapsto (a\mapsto (y\mapsto f(a,y))$
$\hom(A,X^Y)\to \hom(A\times Y, X) : g\mapsto ((a,y)\mapsto g(a)(y))$
That is usually what is meant by Curryfication, Currying etc. and (one of) the reason(s) we are interested in exponential objects is precisely this currying business, and the fact that it's so natural and easy to write down