Lemma isassocquot {X : monoid} (R : binopeqrel X) : isassoc (@op (setwithbinopquot R)). Proof. intros a b c. apply (setquotuniv3prop R (λ x x' x'' : setwithbinopquot R, make_hProp _ (setproperty (setwithbinopquot R) ((x * x') * x'') (x * (x' * x''))))). intros x x' x''. apply (maponpaths (setquotpr R) (assocax X x x' x'')). Qed.
Require Import UniMath.MoreFoundations.Subtypes. Require Import UniMath.MoreFoundations.Sets.