fact: Definition abses_direct_sum `{Funext} {B A B' A' : AbGroup} (E : AbSES B A) (F : AbSES B' A') : AbSES (ab_biprod B B') (ab_biprod A A') := Build_AbSES (ab_biprod E F) (functor_ab_biprod (inclusion E) (inclusion F)) (functor_ab_biprod (projection E) (projection F)) (functor_ab_biprod_embedding _ _) (functor_ab_biprod_surjection _ _) (ab_biprod_exact _ _ _ _).
imports: Basics Types Truncations.Core Pointed.Core WildCat.Core Homotopy.ExactSequence AbGroups.AbelianGroup AbSES.Core AbGroups.Biproduct