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