{A B B' : AbGroup} (f : B' $-> B) : AbSES B A -> AbSES B' A. Proof. intro E. snrapply (Build_AbSES (ab_pullback (projection E) f) (grp_pullback_corec _ _ (inclusion _) grp_homo_const _) (grp_pullback_pr2 (projection _) f)). - intro x. nrefine (_ @ (grp_homo_unit f)^). apply isexact_inclusion_projection. - exact (cancelL_isembedding (g:= grp_pullback_pr1 _ _)). - rapply conn_map_pullback'. - snrapply Build_IsExact. + snrapply phomotopy_homotopy_hset. * exact _. * reflexivity. + nrefine (cancelL_equiv_conn_map _ _ (hfiber_pullback_along_pointed f (projection _) (grp_homo_unit _))). nrefine (conn_map_homotopic _ _ _ _ (conn_map_isexact (IsExact:=isexact_inclusion_projection _))). intro a. by apply path_sigma_hprop. Defined.
Require Import Basics Types. Require Import HSet Limits.Pullback. Require Import WildCat Pointed.Core Homotopy.ExactSequence. Require Import Modalities.ReflectiveSubuniverse. Require Import AbGroups.AbelianGroup AbGroups.AbPullback AbGroups.Biproduct. Require Import AbSES.Core AbSES.DirectSum.