{A B : Group} (f : A $-> B) : IsExact purely (grp_trivial_rec A) f <-> IsEmbedding f. 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.
Require Import Basics Types. Require Import Truncations.Core. Require Import WildCat.Core Pointed. Require Import Groups.Group Groups.Subgroup Groups.Kernel. Require Import Homotopy.ExactSequence Modalities.Identity.