21
$\begingroup$

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$?

$\endgroup$
  • 3
    $\begingroup$ In a category it is the exponential object, but in type theory it might be called the exponential type. $\endgroup$ – Andrej Bauer Apr 17 '13 at 9:58
  • $\begingroup$ This is not a research level question. Move to cs-exchange? $\endgroup$ – Andrea Asperti Mar 15 '17 at 7:49
34
$\begingroup$

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.

$\endgroup$
  • $\begingroup$ Thanks for the great answer, completely dispelling the mystery. $\endgroup$ – day Apr 17 '13 at 10:05
  • $\begingroup$ Indeed! Great explanation! $\endgroup$ – Uday Reddy Apr 21 '13 at 20:19
  • $\begingroup$ So which is internal and which is external? $\endgroup$ – CMCDragonkai Mar 25 '15 at 13:49

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.