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