\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