{A B B' : AbGroup@{u}} (bt : B' $-> B) (E : AbSES B A) (F : AbSES B' A) (p : abses_pullback bt E = F) : exists phi : middle F $-> E, projection E o phi == bt o projection F. Proof. induction p. exists (grp_pullback_pr1 _ _); intro x. nrapply 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.