proposition: Lemma abses_pushout_is_pullback' `{Univalence} {A A' B B' : AbGroup@{u}} {E : AbSES B A} {E' : AbSES B' A'} (f : AbSESMorphism E E') : abses_pushout (component1 f) E $== abses_pullback (component3 f) E'.
proof: Proof. exact (abses_pullback_component1_id' (abses_pushout_morphism_rec f) (fun _ => idpath)). Defined.
imports: Basics Types WildCat Pointed.Core AbGroups.AbelianGroup AbGroups.Biproduct AbGroups.AbHom AbSES.Core AbSES.Pullback AbSES.Pushout AbSES.DirectSum Homotopy.HSpace.Core