{F F' X X' Y : pType} (i : F ->* X) (i' : F' ->* X') (g : F' <~>* F) (h : X' <~>* X) (p : h o* i' ==* i o* g) (f : X ->* Y) (cx: IsComplex i f) : IsComplex i' (f o* h). Proof. refine (pmap_compose_assoc _ _ _ @* _). refine (pmap_postwhisker f p @* _). refine ((pmap_compose_assoc _ _ _)^* @* _). refine (pmap_prewhisker g 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.