In category theory: Do we need products to define exponentials?

Question

In the HoTT book the type of functions $A\to C$ construction is described first and the product type $A\times B$ construction later, using function types in its definition.

So my obvious naive question is:

Is there a universal property for exponentials which is independent of the existence of binary products? (or at the very least does not use them in its formulation)

Remark: I do not want to generalize exponentials to internal-homs in a monoidal category. I am looking for a property characterizing exponentials, which is equivalent to the usual property in the presence of binary products but makes no mention of binary products, if something like this exists.

Answer 1

If I'm understanding the question, the answer is pretty much "no", to the best of my knowledge. There is a notion of closed category (note the absence of the word "monoidal") which involves a mixed variance bifunctor, say $[-\Rightarrow -]$, satisfying certain naturality conditions that make it resemble an exponential minus the universal property. The best you can say is that if all functors of the form $[a\Rightarrow-]$ have left adjoints, then the category is also monoidal closed; but what makes for "real" exponentials is exactly that the monoidal structure is the Cartesian monoidal structure. Exponentiation doesn't distinguish itself as a closed structure in any other way that I'm aware of.

The reason that you can seemingly treat function types in theories like HoTT without even having product types is that the syntax of the language smuggles in products automatically. They do this with their context, the list of variables we're considering free in our type expression. The structural rules (as seen in the HoTT book's appendix) tell you in a sly way that the lists of free variables behave like products, and terms-in-context are actually morphisms with domains products. That is, you should think of a judgment like "$x:A,y:B\vdash t:C$" as notation for $t:A\times B\to C$ in whatever category our types might be interpreted in. Lambda abstraction, which consists of passing from the previous sequent to "$x:A\vdash\lambda y.t:B\to C$", can then be seen to be just to be the syntax of the exponential transposition operation (when considered in the company of all the introduction, elimination, and computation rules).

Answer 2

The presheaf category is Cartesian monoidal and the Yoneda embedding is fully faithful and preserves products and exponentials which exist, so an object $C$ is an exponential of two objects if and only if the image of $C$ under Yoneda is an exponential of the corresponding images. Thus the universal proper for exponentials is presheaves serves well as a substitute for exponentials in the base category in the absence of finite products.

Answer 3

You may be looking for the concept of a closed category. A closed category is a category equipped with an internal hom-functor $[-,-] : \mathsf{C}^\mathrm{op} \times \mathsf{C} \to \mathsf{C}$ (think of $[X,Y]$ as $Y^X$) and a unit object (morally, the initial object) that satisfy a bunch of axioms. Any closed monoidal category has a closed structure; when all exponential objects exist, the monoidal product given by the cartesian product is a closed monoidal structure. So this is a generalization of exponentials when the product in $\mathsf{C}$ may not necessarily exist.