{B A : AbGroup@{u}} (E F : AbSES B A) := {phi : GroupHomomorphism E F & (phi $o inclusion _ == inclusion _) * (projection _ == projection _ $o phi)}.
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.