Product

\import Algebra.Monoid
\import Paths

\instance ProductMonoid (M N : Monoid) : Monoid (\Sigma M N)
  | ide => (1, 1)
  | * p q => (p.1 * q.1, p.2 * q.2)
  | ide-left => pmap2 (__,__) ide-left ide-left
  | ide-right => pmap2 (__,__) ide-right ide-right
  | *-assoc => pmap2 (__,__) *-assoc *-assoc

\instance ProductAddMonoid (A B : AddMonoid) : AddMonoid (\Sigma A B)
  | zro => (0, 0)
  | + p q => (p.1 + q.1, p.2 + q.2)
  | zro-left => pmap2 (__,__) zro-left zro-left
  | zro-right => pmap2 (__,__) zro-right zro-right
  | +-assoc => pmap2 (__,__) +-assoc +-assoc

\instance ProductCMonoid (M N : CMonoid) : CMonoid
  | Monoid => ProductMonoid M N
  | *-comm => pmap2 (__,__) *-comm *-comm

\instance ProductAbMonoid (A B : AbMonoid) : AbMonoid
  | AddMonoid => ProductAddMonoid A B
  | +-comm => pmap2 (__,__) +-comm +-comm