Definition abgr_univalence_weq3 (X Y : abgr) : (pr1 (make_abgr' X) = pr1 (make_abgr' Y)) ≃ (monoidiso X Y) := gr_univalence (pr1 (make_abgr' X)) (pr1 (make_abgr' Y)).
Require Import UniMath.MoreFoundations.Orders. Require Import UniMath.MoreFoundations.Subtypes.