`{Univalence} {A B B' : AbGroup} {E : AbSES B A} (f g : ab_hom B' B) : abses_pullback (f + g) E = abses_baer_sum (abses_pullback f E) (abses_pullback g E). Proof. unfold abses_baer_sum. refine ((abses_pullback_compose (B1:=ab_biprod B B) _ _ E)^ @ _). refine (ap (abses_pullback _) (abses_pushout_is_pullback (abses_codiagonal E))^ @ _). unfold abses_codiagonal, component1. refine (_^ @ _ @ _). 1,3: apply abses_reorder_pullback_pushout. refine (ap (abses_pushout _) _). refine (ap (fun h => abses_pullback h _) (ab_biprod_corec_diagonal _ _) @ _). refine ((abses_pullback_compose _ _ (abses_direct_sum E E))^ @ _). exact (ap (abses_pullback _) (abses_directsum_distributive_pullbacks 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.