Definition commrig_univalence_weq1 : commrig ≃ commrig' := weqtotal2asstol (λ X : setwith2binop, isrigops (@op1 X) (@op2 X)) (λ y : (∑ (X : setwith2binop), isrigops (@op1 X) (@op2 X)), iscomm (@op2 (pr1 y))).
Require Import UniMath.Algebra.Groups. Require Import UniMath.MoreFoundations.Sets. Require Import UniMath.MoreFoundations.Orders.