{A B : AbGroup@{u}} (E : AbSES B A) : AbSESMorphism E E. Proof. snrapply (Build_AbSESMorphism grp_homo_id grp_homo_id grp_homo_id). 1,2: reflexivity. Defined.
Require Import Basics Types Truncations.Core. Require Import HSet WildCat. Require Import Groups.QuotientGroup Groups.ShortExactSequence. Require Import AbelianGroup AbGroups.Biproduct AbHom. Require Import Homotopy.ExactSequence Pointed. Require Import Modalities.ReflectiveSubuniverse.