Lemma rigtoringrunit2 (X : rig) : isrunit (rigtoringop2 X) (rigtoringunel2 X). Proof. unfold isrunit. apply (setquotunivprop _ (λ x, _ = _)). intro x. change (setquotpr (eqrelrigtoring X) (rigtoringop2int X x (rigtoringunel2int X)) = setquotpr (eqrelrigtoring X) x). apply (maponpaths (setquotpr (eqrelrigtoring X))). unfold rigtoringop2int. simpl. induction x as [ x1 x2 ]. simpl. set (ru1 := rigrunax1 X). set (ru2 := rigrunax2 X). set (lu1 := riglunax1 X). set (mx0 := rigmultx0 X). apply pathsdirprod. - rewrite (ru2 x1). rewrite (mx0 x2). apply (ru1 x1). - rewrite (ru2 x2). rewrite (mx0 x1). apply (lu1 x2). Qed.
Require Import UniMath.Algebra.Groups. Require Import UniMath.MoreFoundations.Sets. Require Import UniMath.MoreFoundations.Orders.