2
$\begingroup$

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.

$\endgroup$
4
  • $\begingroup$ Do you need a definition of the exponential function $y=a^x$ or of the exponentiation $y=x^n$ ? $\endgroup$ Jun 16, 2016 at 14:43
  • 1
    $\begingroup$ @EmilioNovati en.wikipedia.org/wiki/Exponential_object $\endgroup$ Jun 16, 2016 at 14:55
  • $\begingroup$ OK. I delete my answer that is not pertinent. $\endgroup$ Jun 16, 2016 at 14:56
  • $\begingroup$ Sorry; perhaps I should make it more obvious, that this question is about category theory. $\endgroup$ Jun 16, 2016 at 14:57

3 Answers 3

4
$\begingroup$

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

$\endgroup$
1
  • $\begingroup$ Ah, yes. Your comments about type theory sound very reasonable. Actually, the notion of a closed category seems to be at least a good approximation of what I had in mind! $\endgroup$ Jun 17, 2016 at 8:20
2
$\begingroup$

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.

$\endgroup$
1
$\begingroup$

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.

$\endgroup$
3
  • $\begingroup$ This is not quite what I had in mind, I believe, because we still need binary products to specify the monoidal structure. - I literally meant exponentials, not internal-homs in general. $\endgroup$ Jun 16, 2016 at 15:00
  • $\begingroup$ @StefanPerko - You need products in $\mathbf{Cat}$, but you don't need $\mathsf{C}$ to have products to have a monoidal product. $\endgroup$ Jun 17, 2016 at 7:49
  • $\begingroup$ @MaliceVidrine Again, morally I want the cartesian closed structure, but without the binary products. $\endgroup$ Jun 17, 2016 at 8:18

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .