Lemma isrigquot {X : rig} (R : @rigeqrel X) : isrigops (@op1 (setwith2binopquot R)) (@op2 (setwith2binopquot R)). Proof. intros. split. - exists (isabmonoidquot (addabmonoideqrel R) ,, ismonoidquot (multmonoideqrel R)). set (opp1 := @op1 (setwith2binopquot R)). set (opp2 := @op2 (setwith2binopquot R)). set (zr := setquotpr R (@rigunel1 X)). split. + apply (setquotunivprop R (λ x , make_hProp _ (setproperty (setwith2binopquot R) (opp2 zr x) zr))). intro x. apply (maponpaths (setquotpr R) (rigmult0x X x)). + apply (setquotunivprop R (λ x , make_hProp _ (setproperty (setwith2binopquot R) (opp2 x zr) zr))). intro x. apply (maponpaths (setquotpr R) (rigmultx0 X x)). - set (opp1 := @op1 (setwith2binopquot R)). set (opp2 := @op2 (setwith2binopquot R)). split. + unfold isldistr. apply (setquotuniv3prop R (λ x x' x'', make_hProp _ (setproperty (setwith2binopquot R) (opp2 x'' (opp1 x x')) (opp1 (opp2 x'' x) (opp2 x'' x'))))). intros x x' x''. apply (maponpaths (setquotpr R) (rigldistr X x x' x'')). + unfold isrdistr. apply (setquotuniv3prop R (λ x x' x'', make_hProp _ (setproperty (setwith2binopquot R) (opp2 (opp1 x x') x'') (opp1 (opp2 x x'') (opp2 x' x''))))). intros x x' x''. apply (maponpaths (setquotpr R) (rigrdistr X x x' x'')). Defined.
Require Import UniMath.Algebra.Groups. Require Import UniMath.MoreFoundations.Sets. Require Import UniMath.MoreFoundations.Orders.