{A B B' : AbGroup@{u}} (E : AbSES B A) (f : B' $-> B) : AbSESMorphism (abses_pullback f E) E. Proof. snrapply (Build_AbSESMorphism grp_homo_id _ f). - apply grp_pullback_pr1. - reflexivity. - apply pullback_commsq. 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.