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. exact (abses_pullback_component1_id' (abses_pushout_morphism_rec f) (fun _ => idpath)). 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.