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