{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.
Require Import Basics Types. Require Import SuccessorStructure. Require Import WildCat. Require Import Pointed. Require Import Modalities.Identity Modalities.Descent. Require Import Truncations. Require Import HFiber. Require Import ObjectClassifier.