`{Univalence} {A A' B : AbGroup} {E : AbSES B A'} (f g : ab_hom A' A) : abses_pushout (f + g) E = abses_baer_sum (abses_pushout f E) (abses_pushout g E). Proof. unfold abses_baer_sum. refine (abses_pushout_compose (A1 := ab_biprod A A) _ _ E @ _). refine (_ @ abses_pushout_pullback_reorder _ _ _). refine (ap (abses_pushout ab_codiagonal) _). refine (ap (fun f => abses_pushout f E) (ab_biprod_corec_diagonal f g) @ _). refine (abses_pushout_compose _ _ E @ _). refine (ap (abses_pushout _) (abses_pushout_is_pullback (abses_diagonal E)) @ _). refine (abses_pushout_pullback_reorder _ _ _ @ _). exact (ap (abses_pullback _) (abses_directsum_distributive_pushouts f g)). 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.