`{Funext} {A E B : AbGroup@{u}} (f : A $-> E) (g : GroupHomomorphism E B) `{IsSurjection g, IsExact (Tr (-1)) _ _ _ f g} : GroupIsomorphism (ab_cokernel f) B. Proof. snrapply Build_GroupIsomorphism. - snrapply (quotient_abgroup_rec _ _ g). intros e; rapply Trunc_rec; intros [a p]. refine (ap _ p^ @ _). rapply cx_isexact. - apply isequiv_surj_emb. 1: rapply cancelR_conn_map. apply isembedding_isinj_hset. srapply Quotient_ind2_hprop; intros x y. intro p. apply qglue; cbn. refine (isexact_preimage (Tr (-1)) _ _ (-x + y) _). refine (grp_homo_op _ _ _ @ _). rewrite grp_homo_inv. apply grp_moveL_M1^-1. exact p^. 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.