proposition: Lemma baer_sum_inverse_l `{Univalence} {A B : AbGroup} (E : AbSES B A) : abses_baer_sum E (abses_pullback (- grp_homo_id) E) = point (AbSES B A).
proof: Proof. refine (ap (fun F => abses_baer_sum F (abses_pullback _ E)) (abses_pullback_id E)^ @ _). refine ((baer_sum_distributive_pullbacks grp_homo_id (-grp_homo_id))^ @ _). refine (ap (fun f => abses_pullback f _) (grp_inv_r (G := ab_hom _ _) _) @ _). symmetry; apply abses_pullback_const. Defined.
imports: Basics Types WildCat Pointed.Core AbGroups.AbelianGroup AbGroups.Biproduct AbGroups.AbHom AbSES.Core AbSES.Pullback AbSES.Pushout AbSES.DirectSum Homotopy.HSpace.Core