Definition opposite_commrig (X : commrig) : commrig := (pr1 (X⁰),, (pr2 (X⁰) ,, λ x y, rigcomm2 X y x)).
Require Import UniMath.Algebra.Groups. Require Import UniMath.MoreFoundations.Sets. Require Import UniMath.MoreFoundations.Orders.