abses_pullback_homotopic' {A B B' : AbGroup} (f f' : B $-> B') (h : f == f') : abses_pullback (A:=A) f $=> abses_pullback f'. 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.
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.