abses_pushout_homotopic' `{Univalence} {A A' B : AbGroup} (f f' : A $-> A') (h : f == f') : abses_pushout (B:=B) f $=> abses_pushout f'. Proof. intro E; cbn. apply abses_path_data_to_iso. snrefine (_; (_, _)). - srapply (ab_pushout_rec (inclusion _)). 1: apply ab_pushout_inr. intro x. refine (ap _ (h x) @ _). apply (ab_pushout_commsq x). - apply ab_pushout_rec_beta_left. - rapply Quotient_ind_hprop; intros [a' e]; simpl. exact (ap (fun x => _ + projection E x) (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.