`{Funext} {A B X Y : AbGroup@{u}} {E : AbSES B A} {F : AbSES Y X} (f : AbSESMorphism E F) : f = absesmorphism_compose (abses_pullback_morphism F (component3 f)) (abses_pullback_morphism_corec f). Proof. apply (equiv_ap issig_AbSESMorphism^-1 _ _). srapply path_sigma_hprop. apply path_prod. 1: apply path_prod. all: by apply equiv_path_grouphomomorphism. 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.