proposition: Lemma iff_grp_isexact_isembedding {A B : Group} (f : A $-> B) : IsExact purely (grp_trivial_rec A) f <-> IsEmbedding f.
proof: Proof. split. - intros ex b. apply hprop_inhabited_contr; intro a. rapply (contr_equiv' grp_trivial). exact ((equiv_grp_hfiber f b a)^-1 oE pequiv_cxfib). - intro isemb_f. exists (grp_iscomplex_trivial f). intros y; rapply contr_inhabited_hprop. exists tt; apply path_ishprop. Defined.
imports: Basics Types Truncations.Core WildCat.Core Pointed Groups.Group Groups.Subgroup Groups.Kernel Homotopy.ExactSequence Modalities.Identity