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