`{Univalence} {A B : AbGroup@{u}} (E F G : AbSES B A) : abses_baer_sum (abses_baer_sum E F) G = abses_trinary_baer_sum E F G. Proof. unfold abses_baer_sum, abses_trinary_baer_sum, ab_triagonal, ab_cotriagonal. refine (ap (abses_pullback _ o abses_pushout _) _^ @ _). - refine (_ @ ap (abses_direct_sum _) (abses_pullback_id G)). refine (_ @ abses_directsum_distributive_pullbacks _ _). refine (ap (abses_pullback _) _). refine (_ @ ap (abses_direct_sum _) (abses_pushout_id G)). apply abses_directsum_distributive_pushouts. - refine (ap (abses_pullback _) (abses_pushout_pullback_reorder _ _ _) @ _). refine (abses_pullback_compose _ _ _ @ _). refine (ap (abses_pullback _) _^). apply abses_pushout_compose. 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.