IsCommutativeMonoid should use IsMonoid not IsSemigroup

[MatthewDaggitt]

Obviously Maybe a case of mis-subclassing. It leads to unobvious requirements and also makes the record much longer than it needs to be.

agda-stdlib/src/Algebra/Structures.agda

Lines 45 to 51 in a0bdb8e

	record IsCommutativeMonoid {a ℓ} {A : Set a} (≈ : Rel A ℓ)
	(_∙_ : Op₂ A) (ε : A) : Set (a ⊔ ℓ) where
	open FunctionProperties ≈
	field
	isSemigroup : IsSemigroup ≈ _∙_
	identityˡ : LeftIdentity ε _∙_
	comm : Commutative _∙_

[MatthewDaggitt]

Likewise with IsCommutativeSemiring

[gallais]

I think the point of this is that an IsCommutativeX can be used anywhere an X is
expected thanks to subtyping. Not sure whether it'd still be the case if everything was
packed up in a subfield.

That being said, I'm not sure how useful the subtyping aspect is.

[MatthewDaggitt]

Ooh I hadn't considered that. Apologies for my too hasty comment.

Hang on, does that mean identityˡ : LeftIdentity ε _∙_ is a subtype of identity : Identity ε ∙?

[andreasabel]

I could imagine the reason is that in the presence of commutativity, left identity implies right identity, thus, there is less proof obligations to build a commutative monoid.

Unless there are strong reasons for change, I'd advise to leave it as-is. (Maybe add documentation to not fall into the same trap again.)

[MatthewDaggitt]

Unless there are strong reasons for change, I'd advise to leave it as-is. (Maybe add documentation to not fall into the same trap again.)

Agreed.