{A0 A1 A2 B0 B1 B2 : AbGroup@{u}} {E : AbSES B0 A0} {F : AbSES B1 A1} {G : AbSES B2 A2} (g : AbSESMorphism F G) (f : AbSESMorphism E F) : AbSESMorphism E G. Proof. rapply (Build_AbSESMorphism (component1 g $o component1 f) (component2 g $o component2 f) (component3 g $o component3 f)). - intro x; cbn. exact (left_square g _ @ ap _ (left_square f _)). - intro x; cbn. exact (right_square g _ @ ap _ (right_square f _)). Defined.
Require Import Basics Types Truncations.Core. Require Import HSet WildCat. Require Import Groups.QuotientGroup Groups.ShortExactSequence. Require Import AbelianGroup AbGroups.Biproduct AbHom. Require Import Homotopy.ExactSequence Pointed. Require Import Modalities.ReflectiveSubuniverse.