AbSES' {B A : AbGroup@{u}} := Build_AbSES { middle : AbGroup@{u}; inclusion : A $-> middle; projection : middle $-> B; isembedding_inclusion : IsEmbedding inclusion; issurjection_projection : IsSurjection projection; isexact_inclusion_projection : IsExact (Tr (-1)) inclusion projection; }.
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.