Monoid -> Monoid -> Monoid. Proof. intros M N. snrapply (Build_Monoid (M * N)). 3: repeat split. - intros [m1 n1] [m2 n2]. exact (m1 * m2, n1 * n2). - exact (mon_unit, mon_unit). - exact _. - intros x y z; snrapply path_prod; nrapply mnd_assoc. - intros x; snrapply path_prod; nrapply mnd_unit_l. - intros x; snrapply path_prod; nrapply mnd_unit_r. Defined.
Require Import Basics.Overture Basics.Tactics Basics.Equivalences Basics.Trunc. Require Import Types.Sigma Types.Forall Types.Prod. Require Import WildCat.Core WildCat.Induced WildCat.Equiv WildCat.Universe Require Import (notations) Classes.interfaces.canonical_names.