# Why do exponential objects (in category theory) require currying?

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.)

• Perhaps a reason we don't look at arrows $1\to Z^A$ is that in many categories, such points don't characterize objects, e.g. in $G-Set$, a point $1\to X$ corresponds to a fixed point in $X$: there may be "nonempty" objects without points. So if we looked at exponentials only this way, we might "miss some arrows". In a sense, $Z^A$ has some "internal coherence" that maps $1\to Z^A$ don't classify – Max Aug 1 '18 at 21:16
• As Qiaochu Yuan indicates, attempting to view exponentials as "arbitrary arity products" is very limiting and fails very quickly. It's not clear what a "torus-fold product" or "ring-fold product" should be at all. A notion of "underlying set" might not exist at all, and, at any rate, using it would discard all the structure of the objects. Do we really want $B^R\cong B^S$ for all rings $R$ and $S$ with the same cardinality? Usually an identification between exponentials $B^A$ and "$A$-fold" products is only possible if $A$ is "discrete" in some way. In $\mathbf{Set}$, everything is discrete. – Derek Elkins Aug 1 '18 at 21:22
• The currying isomorphism is basically the entire definition of an exponential or its generalization in monoidal categories. If we drop that "requirement", we are left with basically no requirements. I would say the "real" question is: "Why do we care so much about currying at all?" – Derek Elkins Aug 1 '18 at 22:05
• Do you have any intuition as to why we care so much about currying at all? :-p – Nate Aug 3 '18 at 15:11

## 1 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.

• Thanks. My point about exponentials generalizing products was less a claim about how exponentials always generalize products, and more a claim about how I could generate the diagram for exponentials given the prompt "think about how generalized products work in Set". My trouble is that I don't think I could generate the same diagram given the prompt "think about how functions work in Set", because while I would have come up with compose, I wouldn't have thought to demand currying. – Nate Aug 1 '18 at 21:13
• Also, thanks for the note re: eval -- I stared at this a bit myself yesterday, and I wasn't able to get exponentials from compose + eval either; I still needed an extra function $pair : [A, [B, A \times B]]$. This is the sort of thing that I don't think I'd demand when trying to write a diagram that captures functions in Set and see what it generalizes to in other (not-necessarily-concrete) categories, and that I'm therefore confused about. – Nate Aug 1 '18 at 21:15
• @Nate: okay, I think I understand your question better now. In fact there is an axiomatization of "arrow objects" that doesn't require currying. – Qiaochu Yuan Aug 1 '18 at 21:49
• @QiaochuYuan For monoidally closed categories, the key adjunction is exactly a "currying" style adjunction. I would say that it more indicates that "currying" doesn't depend that much on the "cartesian-ness" of the product, than that "currying" has been avoided. Almost all the usual properties of exponentials follow from symmetric monoidally closed structure. For general closed categories, it feels more like centipede mathematics that skirts around the monoidal structure but still has shadows of "currying" in it. – Derek Elkins Aug 1 '18 at 22:02
• Thanks Qiaochu and Derek, that helps. I now think of Vect as coming equipped with exponential-ish objects that curry wrt the tensor product rather than the cartesian product. I'm still feeling a bit confused about why currying (with respect to some product-like thing) is so central to the definition of an exponential in a way that feels central to my question; do you have any insight as to what's up with that? – Nate Aug 3 '18 at 15:14