fact: Definition abses_pullback_phomotopic `{Univalence} {A B B' : AbGroup} (f f' : B $-> B') (h : f == f') : abses_pullback_pmap (A:=A) f ==* abses_pullback_pmap f' := equiv_ptransformation_phomotopy (abses_pullback_phomotopic' f f' h).
imports: Basics Types HSet Limits.Pullback WildCat Pointed.Core Homotopy.ExactSequence Modalities.ReflectiveSubuniverse AbGroups.AbelianGroup AbGroups.AbPullback AbGroups.Biproduct AbSES.Core AbSES.DirectSum