{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).
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.