Definition gr_univalence_weq2 (X Y : gr) : ((make_gr' X) = (make_gr' Y)) ≃ ((gr'_to_monoid (make_gr' X)) = (gr'_to_monoid (make_gr' Y))). Proof. use subtypeInjectivity. intros w. use isapropinvstruct. Defined.
Require Import UniMath.MoreFoundations.Subtypes.