fact: Definition abses_pushout_point `{Univalence} {A A' B : AbGroup} (f : A $-> A') : abses_pushout f (point (AbSES B A)) = pt := equiv_path_abses_iso (abses_pushout_point' f).
imports: Basics Types Truncations.Core WildCat Pointed.Core Homotopy.ExactSequence HIT.epi Modalities.ReflectiveSubuniverse AbelianGroup AbPushout AbHom AbGroups.Biproduct AbSES.Core AbSES.DirectSum