(g : G) : { g' : G & in_coset g g'} <~> H. Proof. simple refine (equiv_adjointify _ _ _ _). - intros [? [h ?]]; exact h. - intros h; exists (incl h^ @ g); exists h; simpl. abstract (rewrite inv_pp, grouphom_V, inv_V, concat_p_Vp; reflexivity). - intros h; reflexivity. - intros [g' [h p]]. apply path_sigma_hprop; simpl. refine ((grouphom_V incl h @@ 1) @ _). apply moveR_Vp, moveL_pM. exact (p^). Defined.
Require Import Basics Types. Require Import Pointed. Require Import Truncations.Core Truncations.Connectedness. Require Import Homotopy.ClassifyingSpace. Require Import Algebra.Groups. Require Import WildCat.