Exponential Object - Ryan Brewer

Exponential Object

In many cases, the arrows of a category will also have some representation as objects in that same category. For example, in a category of sets and functions, functions are also sets, so may be present as both arrows and objects in the category. Categories where every arrow has a corresponding object are called "closed," though this adjective doesn't appear by itself because there are several types of "closed:" "monoidal closed," "cartesian closed," and other's; I'll discuss them in a moment. The object of an arrow \(f:X\to Y\) is called an "exponential" or "exponential object" and is written \(Y^X\). This notation comes from the idea that if \(X\) and \(Y\) are sets, the number of elements (functions) in the set \(X\to Y\) is equal to the number of elements in \(Y\) raised to the power of the number of elements in \(X\), which is kinda fun I think.

In a monoidal category, given objects \(X\) and \(Y\), an exponential object \(Y^X\) is an object such that there's an arrow \(\texttt{eval}:Y^X\otimes X\to Y\). It's a universal construction, so for any candidate exponential object \(Z\) with its arrow \(e:Z\otimes X\to Y\), there's exactly one arrow \(u: Z\to Y^X\) such that the following diagram commutes:

The notation \(u\otimes id_X\) is taking advantage of the fact that \(\otimes\) is a bifunctor, so can map a pair of morphisms \(u:Z\to Y^X\) and \(id_X:X\to X\) into a morphism from \(Z\otimes X\) to \(Y^X\otimes X\). With this sort of notation you have to just know that the things on either side of the \(\otimes\) are morphisms, not objects, to know what's going on. Note that when the tensor product is some specific bifunctor (like a cartesian product), we write that instead of \(\otimes\) (like \(\times\)).

So the idea of an exponential object \(Y^X\) is that if you have an \(Y^X\) and an \(X\), there's a way to produce a \(Y\). In that way, exponential objects behave like the collection of arrows from \(X\) to \(Y\). When a category is enriched over itself, like \(\texttt{Set}\) and Cat are, it just means that the exponential objects and the collections of arrows are actually one and the same. For example, in \(\texttt{Set}\), a function space \(A\to B\) is the set of all functions from the set \(A\) to the set \(B\), which is equal to the homset \(\texttt{Set}(A,B)\). Such categories are "monoidal closed categories," meaning any collection of arrows from an object \(X\) to an object \(Y\) has a corresponding exponential object \(Y^X\). Exponential objects only make sense in monoidal categories because you need some way of saying you have both the input object \(X\) and the arrows \(Y^X\) to get to the output object \(Y\). To say "two objects together as an object," we use the monoidal bifunctor \(\otimes\).

If that bifunctor is \(\times\), then we instead call it a "cartesian closed category," sometimes written CCC. If the bifunctor is \(+\) then we call it a "cocartesian closed category," sometime written CoCCC. And if a category has both all products and all coproducts then we call it a "bicartesian monoidal category," and if it also has all exponential objects then it's a "bicartesian closed category," sometimes written BCCC. \(\texttt{Set}\) is a BCCC because of cartesian products, singleton sets, unions, the empty set, and function spaces. Categories of types and functions, used in functional programming, are often BCCCs because of tuple types, the unit type (), tagged unions, the empty type void, and function types.

The dual of an exponential is a coexponential, written \(Y-X\). These are interesting for modelling classical, cointuitionistic, and bi-intuitionistic logic in category theory. Logically they are a proof of \(Y\) and a refutation of \(X\) conjoined.