proposition: Lemma commrigtocommringcomm2 (X : commrig) : iscomm (rigtoringop2 X).
proof: Proof. unfold iscomm. apply (setquotuniv2prop _ (λ x x', _ = _)). intros x x'. change (paths (setquotpr (eqrelrigtoring X) (rigtoringop2int X x x')) (setquotpr (eqrelrigtoring X) (rigtoringop2int X x' x))). apply (maponpaths (setquotpr (eqrelrigtoring X))). unfold rigtoringop2int. set (cm1 := rigcomm1 X). set (cm2 := rigcomm2 X). apply pathsdirprod. - rewrite (cm2 (pr1 x) (pr1 x')). rewrite (cm2 (pr2 x) (pr2 x')). apply idpath. - rewrite (cm2 (pr1 x) (pr2 x')). rewrite (cm2 (pr2 x) (pr1 x')). apply cm1. Defined.
imports: UniMath.Algebra.Groups UniMath.MoreFoundations.Sets UniMath.MoreFoundations.Orders UniMath.Algebra.Monoids