Lemma rigtoringop2comp (X : rig) : iscomprelrelfun2 (eqrelrigtoring X) (eqrelrigtoring X) (rigtoringop2int X). Proof. intros. apply iscomprelrelfun2if. - intros xx xx' aa. simpl. apply @hinhfun. intro tt1. induction tt1 as [ x0 e ]. exists (x0 * pr2 aa + x0 * pr1 aa). set (rd := rigrdistr X). set (cm1 := rigcomm1 X). set (as1 := rigassoc1 X). set (rr := abmonoidoprer (rigop1axs X)). rewrite (cm1 (pr1 xx * pr1 aa) (pr2 xx * pr2 aa)). rewrite (rr _ (pr1 xx * pr1 aa) (pr1 xx' * pr2 aa) _). rewrite (cm1 (pr2 xx * pr2 aa) (pr1 xx' * pr2 aa)). induction (rd (pr1 xx) (pr2 xx') (pr1 aa)). induction (rd (pr1 xx') (pr2 xx) (pr2 aa)). rewrite (rr ((pr1 xx' + pr2 xx) * pr2 aa) ((pr1 xx + pr2 xx') * pr1 aa) (x0 * pr2 aa) (x0 * pr1 aa)). induction (rd (pr1 xx' + pr2 xx) x0 (pr2 aa)). induction (rd (pr1 xx + pr2 xx') x0 (pr1 aa)). rewrite (cm1 (pr1 xx' * pr1 aa) (pr2 xx' * pr2 aa)). rewrite (rr _ (pr1 xx' * pr1 aa) (pr1 xx * pr2 aa) _). rewrite (cm1 (pr2 xx' * pr2 aa) (pr1 xx * pr2 aa)). induction (rd (pr1 xx') (pr2 xx) (pr1 aa)). induction (rd (pr1 xx) (pr2 xx') (pr2 aa)). rewrite (rr ((pr1 xx + pr2 xx') * pr2 aa) ((pr1 xx' + pr2 xx) * pr1 aa) (x0 * pr2 aa) (x0 * pr1 aa)). induction (rd (pr1 xx + pr2 xx') x0 (pr2 aa)). induction (rd (pr1 xx' + pr2 xx) x0 (pr1 aa)). induction e. apply idpath. - intros aa xx xx'. simpl. apply @hinhfun. intro tt1. induction tt1 as [ x0 e ]. exists (pr1 aa * x0 + pr2 aa * x0). set (ld := rigldistr X). set (cm1 := rigcomm1 X). set (as1 := rigassoc1 X). set (rr := abmonoidoprer (rigop1axs X)). rewrite (rr _ (pr2 aa * pr2 xx) (pr1 aa * pr2 xx') _). induction (ld (pr1 xx) (pr2 xx') (pr1 aa)). induction (ld (pr2 xx) (pr1 xx') (pr2 aa)). rewrite (rr _ (pr2 aa * (pr2 xx + pr1 xx')) (pr1 aa * x0) _). induction (ld (pr1 xx + pr2 xx') x0 (pr1 aa)). induction (ld (pr2 xx + pr1 xx') x0 (pr2 aa)). rewrite (rr _ (pr2 aa * pr2 xx') (pr1 aa * pr2 xx) _). induction (ld (pr1 xx') (pr2 xx) (pr1 aa)). induction (ld (pr2 xx') (pr1 xx) (pr2 aa)). rewrite (rr _ (pr2 aa * (pr2 xx' + pr1 xx)) (pr1 aa * x0) _). induction (ld (pr1 xx' + pr2 xx) x0 (pr1 aa)). induction (ld (pr2 xx' + pr1 xx) x0 (pr2 aa)). rewrite (cm1 (pr2 xx) (pr1 xx')). rewrite (cm1 (pr2 xx') (pr1 xx)). induction e. apply idpath. Qed.
Require Import UniMath.Algebra.Groups. Require Import UniMath.MoreFoundations.Sets. Require Import UniMath.MoreFoundations.Orders.