{B A : AbGroup} (E : AbSES B A) : AbSESMorphism (pt : AbSES E A) E. Proof. srapply (Build_AbSESMorphism grp_homo_id _ (projection E)). - cbn. exact (ab_biprod_rec (inclusion E) grp_homo_id). - intro x; cbn. exact (right_identity _)^. - intros [a e]; cbn. refine (grp_homo_op _ _ _ @ _). refine (ap (fun x => sg_op x _) _ @ _). 1: apply isexact_inclusion_projection. apply left_identity. 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.