clarify monoidal assumption in comment

Signed-off-by: Ali Caglayan <[email protected]>

Author: Alizter

theories/Algebra/Categorical/MonoidObject.v

@@ -5,7 +5,9 @@ Require Import abstract_algebra.
 
 (** * Monoids and Comonoids *)
 
-(** Here we define a monoid internal to a monoidal category. Various algebraic theories such as groups and rings may also be internalized, however these specifically require a cartesian monoidal structure. The theory of monoids however has no such requirement and can therefore be developed in much greater generality. This can be used to define a range of objects such as R-algebras, H-spaces, Hopf algebras and more. *)
+(** Here we define a monoid internal to a monoidal category. Note that we don't actually need the full monoidal structure so we assume only the parts we need. This allows us to keep the definitions general between various flavours of monoidal category.
+
+Many algebraic theories such as groups and rings may also be internalized, however these specifically require a cartesian monoidal structure. The theory of monoids however has no such requirement and can therefore be developed in much greater generality. This can be used to define a range of objects such as R-algebras, H-spaces, Hopf algebras and more. *)
 
 (** * Monoid objects *)