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). Proof. pose (F := absesmorphism_compose (abses_pushout_morphism E f) (abses_pullback_morphism E g)). refine (abses_pushout_is_pullback' (Build_AbSESMorphism f (component2 F) g _ _)); apply F. Defined.
Require Import Basics Types. Require Import WildCat Pointed.Core. Require Import AbGroups.AbelianGroup AbGroups.Biproduct AbGroups.AbHom. Require Import AbSES.Core AbSES.Pullback AbSES.Pushout AbSES.DirectSum. Require Import Homotopy.HSpace.Core.