Definition subrigtosubsetswith2binop (X : rig) : subrig X → @subsetswith2binop X := λ A, make_subsetswith2binop (pr1 A) (pr1 (pr1 (pr2 A)) ,, pr1 (pr2 (pr2 A))).
Require Import UniMath.Algebra.Groups. Require Import UniMath.MoreFoundations.Sets. Require Import UniMath.MoreFoundations.Orders.