`{Funext} {A B : AbGroup} (E : AbSES B A) : AbSESMorphism (abses_direct_sum E E) E. Proof. snrapply Build_AbSESMorphism. 1,2,3: exact ab_codiagonal. all: intro x; cbn; apply grp_homo_op. 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.