Definition in_same_right_coset_prop : X → X → hProp. Proof. intros x1 x2. use make_hProp. + exact (in_same_right_coset Y x1 x2). + apply isaprop_in_same_right_coset. Defined.
Require Import UniMath.MoreFoundations.Subtypes.