An exponential object B^A is often defined in a category with *all* binary products _×A

[MiddleAdjunction]

As hinted by a comment in the module, the definition of exponential objects in Categories.Object.Exponential seems odd. It does not follow Wikipedia or nLab.
An exponential object B^A is often defined in a category where all binary products _×A exist, not only B^A×A.
Changing the definition to include _×A further simplifies the definition of other fields by avoiding the need for an explicit Product parameter. Is there any specific reason for the current definition?

[JacquesCarette]

It was already like that in copumpkin's version, and this is a straight port of that part.

As sometimes happens in category theory, a number of 'common' definitions are done in a convenient setting, which is far from the minimal setting. Asking for all binary products is overkill.

Having said, an alternate definition of exponential object that is specialized for that case would be a welcome addition. Alternatively, a theorem showing that if a category has exponential objects as defined here, it has all binary products, would go a long way to convince me that the current definition is overly pedantic.

[MiddleAdjunction]

As sometimes happens in category theory, a number of 'common' definitions are done in a convenient setting, which is far from the minimal setting. Asking for all binary products is overkill.

In this case, needing all binary products with A seems natural. Currently, λg and eval work on different products: eval works with the product supplied via Exponential and λg works with the product supplied as a parameter.

Alternatively, a theorem showing that if a category has exponential objects as defined here, it has all binary products, would go a long way to convince me that the current definition is overly pedantic.

Currently, if a category has an exponential B^A, then it also has λg : (X×A : Product X A) → (Product.A×B X×A ⇒ B) → (X ⇒ B^A) for all X : Obj. In other words, λg is only defined for objects with _×A. The key question is whether this partiality is desirable.

Having said, an alternate definition of exponential object that is specialized for that case would be a welcome addition.

If you decide to keep the current partial/minimal definition of exponential, in which module do you want the conventional definition (as in Wikipedia or nLab) of an exponential object to go? Some other definitions like that of CartesianClosed may also need to be adjusted and/or duplicated.

On that note, the fact that exponential objects in a cartesian closed setting carry their own products, that are not definitionally equal to the cartesian product, is another annoyance. It leads me to think having a parametric definition of exponential objects such as Exponential (A B : Obj) ([_×A] : (C : Obj) → Product C A) : Set ... may be the right design.

Alternatively, one can define [_×A] : (C : Obj) → Product C A as a field for Exponential. However, then in cases like CartesianClosed, either definitional equality of the products in exponentials and the cartesian product needs to be asserted by an explicit proof field or entirely ignore by using isomorphisms as in repack. Both designs go against the spirit of the library that includes, for instance, sym-assoc to keep definitional equality.

[sstucki]

I agree the current definition is a bit odd and hard to work with. But I'm curious: do you have a concrete use case in mind for the alternative definition? I'm asking because, if you just want a more convenient way to work with CCCs, we already have support for that in Categories.Category.CartesianClosed.Canonical. But maybe that's not what you want?

[MiddleAdjunction]

@sstucki Thank you for pointing me to Categories.Category.CartesianClosed.Canonical. I am simply porting/comparing a few categorical proofs including between different mechanisations.

About the canonical interface (possibly should be a separate note), the field curry-resp-≈ seems redundant:

curry-resp-≈' f≈g = curry-unique (eval-comp ○ f≈g)