Definition gr_univalence_weq1 : gr ≃ gr' := weqtotal2asstol (λ Z : setwithbinop, ismonoidop (@op Z)) (λ y : (∑ (x : setwithbinop), ismonoidop (@op x)), invstruct (@op (pr1 y)) (pr2 y)).
Require Import UniMath.MoreFoundations.Subtypes.