`{Univalence} {A B : AbGroup} (E F : AbSES B A) : abses_baer_sum E F = abses_baer_sum F E. Proof. unfold abses_baer_sum. refine (_ @ abses_pullback_compose ab_diagonal direct_sum_swap _). refine (ap (abses_pullback ab_diagonal) _). refine (ap (fun f => abses_pushout f _) ab_codiagonal_swap^ @ _). refine ((abses_pushout_compose _ _ _) @ _). refine (ap _ (abses_pushout_is_pullback (abses_swap_morphism E F)) @ _). unfold abses_swap_morphism, component3. apply abses_pushout_pullback_reorder. 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.