abses_pushout_phomotopic' `{Univalence} {A A' B : AbGroup} (f f' : A $-> A') (h : f == f') : abses_pushout' (B:=B) f $=>* abses_pushout' f'. Proof. exists (abses_pushout_homotopic' _ _ h). apply gpd_moveL_Vh. rapply Quotient_ind_hprop; intros [a' [a b]]; simpl. apply path_prod'. - by rewrite grp_unit_l, grp_unit_r, (h a). - apply grp_unit_l. 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.