{E B : AbGroup@{u}} (p : E $-> B) `{IsSurjection p} : AbSES B (ab_kernel p). Proof. srapply (Build_AbSES E _ p). 1: exact (subgroup_incl _). 1: exact _. snrapply Build_IsExact. - apply phomotopy_homotopy_hset. intros [e q]; cbn. exact q. - 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.