Definition in_same_coset_test (x1 x2 : X) : (Y (x1^-1 * x2)) ≃ in_same_left_coset Y x1 x2. Proof. apply weqimplimpl; unfold in_same_left_coset in *. - intros yx1x2. exists (x1^-1 * x2,, yx1x2); cbn. refine (!assocax X _ _ _ @ _). refine (maponpaths (λ z, z * _) (grrinvax X _) @ _). apply lunax. - intros y. use (transportf (pr1 Y)). + exact (pr11 y). + refine (_ @ maponpaths _ (pr2 y)). refine (_ @ assocax _ _ _ _). refine (_ @ !maponpaths (λ z, z * _) (grlinvax X _)). exact (!lunax _ _). + exact (pr2 (pr1 y)). - apply propproperty. - apply isaprop_in_same_left_coset. Defined.
Require Import UniMath.MoreFoundations.Subtypes.