`{Univalence} {A A' B : AbGroup} (E : AbSES B A) (f : A $-> A') : AbSESMorphism E (abses_pushout f E). Proof. snrapply (Build_AbSESMorphism f _ grp_homo_id). - exact ab_pushout_inr. - exact ab_pushout_commsq. - rapply ab_pushout_rec_beta_right. 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.