proposition: Lemma abses_pullback_homotopic `{Univalence} {A B B' : AbGroup} (f f' : B $-> B') (h : f == f') : abses_pullback (A:=A) f == abses_pullback f'.
proof: Proof. intro E. apply equiv_path_abses_iso. exact (abses_pullback_homotopic' _ _ h _). Defined.
imports: Basics Types HSet Limits.Pullback WildCat Pointed.Core Homotopy.ExactSequence Modalities.ReflectiveSubuniverse AbGroups.AbelianGroup AbGroups.AbPullback AbGroups.Biproduct AbSES.Core AbSES.DirectSum