Lemma abmonoidshombinop_ismonoidfun {X Y : abmonoid} (f g : monoidfun X Y) : @ismonoidfun X Y (λ x : pr1 X, pr1 f x + pr1 g x). 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')). use (commax Y). - refine (maponpaths (λ h : Y, pr1 f 0 + h) (monoidfununel g) @ _). rewrite runax. exact (monoidfununel f). Qed.
Require Import UniMath.MoreFoundations.Sets. Require Import UniMath.MoreFoundations.Orders. Require Import UniMath.Algebra.Monoids2.