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