`{Funext} {A B : AbGroup} (E : AbSES B A) : AbSESMorphism E (abses_direct_sum E E). Proof. snrapply Build_AbSESMorphism. 1,2,3: exact ab_diagonal. 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.