Monoidal Groupoid

[JacquesCarette]

In my 'negative thinking' exploration, it has become clear that I need to enrich over a monoidal groupoid too [this is how to get Setoid, since otherwise one only gets Poset]. The question here is how to 'encode' monoidal groupoid. For using them for enriching, there are two obvious ways:

1. {C : Category} (G : IsGroupoid C) (M : Monoidal C)
2. {C : Category} (MG : MonoidalGroupoid C) where MonoidalGroupoid is the obvious record with 2 fields.

They are both 'equivalent' in some ways, so the question is one of usability / expectations. Opinions?

[sstucki]

A third option would be:

3. (MG : MonoidalGroupoid) where everything is in one record (i.e. MonoidalGroupoid "extends" Groupoid with another field).

I'm tempted to also add a MonoidalCategory record. That would simplify the parametrization of the various enriched modules quite a bit and eliminate duplicate code that just opens and imports the same fields from the two records over and over.

[JacquesCarette]

Indeed. Sometimes it's useful to be able to say you have 2 monoidal structures on the same category (which is what option 1 makes easiest), but sometimes you have a unique one, where option 3 is likely simplest.

[HuStmpHrrr]

I'd prefer option 2. in option 1, G and M are disjoint so option 2 makes no harm. in addition, it's clear to write. we can add another definition describing option 3, so option 2 seems the right solution.

[JacquesCarette]

So option 2 is basically along the lines of "a category C along with extra structure that makes it into a Monoidal Groupoid" while option 3 is "a Monoidal Groupoid". Option 2 is crucial when you want to talk about 2 different structures on the same category, while option 3 makes sense when you really are not all that interested in the category itself, but all of the structure.

I think we should provide both! And that, given our current naming conventions, option 2 should be called IsMonoidalGroupoid and option 3 MonoidalGroupoid. And both ought to be defined in the same file.

[sstucki]

I think we should provide both! And that, given our current naming conventions, option 2 should be called IsMonoidalGroupoid and option 3 MonoidalGroupoid. And both ought to be defined in the same file.

Sounds good to me!