Lemma abmonoidshombinop_assoc {X Y : abmonoid} (f g h : monoidfun X Y) : abmonoidshombinop (abmonoidshombinop f g) h = abmonoidshombinop f (abmonoidshombinop g h). Proof. use monoidfun_paths. use funextfun. intros x. use assocax. Qed.
Require Import UniMath.MoreFoundations.Sets. Require Import UniMath.MoreFoundations.Orders. Require Import UniMath.Algebra.Monoids2.