proposition: Lemma abmonoidshombinop_ismonoidfun {X Y : abmonoid} (f g : monoidfun X Y) : @ismonoidfun X Y (λ x : pr1 X, (pr1 f x * pr1 g x)%multmonoid).
proof: Proof. use make_ismonoidfun. - use make_isbinopfun. intros x x'. cbn. rewrite (pr1 (pr2 f)). rewrite (pr1 (pr2 g)). rewrite (assocax Y). rewrite (assocax Y). use maponpaths. rewrite <- (assocax Y). rewrite <- (assocax Y). use (maponpaths (λ y : Y, (y * (pr1 g x'))%multmonoid)). use (commax Y). - use (pathscomp0 (maponpaths (λ h : Y, (pr1 f (unel X) * h)%multmonoid) (monoidfununel g))). rewrite runax. exact (monoidfununel f). Qed.
imports: UniMath.Algebra.BinaryOperations UniMath.MoreFoundations.Subtypes UniMath.MoreFoundations.Sets UniMath.MoreFoundations.Orders