{F X Y Y' : pType} (i : F ->* X) (f : X ->* Y) (e : Y <~>* Y') (cx : IsComplex i (e o* f)) : IsComplex i f. Proof. refine (_ @* precompose_pconst e^-1*). refine ((compose_V_hh e (f o* i))^$ $@ _). refine (cat_postwhisker e^-1* _). refine ((cat_assoc _ _ _)^$ $@ _). exact cx. 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.