{F F' X Y : pType} (i : F ->* X) (f : X ->* Y) (phi : F' <~>* F) `{cx : IsComplex i f} : IsComplex (i o* phi) f. Proof. refine ((pmap_compose_assoc _ _ _)^* @* _). refine (pmap_prewhisker _ cx @* _). apply postcompose_pconst. Defined.
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.