Lemma rigtoringassoc2 (X : rig) : isassoc (rigtoringop2 X). Proof. unfold isassoc. apply (setquotuniv3prop _ (λ x x' x'', _ = _)). intros x x' x''. change (setquotpr (eqrelrigtoring X) (rigtoringop2int X (rigtoringop2int X x x') x'') = setquotpr (eqrelrigtoring X) (rigtoringop2int X x (rigtoringop2int X x' x''))). apply (maponpaths (setquotpr (eqrelrigtoring X))). unfold rigtoringop2int. simpl. set (rd := rigrdistr X). set (ld := rigldistr X). set (cm1 := rigcomm1 X). set (as1 := rigassoc1 X). set (as2 := rigassoc2 X). set (rr := abmonoidoprer (rigop1axs X)). apply pathsdirprod. rewrite (rd _ _ (pr1 x'')). rewrite (rd _ _ (pr2 x'')). rewrite (ld _ _ (pr1 x)). rewrite (ld _ _ (pr2 x)). induction (as2 (pr1 x) (pr1 x') (pr1 x'')). induction (as2 (pr1 x) (pr2 x') (pr2 x'')). induction (as2 (pr2 x) (pr1 x') (pr2 x'')). induction (as2 (pr2 x) (pr2 x') (pr1 x'')). induction (cm1 (pr2 x * pr2 x' * pr1 x'') (pr2 x * pr1 x' * pr2 x'')). rewrite (rr _ (pr2 x * pr2 x' * pr1 x'') (pr1 x * pr2 x' * pr2 x'') _). apply idpath. rewrite (rd _ _ (pr1 x'')). rewrite (rd _ _ (pr2 x'')). rewrite (ld _ _ (pr1 x)). rewrite (ld _ _ (pr2 x)). induction (as2 (pr1 x) (pr1 x') (pr2 x'')). induction (as2 (pr1 x) (pr2 x') (pr1 x'')). induction (as2 (pr2 x) (pr1 x') (pr1 x'')). induction (as2 (pr2 x) (pr2 x') (pr2 x'')). induction (cm1 (pr2 x * pr2 x' * pr2 x'') (pr2 x * pr1 x' * pr1 x'')). rewrite (rr _ (pr1 x * pr2 x' * pr1 x'') (pr2 x * pr2 x' * pr2 x'') _). apply idpath. Qed.
Require Import UniMath.Algebra.Groups. Require Import UniMath.MoreFoundations.Sets. Require Import UniMath.MoreFoundations.Orders.