abses_pullback_phomotopic' {A B B' : AbGroup} (f f' : B $-> B') (h : f == f') : abses_pullback' (A:=A) f $=>* abses_pullback' f'. Proof. exists (abses_pullback_homotopic' f f' h); cbn. intros [[a b'] [b c]]; cbn in c. srapply equiv_path_pullback_hset; split; cbn. 2: reflexivity. exact (path_prod' idpath (c @ h b)). 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.