`{Univalence} {A B B' : AbGroup} (f : B' $-> B) (E F : AbSES B A) : abses_pullback f (abses_baer_sum E F) = abses_baer_sum (abses_pullback f E) (abses_pullback f F). Proof. unfold abses_baer_sum. refine (abses_pullback_compose _ _ _ @ _). refine ((abses_pushout_pullback_reorder _ _ _)^ @ ap _ _ @ abses_pushout_pullback_reorder _ _ _). refine (abses_pullback_homotopic _ (functor_ab_biprod f f $o ab_diagonal) _ _ @ _). 1: reflexivity. refine ((abses_pullback_compose _ _ _)^ @ ap _ _). apply abses_directsum_distributive_pullbacks. 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.