`{Univalence} {A B X Y : AbGroup} {E : AbSES B A} {F : AbSES Y X} (f : AbSESMorphism E F) : AbSESMorphism (abses_pushout (component1 f) E) F. Proof. snrapply (Build_AbSESMorphism grp_homo_id _ (component3 f)). - rapply ab_pushout_rec. apply left_square. - intro x; simpl. rewrite grp_homo_unit. exact (right_identity _)^. - snrapply (issurj_isepi_funext grp_quotient_map). 1: apply issurj_class_of. 2: exact _. intro x; simpl. nrapply grp_homo_op_agree. + refine (_ @ (grp_homo_unit _)^). apply iscomplex_abses. + apply right_square. 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.