`{Univalence} {A A' B : AbGroup} (f : A $-> A') : AbSES B A -> AbSES B A'. Proof. intro E. snrapply (Build_AbSES (ab_pushout f (inclusion E)) ab_pushout_inl (ab_pushout_rec grp_homo_const (projection E) _)). - symmetry; rapply iscomplex_abses. - rapply ab_pushout_embedding_inl. - nrapply (cancelR_issurjection ab_pushout_inr _). rapply (conn_map_homotopic _ (projection E)); symmetry. nrapply ab_pushout_rec_beta_right. - snrapply Build_IsExact. + srapply phomotopy_homotopy_hset. nrapply ab_pushout_rec_beta_left. + intros [bc' p]. rapply contr_inhabited_hprop. assert (bc : merely (hfiber grp_quotient_map bc')). 1: apply center, issurj_class_of. strip_truncations. destruct bc as [[b c] q]. assert (c_in_kernel : (projection E) c = mon_unit). 1: { refine (_ @ p); symmetry. rewrite <- q; simpl. apply left_identity. } pose proof (a := isexact_preimage _ _ _ c c_in_kernel). strip_truncations. destruct a as [a s]. apply tr. exists (b + - f (- a)); cbn. apply path_sigma_hprop; cbn. change (ab_pushout_inl (b + - f (- a)) = bc'). refine (_ @ q). symmetry. apply path_ab_pushout; cbn. refine (tr (-a; _)). apply path_prod; cbn. * apply grp_moveL_Mg. by rewrite negate_involutive. * exact ((preserves_negate a) @ ap _ s @ (right_identity _)^). 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.