n {F X Y : pType} {i i' : F ->* X} (ii : i' ==* i) (f : X ->* Y) `{IsExact n F X Y i f} : IsExact n i' f. Proof. exists (iscomplex_homotopic_i ii f cx_isexact). refine (conn_map_homotopic n (cxfib cx_isexact) _ _ _). intros u; cbn. refine (path_sigma' _ (ii u)^ _). exact (transport_paths_Fl _ _ @ ((inverse2 (ap_V _ _) @ inv_V _) @@ 1)). 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.