proposition: Lemma functor_abses_directsum `{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: 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.
imports: Basics Types Truncations.Core Pointed.Core WildCat.Core Homotopy.ExactSequence AbGroups.AbelianGroup AbSES.Core AbGroups.Biproduct