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