n {F F' X Y : pType} (i : F ->* X) (f : X ->* Y) (phi : F' <~>* F) `{E : IsExact n _ _ _ i f} : IsExact n (i o* phi) f. Proof. snrapply Build_IsExact. 1: apply iscomplex_equiv_fiber, cx_isexact. apply (conn_map_homotopic _ (cxfib cx_isexact o* phi)). { intro x; cbn. by rewrite concat_p1, concat_1p. } exact _. 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.