`{Univalence} {A E : AbGroup@{u}} (i : A $-> E) `{IsEmbedding i} : AbSES (QuotientAbGroup E (grp_image_embedding i)) A. Proof. srapply (Build_AbSES E i). 1: exact grp_quotient_map. 1: exact _. srapply Build_IsExact. - srapply phomotopy_homotopy_hset. intro x. apply qglue; cbn. exists (-x). exact (grp_homo_inv _ _ @ (grp_unit_r _)^). - snrapply (conn_map_homotopic (Tr (-1)) (B:=grp_kernel (@grp_quotient_map E _))). + exact (grp_kernel_quotient_iso _ o ab_image_in_embedding i). + intro a. by rapply (isinj_embedding (subgroup_incl _)). + rapply conn_map_isequiv. 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.