fact: Definition hfiber_abses_path {A B B' : AbGroup} {f : B' $-> B} {X : AbSES B' A} (E F : graph_hfiber (abses_pullback f) X) := {p : E.1 $-> F.1 & (fmap (abses_pullback f) p)^$ $@ E.2 $-> F.2}.
imports: Basics Types HSet Limits.Pullback WildCat Pointed.Core Homotopy.ExactSequence Modalities.ReflectiveSubuniverse AbGroups.AbelianGroup AbGroups.AbPullback AbGroups.Biproduct AbSES.Core AbSES.DirectSum