`{Univalence} {A B : AbGroup} (E : AbSES B A) : abses_baer_sum E (abses_pullback (- grp_homo_id) E) = point (AbSES B A). 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.
Require Import Basics Types. Require Import WildCat Pointed.Core. Require Import AbGroups.AbelianGroup AbGroups.Biproduct AbGroups.AbHom. Require Import AbSES.Core AbSES.Pullback AbSES.Pushout AbSES.DirectSum. Require Import Homotopy.HSpace.Core.