proposition: Lemma abses_pullback_homotopic' {A B B' : AbGroup} (f f' : B $-> B') (h : f == f') : abses_pullback (A:=A) f $=> abses_pullback f'.
proof: Proof. intro E. srefine (_; (_, _)). - srapply equiv_functor_grp_pullback. 1-3: exact grp_iso_id. 1: reflexivity. apply h. - intro a; cbn. by srapply equiv_path_pullback_hset; split. - 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