proposition: Lemma abses_kernel_iso `{Funext} {A E B : AbGroup} (i : A $-> E) (p : E $-> B) `{IsEmbedding i, IsExact (Tr (-1)) _ _ _ i p} : GroupIsomorphism A (ab_kernel p).
proof: Proof. snrapply Build_GroupIsomorphism. - apply (grp_kernel_corec i). rapply cx_isexact. - apply isequiv_surj_emb. 2: rapply (cancelL_mapinO _ (grp_kernel_corec _ _) _). intros [y q]. assert (a : Tr (-1) (hfiber i y)). 1: by rapply isexact_preimage. strip_truncations; destruct a as [a r]. rapply contr_inhabited_hprop. refine (tr (a; _)); cbn. apply path_sigma_hprop; cbn. exact r. Defined.
imports: Basics Types Truncations.Core HSet WildCat Groups.QuotientGroup Groups.ShortExactSequence AbelianGroup AbGroups.Biproduct AbHom Homotopy.ExactSequence Pointed Modalities.ReflectiveSubuniverse