<p>One is <em>internal</em> and the other is <em>external</em>.</p>

<p>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 <strong>set of morphisms</strong> $\mathrm{Hom}_{\mathcal{C}}(A,B)$, called the "hom-set". This set is <strong>not</strong> an object of $\mathcal{C}$, but rather an object of the category of sets.</p>

<p>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.</p>

<p>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).
$$</p>

<p>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.</p>

<p>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, <em>all</em> 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.</p>

CC BY-SA 3.0
2013-04-17T10:05:50.370Z
Thanks for the great answer, completely dispelling the mystery.
day
CC BY-SA 3.0
2013-04-21T20:19:43.590Z
Indeed! Great explanation!
Uday Reddy
CC BY-SA 3.0
2015-03-25T13:49:19.103Z
So which is internal and which is external?
CMCDragonkai
CC BY-SA 3.0
2013-04-17T09:46:40.297Z
2013-04-17T09:56:59.537Z
2013-04-17T09:56:59.537Z
Andrej Bauer
<p>In a <strong>Cartesian Closed Category</strong> (<em>CCC</em>), there exist the so-called <strong>exponential objects</strong>, written $B^A$.  When a CCC is considered as a model of the <strong>simply-typed $\lambda$-calculus</strong>, 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$?</p>

CC BY-SA 3.0
2013-04-17T09:58:47.310Z
In a *category* it is the *exponential **object***, but in *type theory* it might be called the *exponential **type***.
Andrej Bauer
CC BY-SA 3.0
2017-03-15T07:49:42.247Z
This is not a research level question. Move to cs-exchange?
Andrea Asperti
<type-theory><lambda-calculus><ct.category-theory>
What is the difference between arrows and exponential objects in a cartesian closed category?
day
# What is the difference between arrows and exponential objects in a cartesian closed category?

(Asked by: username_0 on 2013-04-17)

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

**Tags:** type-theory, lambda-calculus, ct.category-theory

> **Comments:**
> **username_1**: In a *category* it is the *exponential **object***, but in *type theory* it might be called the *exponential **type***.  
> **username_2**: This is not a research level question. Move to cs-exchange?  

---

## 1 answers

### Answer by username_1 on 2013-04-17. Score: 33 | Accepted answer

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.

> **Comments:**
> **username_0**: Thanks for the great answer, completely dispelling the mystery.  
> **username_3**: Indeed! Great explanation!  
> **username_4**: So which is internal and which is external?  

---

