Definition gr_univalence_weq3 (X Y : gr) : ((gr'_to_monoid (make_gr' X)) = (gr'_to_monoid (make_gr' Y))) ≃ (monoidiso X Y) := monoid_univalence (gr'_to_monoid (make_gr' X)) (gr'_to_monoid (make_gr' Y)).
Require Import UniMath.MoreFoundations.Subtypes.