`{Univalence} {A A' B : AbGroup} (f : A $-> A') (E F : AbSES B A) : abses_pushout f (abses_baer_sum E F) = abses_baer_sum (abses_pushout f E) (abses_pushout f F). Proof. unfold abses_baer_sum. refine (abses_pushout_pullback_reorder _ _ _ @ ap _ _). refine ((abses_pushout_compose _ _ _)^ @ _). refine (abses_pushout_homotopic _ _ _ _ @ _). 1: apply ab_codiagonal_natural. refine (abses_pushout_compose _ _ _ @ ap _ _). apply abses_directsum_distributive_pushouts. 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.