fact: Definition baer_sum_pullback `{Univalence} {A B B' : AbGroup} (f : B' $-> B) (E F : AbSES B A) : abses_pullback f (abses_baer_sum E F) = abses_baer_sum (abses_pullback f E) (abses_pullback 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