proposition: Lemma projection_split_to_kernel_beta {B A : AbGroup} (E : AbSES B A) {s : B $-> E} (h : (projection _) $o s == idmap) : (projection_split_to_kernel E h) $o (inclusion _) == grp_cxfib cx_isexact.
proof: Proof. intro a. apply path_sigma_hprop; cbn. apply grp_cancelL1. refine (ap (fun x => - s x) _ @ _). 1: rapply cx_isexact. exact (ap _ (grp_homo_unit _) @ negate_mon_unit). Defined.
imports: Basics Types Truncations.Core HSet WildCat Groups.QuotientGroup Groups.ShortExactSequence AbelianGroup AbGroups.Biproduct AbHom Homotopy.ExactSequence Pointed Modalities.ReflectiveSubuniverse