Definition abgr_univalence_weq2 (X Y : abgr) : (make_abgr' X = make_abgr' Y) ≃ (pr1 (make_abgr' X) = pr1 (make_abgr' Y)). Proof. use subtypeInjectivity. intros w. use isapropiscomm. Defined.
Require Import UniMath.MoreFoundations.Orders. Require Import UniMath.MoreFoundations.Subtypes.