(B A : AbGroup@{u}) := pTr 0 (AbSES B A).
Require Import Basics Types Truncations.Core. Require Import Pointed WildCat. Require Import Truncations.SeparatedTrunc. Require Import AbelianGroup AbHom AbProjective. Require Import AbSES.Pullback AbSES.Pushout AbSES.BaerSum AbSES.Core.