`{Funext} {A E B : AbGroup} (i : A $-> E) (p : E $-> B) `{IsEmbedding i, IsExact (Tr (-1)) _ _ _ i p} : GroupIsomorphism A (ab_kernel p). 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.
Require Import Basics Types Truncations.Core. Require Import HSet WildCat. Require Import Groups.QuotientGroup Groups.ShortExactSequence. Require Import AbelianGroup AbGroups.Biproduct AbHom. Require Import Homotopy.ExactSequence Pointed. Require Import Modalities.ReflectiveSubuniverse.