feat(category_theory): finite products give a monoidal structure

[semorrison]

This is an alternative to @cipher1024's #1337, defining cartesian categories.

In this approach, we just use has_finite_products C to express that C is cartesian, and then directly give the construction of a monoidal structure on C from this. I think the construction I given here is pretty close to minimal --- we say only what needs to be said, and all the theorems are proved by the simp lemmas provided by the limits library!

Again, this needs some documentation, assuming it's agreed this is the right path.

[cipher1024]

I think I saw somewhere that you already considered using bundled categories instead of a type class. Do you have a link to a conversation about it? This seems like a situation where bundled categories would simplify things.

[semorrison]

I don't recall any particular place where this choice was analysed carefully. Essentially, the current design is optimised for talking about existing bundled algebraic gadgets, but that have interesting structure between instances (e.g. tensor products, kernels, etc.). The reason it works well for this is that the category structures all live in typeclasses, so the primary objects you talk about are the objects of the category (e.g. Top for bundled topological spaces). On the other hand, it is slightly clunky for talking about relationships between abstract categories (for which we would instead want to bundle the categories).

I don't think there's any particular obstacle to also developing bundled categories alongside what is already in mathlib. However I haven't felt much need for it so far; I'd be curious to hear why you think they would have been easier here.

[cipher1024]

The main reason I'd consider it is for the universe level issue with type class resolution. It might be worth considering type classes for small categories only (are all the interesting algebraic instances small categories?) and bundled categories for the rest. That turns variable (C : Type u) [𝒞 : category.{v} C] include 𝒞 into variable (C : Cat.{u v}). In the case of monoidal categories, it also brings down the number of instance you have to assume by one and the class monoidal_category can be resolved without ambiguity because both universes are specified in Cat.{u v}.

[semorrison]

I see. Actually, it's the other way round --- the interesting algebraic instances are all large categories, but I don't think that causes any problem. I'll think about this, but I'm also not really sure where to investigating!

[semorrison]

There's nothing particularly more that I want to add now; hopefully this is pretty straightforward.

[cipher1024]

It looks good to me