{A B X Y : AbGroup@{u}} {E : AbSES B A} {F : AbSES Y X} (f : AbSESMorphism E F) : AbSESMorphism E (abses_pullback (component3 f) F). Proof. snrapply (Build_AbSESMorphism (component1 f) _ grp_homo_id). - apply (grp_pullback_corec (projection F) (component3 f) (component2 f) (projection E)). apply right_square. - intro x; cbn. apply equiv_path_pullback_hset; cbn; split. + apply left_square. + symmetry; apply iscomplex_abses. - reflexivity. 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.