fact: Definition loops_abses `{Univalence} {A B : AbGroup} : (B $-> A) <~> loops (AbSES B A) := equiv_path_abses oE abses_endomorphism_trivial^-1.
imports: Basics Types Truncations.Core HSet WildCat Groups.QuotientGroup Groups.ShortExactSequence AbelianGroup AbGroups.Biproduct AbHom Homotopy.ExactSequence Pointed Modalities.ReflectiveSubuniverse