proposition: Lemma abses_pullback_phomotopic' {A B B' : AbGroup} (f f' : B $-> B') (h : f == f') : abses_pullback' (A:=A) f $=>* abses_pullback' f'.
proof: 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.
imports: Basics Types HSet Limits.Pullback WildCat Pointed.Core Homotopy.ExactSequence Modalities.ReflectiveSubuniverse AbGroups.AbelianGroup AbGroups.AbPullback AbGroups.Biproduct AbSES.Core AbSES.DirectSum