How do I think of the exponential object in a category?

Question

I'm trying to understand Cartesian Closed Categories for purposes of understanding type theory, and I am stuck at understanding what an exponential object is.

Let $C$ be a category, let $Z$ and $Y$ be objects of $C$, and let $C$ have all binary products wit $Y$. An object $Z^Y$ together with a morphism $\text{eval}:(Z^Y \times Y) \to Z$ is an exponential object if for any object $X$ and a morphism $g: X \times Y \to Z$ there is a unique morpism $\lambda g : X \to Z^Y$ (called the transpose of $g$) such that the following diagram commutes:

Could some simpler intuitions on this be shared? I went through the examples, for eg one in set theory but am still confused as to what is the essence of this matter.

Answer 1

Let $Top$ be some category of spaces with continuous maps between them. When you have two spaces $X$ and $Y$, then there is a set $Top(X,Y)$ of continuous maps between them. But it also makes intuitively sense that $Top(X,Y)$ should be more than a set. One can imagine what it might mean to pertube a continuous map slightly, and one can whish that there might be sth like a continuously varying family of maps on one or more parameters and so on. Hence, the set $Top(X,Y)$ should have some kind of cohesion. For some choices of $Top$ it is possible to equip $Top(X,Y)$ with a reasonable topology, and the resulting space is denoted by $Y^X$. For example, when $X$ is the interval $I$ then $Y^I$ is the space of paths in $Y$, equipped with a suitable topology. The universal property of the exponential object implies in particular that the points of $Y^I$ are \begin{align} U(Y^I)=Top(pt,Y^I) = Top(pt\times I,Y)=Top(I,Y) \end{align} (or at last are naturally in bijection with) the paths in $Y$. I think that this is the right intuition for most other instances of exponential objects. The exponentials in the category of sets are just set of functions. It is a good exercise to write down the bijection $Set(X\times Y,Z) = Set(X,Z^Y)$ explicitly, it is called currying. Another good exercise is two use the fact that the forgetful functor $U:Top\to Set$ is represented by the space $pt$ to find out how the bijection $Top(X\times Y,Z) = Top(X,Z^Y)$ must look like on the level of points.

If you already know type theory, then I can tell you that the exponential object is the interpretation of a $\Pi$-type $\Pi(x:X).Y$ where $Y$ does not depend on the variable $x:X$.

Answer 2

If you are looking for elementary, entry-level, motivation ("the essence of this matter"), perhaps these introductory thoughts might help.

Start from the fact that in categories where arrows are functions, they are always monadic functions. So how can we accommodate binary functions?

Pre-categorially, we have a couple of familiar devices for doing without genuine multi-place functions by providing workable substitutes.

1. The default set-theoretic procedure is to trade in an underlying binary function $\underline{f}\colon A, B \to C$ for a related official unary function $f \colon A \times B \to C$.

Alternatively, varieties of type theory typically deal with two-place functions in a quite different way. To illustrate: addition -- naively a binary function -- is traded in for a function of the type ${N} \to ({N} \to {N})$. This is a unary function which takes one number (of type ${N}$) and outputs something of a higher type, i.e. a unary function (of type ${N} \to {N}$). So we get from two numbers as input to a numerical output in two steps. We feed the first number to a function of type ${N} \to ({N} \to {N})$, which delivers another function of type ${N} \to {N}$ as output; and then we feed the second number to this second function.

This so-called currying manoeuvre is of course also perfectly adequate for certain formal purposes. And we can use the same device in a more set-theoretic framework, trading in a binary $\underline{f}\colon A, B \to C$ for a function $A \to (B \to C)$. But in this framework, where does a function from $B$ to $C$ live? In the exponential $C^B$, the set of all the functions from $B$ to $C$.

Hence, in set-theoretic terms,

2. Currying is essentially a matter of trading in a binary function $\underline{f} \colon A, B \to C$ for a related function $\overline{f} \colon A \to C^B$, i.e. the function which sends $a$ to the function $f_a = \underline{f}(a, \cdot)$ whose value for input $b$ is $\underline{f}(a, b).$

The obvious next question, is how do these two substitutes $f$ and $\overline{f}$ for the underlying binary function $\underline{f}$ fit together?

At a first shot, we want something like the following informal, pre-categorial, diagram to commute, where eval is a binary function that takes a function living in $C^B$ (i.e. a function from $B$ to $C$) and evaluates it for a given argument in $B$.

In other words, if we take a pair $\langle a, b\rangle$ from $A \times B$, we can (1) use that pair as input to $f$. Or (2) we can use $\overline{f}$ to send $a$ to a function $f_a\colon B \to C$ (i.e. the function $\underline{f}(a, \cdot)$) while carrying along $b$ unchanged: and then the binary eval applies that function from $B$ to $C$ to the input $b$. By either route, we get the same result.

Now, that first shot gives us the core idea, except that it leaves us with a binary function eval still in play. So let's revise since we want everything unary. As a second shot, we'll say we need the following to commute:

where $\overline{f} \times 1_B$ acts component-wise on $A \times B$, sending a pair $\langle a, b\rangle$ to $\langle\overline{f}(a), b\rangle$, and $ev$ is now a unary function which takes $\langle\overline{f}(a), b\rangle$ and applies its first component -- which, remember, is a function from $B$ to $C$ -- to the argument $b$. Note: given $f$ and given $ev$ with its intended meaning, $\overline{f}$ will be the unique function from $A$ to $C^B$ which makes the diagram commute.

And now everything is nicely set up to carry over smoothly to a categorial framework ...

[That's excerpted from my Category Theory I: Notes towards a gentle introduction which is freely downloadable from logicmatters.net/categories]