Lemma iscommcarrier {X : abmonoid} (A : submonoid X) : iscomm (@op A). Proof. intros a a'. apply (invmaponpathsincl _ (isinclpr1carrier A)). simpl. apply (pr2 (pr2 X)). Qed.
Require Import UniMath.MoreFoundations.Sets. Require Import UniMath.MoreFoundations.Orders. Require Import UniMath.Algebra.Monoids2.