-record isMonoid (SS:SemiGroup) (e:SS) : Prop ≝
- { e_is_left_unit: is_left_unit SS e;
- e_is_right_unit: is_right_unit SS e
+record PreMonoid : Type ≝
+ { magma:> Magma;
+ e: magma
+ }.
+
+notation < "M" for @{ 'pmmagma $M }.
+interpretation "premonoid magma coercion" 'pmmagma M =
+ (cic:/matita/algebra/monoids/magma.con M).
+
+record isMonoid (M:PreMonoid) : Prop ≝
+ { is_semi_group: isSemiGroup M;
+ e_is_left_unit:
+ is_left_unit (mk_SemiGroup ? is_semi_group) (e M);
+ e_is_right_unit:
+ is_right_unit (mk_SemiGroup ? is_semi_group) (e M)