`{Univalence} {A B : AbGroup} : abses_pushout_pmap (B:=B) (@grp_homo_id A) ==* @pmap_idmap (AbSES B A). Proof. srapply Build_pHomotopy. 1: apply abses_pushout_id. refine (_ @ (concat_p1 _)^). nrapply (ap equiv_path_abses_iso (x:=abses_pushout_component3_id' (abses_morphism_id pt) _)). apply path_sigma_hprop. apply equiv_path_groupisomorphism. by rapply Quotient_ind_hprop. Defined.
Require Import Basics Types Truncations.Core. Require Import WildCat Pointed.Core Homotopy.ExactSequence HIT.epi. Require Import Modalities.ReflectiveSubuniverse. Require Import AbelianGroup AbPushout AbHom AbGroups.Biproduct. Require Import AbSES.Core AbSES.DirectSum.