fact: Definition baer_sum_pushout `{Univalence} {A A' B : AbGroup} (f : A $-> A') (E F : AbSES B A) : abses_pushout f (abses_baer_sum E F) = abses_baer_sum (abses_pushout f E) (abses_pushout f F).
imports: Basics Types WildCat Pointed.Core AbGroups.AbelianGroup AbGroups.Biproduct AbGroups.AbHom AbSES.Core AbSES.Pullback AbSES.Pushout AbSES.DirectSum Homotopy.HSpace.Core