fact: Definition iscomplex_homotopic_f {F X Y : pType} (i : F ->* X) {f f' : X ->* Y} (ff : f' ==* f) (cx : IsComplex i f) : IsComplex i f' := pmap_prewhisker i ff @* cx.
imports: Basics Types SuccessorStructure WildCat Pointed Modalities.Identity Modalities.Descent Truncations HFiber ObjectClassifier