n {F F' X X' Y : pType} (i : F ->* X) (i' : F' ->* X') (g : F' <~>* F) (h : X' <~>* X) (p : h o* i' ==* i o* g) (f : X ->* Y) `{IsExact n F X Y i f} : IsExact n i' (f o* h). Proof. exists (iscomplex_equiv_i i i' g h p f cx_isexact); cbn. snrefine (cancelL_equiv_conn_map n (C := pfiber f) _ _). - exact (@equiv_functor_hfiber _ _ _ _ (f o h) f h equiv_idmap (fun x => 1%path) (point Y)). - cbn; unfold functor_hfiber, functor_sigma; cbn. refine (conn_map_homotopic n (@cxfib _ _ _ i f cx_isexact o g) _ _ _). intros u; cbn. refine (path_sigma' _ (p u)^ _). abstract ( rewrite transport_paths_Fl, ap_V, inv_V, !concat_1p, concat_p1, ap_idmap; 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.