`{Univalence} {A B : AbGroup@{u}} (E F G : AbSES B A) : abses_baer_sum (abses_baer_sum E F) G = abses_baer_sum (abses_baer_sum G F) E. Proof. refine ((baer_sum_is_trinary E F G) @ _ @ (baer_sum_is_trinary G F E)^). apply twist_trinary_baer_sum. 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.