Definition rigtoringop1int (X : rig) : binop (X × X) := λ x x', pr1 x + pr1 x' ,, pr2 x + pr2 x'.
Require Import UniMath.Algebra.Groups. Require Import UniMath.MoreFoundations.Sets. Require Import UniMath.MoreFoundations.Orders.