`{Funext} {A A' B B' C C' D D' : AbGroup} {E : AbSES B A} {E' : AbSES B' A'} {F : AbSES D C} {F' : AbSES D' C'} (f : AbSESMorphism E E') (g : AbSESMorphism F F') : AbSESMorphism (abses_direct_sum E F) (abses_direct_sum E' F'). Proof. snrapply Build_AbSESMorphism. + exact (functor_ab_biprod (component1 f) (component1 g)). + exact (functor_ab_biprod (component2 f) (component2 g)). + exact (functor_ab_biprod (component3 f) (component3 g)). + intro x. apply path_prod; apply left_square. + intro x. apply path_prod; apply right_square. 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.