`{Univalence} {A B : AbGroup@{u}} (E F G : AbSES B A) : abses_trinary_baer_sum E F G = abses_trinary_baer_sum G F E. Proof. unfold abses_trinary_baer_sum. refine (_ @ abses_pullback_compose ab_triagonal ab_biprod_twist _). refine (ap (abses_pullback _) _). refine (ap (fun f => abses_pushout f _) ab_cotriagonal_twist^ @ _). refine (abses_pushout_compose _ _ _ @ _). refine (ap _ (abses_pushout_is_pullback (abses_twist_directsum E F G)) @ _). unfold abses_twist_directsum, component3. exact (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.