n {F X Y : pType} (i : F ->* X) {f f' : X ->* Y} (ff : f' ==* f) `{IsExact n F X Y i f} : IsExact n i f'. Proof. exists (iscomplex_homotopic_f i ff cx_isexact). pose (e := equiv_hfiber_homotopic _ _ ff pt). nrefine (cancelL_isequiv_conn_map n _ e). 1: apply equiv_isequiv. refine (conn_map_homotopic n (cxfib (cx_isexact)) _ _ _). intro u. simpl. srapply path_hfiber. 1: reflexivity. refine (concat_1p _ @ concat_V_pp _ _)^. 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.