fact: Definition hfiber_cxfib' {A B C : AbGroup} (E : AbSES C B) (F : AbSES (middle E) A) (p : abses_pullback (inclusion E) F $== pt) := {Y : AbSES C A & hfiber_abses_path (cxfib' E Y) (F; p)}.
imports: Basics Types HSet HFiber Limits.Pullback WildCat Pointed.Core Homotopy.ExactSequence Groups.QuotientGroup AbGroups.AbelianGroup AbGroups.AbPullback AbGroups.Biproduct AbSES.Core AbSES.Pullback Modalities.Identity Modalities.Modality Truncations.Core