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