proposition: Lemma baer_sum_commutative `{Univalence} {A B : AbGroup} (E F : AbSES B A) : abses_baer_sum E F = abses_baer_sum F E.
proof: 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.
imports: Basics Types WildCat Pointed.Core AbGroups.AbelianGroup AbGroups.Biproduct AbGroups.AbHom AbSES.Core AbSES.Pullback AbSES.Pushout AbSES.DirectSum Homotopy.HSpace.Core