Strict monoidal categories are strict categories

[anshwad10]

No description provided.

[anshwad10]

This will fix #753

[anshwad10]

@ecavallo could you take a look at this as well?

[ecavallo]

The change looks good, but I don't know what the intent behind this definition was in the first place (since it is barely used). There are two possibilities here:

1. A StrictMonCategory is a monoidal {strict category}. This is the interpretation taken by this PR.
2. A StrictMonCategory is a MonoidalCategory where the coherence isomorphisms are identities. This the interpretation suggested by @anuyts in Strict monoidal categories lack coherence laws #753.

Opinions from @barrettj12 or @anuyts? If there are no objections I will just merge.

[anuyts]

I think this is (equally) wrong before and after. The unit and associativity laws should concern the entire functors, not just their object part. The current formulation is only correct on thin/posetal categories.

[ecavallo]

Thanks, I completely overlooked that.

[anuyts]

Additionally, in the light of #753 cited by @anshwad10 , I think we need triangle & pentagon coherence laws since we cannot assume that the type of objects is an hset.

[ecavallo]

As it stands the PR does assume the type of objects is an h-set, as part of the definition of IsMonoid. This is what I meant by strict category in my option "1".

[anshwad10]

Yeah, I had forgotten to axioms for the morphisms too (so I added it now). I think strict monoidal categories should have underlying strict categories, which is why I required the type of objects to be a set instead of assuming more coherence laws.

[anuyts]

Ok, that makes sense.

[ecavallo]

Then I will merge! Thanks all.