fact: Definition abses_baer_sum `{Univalence} {B A : AbGroup@{u}} (E F : AbSES B A) : AbSES B A := abses_pullback ab_diagonal (abses_pushout ab_codiagonal (abses_direct_sum E F)).
imports: Basics Types WildCat Pointed.Core AbGroups.AbelianGroup AbGroups.Biproduct AbGroups.AbHom AbSES.Core AbSES.Pullback AbSES.Pushout AbSES.DirectSum Homotopy.HSpace.Core