proposition: Lemma abses_pullback_pconst' {A B B' : AbGroup} : @pmap_abses_const B' A B A $=>* abses_pullback' grp_homo_const.
proof: Proof. srefine (_; _). 1: rapply abses_pullback_const'. lazy beta. intro x; reflexivity. Defined.
imports: Basics Types HSet Limits.Pullback WildCat Pointed.Core Homotopy.ExactSequence Modalities.ReflectiveSubuniverse AbGroups.AbelianGroup AbGroups.AbPullback AbGroups.Biproduct AbSES.Core AbSES.DirectSum