fact: Definition abses_pushout_is_pullback `{Univalence} {A A' B B' : AbGroup} {E : AbSES B A} {E' : AbSES B' A'} (f : AbSESMorphism E E') : abses_pushout (component1 f) E = abses_pullback (component3 f) E' := equiv_path_abses_iso (abses_pushout_is_pullback' f).
imports: Basics Types WildCat Pointed.Core AbGroups.AbelianGroup AbGroups.Biproduct AbGroups.AbHom AbSES.Core AbSES.Pullback AbSES.Pushout AbSES.DirectSum Homotopy.HSpace.Core