proposition: Lemma iscommquot {X : abmonoid} (R : binopeqrel X) : iscomm (@op (setwithbinopquot R)).
proof: Proof. intros. set (X0 := setwithbinopquot R). intros x x'. apply (setquotuniv2prop R (λ x x' : X0, make_hProp _ (setproperty X0 (op x x') (op x' x)))). intros x0 x0'. apply (maponpaths (setquotpr R) ((commax X) x0 x0')). Defined.
imports: UniMath.Algebra.BinaryOperations UniMath.MoreFoundations.Subtypes UniMath.MoreFoundations.Sets UniMath.MoreFoundations.Orders