fact: Definition issig_AbSESMorphism {A X B Y : AbGroup@{u}} {E : AbSES B A} {F : AbSES Y X} : { f : (A $-> X) * (middle E $-> middle F) * (B $-> Y) & ((inclusion _) $o (fst (fst f)) == (snd (fst f)) $o (inclusion _)) * ((projection F) $o (snd (fst f)) == (snd f) $o (projection _)) } <~> AbSESMorphism E F := ltac:(make_equiv).
imports: Basics Types Truncations.Core HSet WildCat Groups.QuotientGroup Groups.ShortExactSequence AbelianGroup AbGroups.Biproduct AbHom Homotopy.ExactSequence Pointed Modalities.ReflectiveSubuniverse