Why do exponential objects (in category theory) require currying

category-theoryuniversal-property

I'm a bit confused about exponential objects in category theory.

I find them pretty intuitive when I think about them as "arbitrary-arity cartesian products"; in the sense that if I had never seen exponentials and you reminded me of the standard definition of categorical products via the usual universal construction, and you asked me to come up with a universal construction for products indexed not by just fst and snd but by an arbitrary object in the category, then I could plausibly come up with the standard diagrams for exponential objects. In this setting, the eval morphisms $A \times Z^A \to Z$ can be thought of as the $A$-indexed family of projection morphisms out of an $|A|$-arity product of $Z$ objects.

However, it seems pretty common to think of exponential objects not as arbitrary-arity cartesian, but as "function objects" — for example, the exponential objects in Hask are more-or-less the function spaces, with eval being function application. (The relation between exponential objects and functions is why those arrows are called eval arrows in the first place, IIUC.) This is an idea that I don't yet think I could replicate on my own. If I had never seen exponentials and you reminded me about categorical products and said "this universal construction pins down internal representations of the external products we could make in the product category", and then asked me to come up with a universal construction that pinned down objects which act like an internal representation of the external Hom-sets, I'd be trying to set up compose morphisms $Z^B \times B^A \to Z^A$ along with some way of generating an arrow $1 \to Z^A$ for every arrow $A \to Z$, along with a bunch of diagrams that ensure that compose acts the way it should. I don't think that I'd have the thought that I should invent eval instead (at least, not if I was a native category theorist as opposed to a native programmer).

I've played around with various definitions of this form and tried to show that this is equivalent to the standard definition of exponential objects. Given exponential objects it's easy to derive compose and a way to get from $A \to Z$ to $1 \to Z^A$, but given those two thingies, I can't see a way to get back to standard definition of exponentials without assuming something that relates the exponentials back to pairs, such as isomorphisms between $(Z^A)^B$ and $Z^{A \times B}$, or suitable morphisms $pair : ((A \times B)^B)^A$ satisfying some desired properties.

Thus, my current intuition is that exponential objects as they're usually defined aren't just internal objects that act like the external hom sets; they're objects that act like hom sets and support currying. It currently seems plausible to me that there could be a natural notion of "arrow objects" that generalize "exponential objects", where arrow objects support composition, and exponential objects add currying. However, I'm still feeling a bit confused here, and I have a vague sense that I've missed a beat somewhere. Thus, my question is:

Is there a natural reason why we should demand currying / eval on our "arrow objects"? Or, another way to state the same question: is there a natural notion of an "arrow object" that generalizes exponential objects
(analogously to how monoids generalize groups)?

(FWIW, yes, I'm aware that exponentials are right adjoint to products and that that's pretty nifty; I understand that "arrow objects" if they exist would not satisfy that property; I'd still like to know whether there exists a natural notion of arrow objects that lack this nice property but generalize exponential objects anyway.)

Best Answer

I'm not quite sure I understand your question, but some comments. The intuition that exponentials generalize products really only makes sense in categories that resemble $\text{Set}$ and in general exponentials can look quite different from this. A nice example to think about is Heyting algebras, where the exponential generalizes implication in propositional logic (to intuitionistic logic). Here eval becomes modus ponens.

In any case, once you have composition you have eval provided that you believe a very small thing. Let me write $A^B$ as $[B, A]$. The composition map $[A, B] \times [B, C] \to [A, C]$ specializes, when $A = 1$, to a map

$$[1, B] \times [B, C] \to [1, C]$$

which reproduces eval as soon as you believe that there should be a natural isomorphism $[1, A] \cong A$.

Edit: Okay, so I think I understand your question better now. In fact it is not necessary to relate exponentials in a suitably generalized sense to products if you don't want to. You can write down the axioms of a closed category instead, although I don't know any natural examples which are not closed monoidal categories. In a closed monoidal category the cartesian product is replaced by another (usually symmetric) monoidal structure; the prototypical example is $\text{Vect}$ equipped with the tensor product.

Related Question