`{Funext} {A B : AbGroup} (E F G : AbSES B A) : AbSESMorphism (abses_direct_sum (abses_direct_sum E F) G) (abses_direct_sum (abses_direct_sum G F) E). Proof. snrapply Build_AbSESMorphism. 1,2,3: exact ab_biprod_twist. all: reflexivity. Defined.
Require Import Basics Types Truncations.Core. Require Import Pointed.Core. Require Import WildCat.Core Homotopy.ExactSequence. Require Import AbGroups.AbelianGroup AbSES.Core AbGroups.Biproduct.