proposition: Lemma baer_sum_associative `{Univalence} {A B : AbGroup@{u}} (E F G : AbSES B A) : abses_baer_sum (abses_baer_sum E F) G = abses_baer_sum E (abses_baer_sum F G).
proof: Proof. refine ((baer_sum_twist _ _ _)^ @ _). refine (baer_sum_commutative _ _ @ _). apply ap. apply baer_sum_commutative. Defined.
imports: Basics Types WildCat Pointed.Core AbGroups.AbelianGroup AbGroups.Biproduct AbGroups.AbHom AbSES.Core AbSES.Pullback AbSES.Pushout AbSES.DirectSum Homotopy.HSpace.Core