Lemma commrigtocommringcomm2 (X : commrig) : iscomm (rigtoringop2 X). Proof. unfold iscomm. apply (setquotuniv2prop _ (λ x x', _ = _)). intros x x'. change (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. Qed.
Require Import UniMath.Algebra.Groups. Require Import UniMath.MoreFoundations.Sets. Require Import UniMath.MoreFoundations.Orders.