n {F F' X X' Y Y' : pType} {i : F ->* X} {i' : F' ->* X'} {f : X ->* Y} {f' : X' ->* Y'} (g : F' <~>* F) (h : X' <~>* X) (k : Y' <~>* Y) (p : h o* i' ==* i o* g) (q : k o* f' ==* f o* h) `{IsExact n F X Y i f} : IsExact n i' f'. Proof. pose (I := isexact_equiv_i n i i' g h p f). pose (I2 := isexact_homotopic_f n i' q). exists (iscomplex_cancelL i' f' k cx_isexact). epose (e := (pequiv_pfiber pequiv_pmap_idmap k (pmap_precompose_idmap (k o* f'))^* : pfiber f' <~>* pfiber (k o* f'))). nrefine (cancelL_isequiv_conn_map n _ e). 1: apply pointed_isequiv. refine (conn_map_homotopic n (cxfib (cx_isexact)) _ _ _). intro u. srapply path_hfiber. { reflexivity. } cbn. unfold moveR_equiv_V. rewrite !concat_1p, !concat_p1, ap_pp_p, ap_pp, (ap_pp k _ (eissect k (point Y'))), ap_V, <- !eisadj. rewrite <- !ap_compose, concat_pp_p. rewrite (concat_A1p (eisretr k)), concat_pV_p. rewrite (concat_A1p (eisretr k)), concat_V_pp. reflexivity. 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.