What is the difference between arrows and exponential objects in a cartesian closed category?

Question

In a Cartesian Closed Category (CCC), there exist the so-called exponential objects, written $B^A$. When a CCC is considered as a model of the simply-typed $\lambda$-calculus, an exponential object like $B^A$ characterizes the function space from type $A$ to type $B$. An exponential object is introduced by an arrow called $curry : (A \times B \rightarrow C) \rightarrow (A \rightarrow C^B)$ and eliminated by an arrow called $apply : C^B \times B \rightarrow C$ (which unfortunately called $eval$ in most texts on category theory). My questions here is: is there any difference between the exponential object $C^B$, and the arrow $B \rightarrow C$?

Answer 1

One is internal and the other is external.

A category $\mathcal{C}$ consists of objects and morphisms. When we write $f : A \to B$ we mean that $f$ is a morphism from object $A$ to object $B$. We may collect all morphisms from $A$ to $B$ into a set of morphisms $\mathrm{Hom}_{\mathcal{C}}(A,B)$, called the "hom-set". This set is not an object of $\mathcal{C}$, but rather an object of the category of sets.

In contrast, an exponential $B^A$ is an object in $\mathcal{C}$. It is how "$\mathcal{C}$ thinks of its hom-sets". Thus, $B^A$ must be equipped with whatever structure the objects of $\mathcal{C}$ have.

As an example, let us consider the category of topological spaces. Then $f : X \to Y$ is a continuous map from $X$ to $Y$, and $\mathrm{Hom}_{\mathsf{Top}}(X,Y)$ is the set of all such continuous maps. But $Y^X$, if it exists, is a topological space! You can prove that the points of $Y^X$ are (in bijective correspondence with) the continuous maps from $X$ to $Y$. In fact, this holds in general: the morphisms $1 \to B^A$ (which are "the global points of $B^A$") are in bijective correspondence with morphisms $A \to B$, because $$\mathrm{Hom}(1, B^A) \cong \mathrm{Hom}(1 \times A, B) \cong \mathrm{Hom}(A, B). $$

Sometimes we get sloppy about writing $B^A$ as opposed to $A \to B$. In fact, often these two are synonyms, with the understanding that $f : A \to B$ might mean "oh by the way here I meant the other notation, so this means $f$ is a morphism from $A$ to $B$." For example, when you wrote down the currying morphism $$\textit{curry}: (A \times B \to C) \to (A \to C^B)$$ you really should have written $$\textit{curry}: C^{A \times B} \to {(C^B)}^A.$$ So we cannot really blame anyone for getting confused here. The inner $\to$ is used in the internal sense, and the outer in the external.

If we work in simply typed $\lambda$-calculus then everything is internal, so to speak. We have just a basic typing judgment "$t$ has type $B$", written as $t : B$. Because here $B$ is a type, and types correspond to objects, then we clearly have to interpet any exponentials and arrows in $B$ in the internal sense. So then, if we understand $$\textit{curry}: (A \times B \to C) \to (A \to C^B)$$ as a typing judgment in the $\lambda$-calculus, all arrows are internal, so this is the same as $$\textit{curry}: ((C^B)^A)^{C^{A \times B}}.$$ I hope by now it is clear why people use $B^A$ and $A \to B$ as synonyms.