Require Export Monoid.

Set Implicit Arguments.
Unset Strict Implicit.


Section group_laws.

Variable A : Monoid.

Definition Inverses_rel (x y : A) := x +_M y =_S Munit A.

Variable inv : Map A A.

Definition Group_invl := ∀ x : A, Inverses_rel (inv x) x.

Definition Group_invr := ∀ x : A, Inverses_rel x (inv x).

End group_laws.

Structure Group : Type :=
  {Gmon :> Monoid;
   Ginv : Map Gmon Gmon;
   Prf_ginv_l : Group_invl Ginv;
   Prf_ginv_r : Group_invr Ginv}.