{M N P : Monoid} (f : MonoidHomomorphism P M) (g : MonoidHomomorphism P N) : MonoidHomomorphism P (mnd_prod M N). Proof. snrapply Build_MonoidHomomorphism. 2: split. - exact (fun x => (f x, g x)). - intros x y; snrapply path_prod; nrapply mnd_homo_op. - snrapply path_prod; nrapply mnd_homo_unit. 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.