fact: Definition cxfib {F X Y : pType} {i : F ->* X} {f : X ->* Y} (cx : IsComplex i f) : F ->* pfiber f.
imports: Basics Types SuccessorStructure WildCat Pointed Modalities.Identity Modalities.Descent Truncations HFiber ObjectClassifier