\import Algebra.Group
\import Algebra.Monoid.Product
\import Paths

\instance ProductGroup (G H : Group) : Group
  | Monoid => ProductMonoid G H
  | inverse p => (inverse p., inverse p.)
  | inverse-left => pmap2 (__,__) inverse-left inverse-left
  | inverse-right => pmap2 (__,__) inverse-right inverse-right

\instance ProductAddGroup (A B : AddGroup) : AddGroup
  | AddMonoid => ProductAddMonoid A B
  | negative p => (negative p., negative p.)
  | negative-left => pmap2 (__,__) negative-left negative-left
  | negative-right => pmap2 (__,__) negative-right negative-right

\instance ProductCGroup (G H : CGroup) : CGroup
  | Group => ProductGroup G H
  | CMonoid => ProductCMonoid G H

\instance ProductAbGroup (A B : AbGroup) : AbGroup
  | AddGroup => ProductAddGroup A B
  | AbMonoid => ProductAbMonoid A B