fact: Definition abses_from_inclusion `{Univalence} {A E : AbGroup@{u}} (i : A $-> E) `{IsEmbedding i} : AbSES (QuotientAbGroup E (grp_image_embedding i)) A.
imports: Basics Types Truncations.Core HSet WildCat Groups.QuotientGroup Groups.ShortExactSequence AbelianGroup AbGroups.Biproduct AbHom Homotopy.ExactSequence Pointed Modalities.ReflectiveSubuniverse