{B' A' B A : AbGroup@{u}} : AbSES B A -->* AbSES B' A' := Build_BasepointPreservingFunctor (const pt) (Id pt).
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.