proposition: Lemma rigtoringrunit2 (X : rig) : isrunit (rigtoringop2 X) (rigtoringunel2 X).
proof: Proof. unfold isrunit. apply (setquotunivprop _ (λ x, _ = _)). intro x. change (paths (setquotpr (eqrelrigtoring X) (rigtoringop2int X x (rigtoringunel2int X))) (setquotpr (eqrelrigtoring X) x)). apply (maponpaths (setquotpr (eqrelrigtoring X))). unfold rigtoringop2int. simpl. destruct 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). Defined.
imports: UniMath.Algebra.Groups UniMath.MoreFoundations.Sets UniMath.MoreFoundations.Orders UniMath.Algebra.Monoids