fact: Definition abses_path_data_1 {B A : AbGroup@{u}} (E : AbSES B A) : E $-> E := (grp_iso_id; (fun _ => idpath, fun _ => idpath)).
imports: Basics Types Truncations.Core HSet WildCat Groups.QuotientGroup Groups.ShortExactSequence AbelianGroup AbGroups.Biproduct AbHom Homotopy.ExactSequence Pointed Modalities.ReflectiveSubuniverse