proposition: Lemma twist_trinary_baer_sum `{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: 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.
imports: Basics Types WildCat Pointed.Core AbGroups.AbelianGroup AbGroups.Biproduct AbGroups.AbHom AbSES.Core AbSES.Pullback AbSES.Pushout AbSES.DirectSum Homotopy.HSpace.Core