(* -*- mode: coq; mode: visual-line -*-  *)
Require Import Basics Types.
[Loading ML file number_string_notation_plugin.cmxs (using legacy method) ... done]
Require Import SuccessorStructure.
Require Import WildCat.
Require Import Pointed.
Require Import Modalities.Identity Modalities.Descent.
Require Import Truncations.
Require Import HFiber.
Require Import ObjectClassifier.

Local Open Scope succ_scope.
Open Scope pointed_scope.

(** * Exact sequences *)

(** ** Very short complexes *)

(** A (very short) complex is a pair of pointed maps whose composite is the zero map. *)
Definition IsComplex {F X Y} (i : F ->* X) (f : X ->* Y)
  := (f o* i ==* pconst).

(** This induces a map from the domain of [i] to the fiber of [f]. *)
Definition cxfib {F X Y : pType} {i : F ->* X} {f : X ->* Y}
  (cx : IsComplex i f)
  : F ->* pfiber f.
F, X, Y: pType
i: F ->* X
f: X ->* Y
cx: IsComplex i f
F ->* pfiber f
Proof.
F, X, Y: pType
i: F ->* X
f: X ->* Y
cx: IsComplex i f
F ->* pfiber f
  srapply Build_pMap.
F, X, Y: pType
i: F ->* X
f: X ->* Y
cx: IsComplex i f
F -> pfiber f
F, X, Y: pType
i: F ->* X
f: X ->* Y
cx: IsComplex i f
?Goal pt = pt
  -
F, X, Y: pType
i: F ->* X
f: X ->* Y
cx: IsComplex i f
F -> pfiber f exact (fun x => (i x; cx x)).
  -
F, X, Y: pType
i: F ->* X
f: X ->* Y
cx: IsComplex i f
(fun x : F => (i x; cx x)) pt = pt cbn.
F, X, Y: pType
i: F ->* X
f: X ->* Y
cx: IsComplex i f
(i pt; cx pt) = ispointed_fiber f refine (path_sigma' _ (point_eq i) _); cbn.
F, X, Y: pType
i: F ->* X
f: X ->* Y
cx: IsComplex i f
transport (fun x : X => f x = pt) (point_eq i) (cx pt) =
point_eq f
    refine (transport_paths_Fl _ _ @ _).
F, X, Y: pType
i: F ->* X
f: X ->* Y
cx: IsComplex i f
(ap f (point_eq i))^ @ cx pt = point_eq f
    apply moveR_Vp.
F, X, Y: pType
i: F ->* X
f: X ->* Y
cx: IsComplex i f
cx pt = ap f (point_eq i) @ point_eq f
    exact ((concat_p1 _)^ @ point_htpy cx).
Defined.

(** ...whose composite with the projection [pfib : pfiber i -> X] is [i].  *)
Definition pfib_cxfib {F X Y : pType} {i : F ->* X} {f : X ->* Y}
  (cx : IsComplex i f)
  : pfib f o* cxfib cx ==* i.
F, X, Y: pType
i: F ->* X
f: X ->* Y
cx: IsComplex i f
pfib f o* cxfib cx ==* i
Proof.
F, X, Y: pType
i: F ->* X
f: X ->* Y
cx: IsComplex i f
pfib f o* cxfib cx ==* i
  srapply Build_pHomotopy.
F, X, Y: pType
i: F ->* X
f: X ->* Y
cx: IsComplex i f
pfib f o* cxfib cx == i
F, X, Y: pType
i: F ->* X
f: X ->* Y
cx: IsComplex i f
?p pt =
dpoint_eq (pfib f o* cxfib cx) @ (dpoint_eq i)^
  -
F, X, Y: pType
i: F ->* X
f: X ->* Y
cx: IsComplex i f
pfib f o* cxfib cx == i reflexivity.
  -
F, X, Y: pType
i: F ->* X
f: X ->* Y
cx: IsComplex i f
(fun x0 : F => 1) pt =
dpoint_eq (pfib f o* cxfib cx) @ (dpoint_eq i)^ cbn.
F, X, Y: pType
i: F ->* X
f: X ->* Y
cx: IsComplex i f
1 =
(ap pr1
   (path_sigma' (fun x : X => f x = pt) (point_eq i)
      (transport_paths_Fl (point_eq i) (cx pt) @
       moveR_Vp (cx pt) (point_eq f)
         (ap f (point_eq i))
         ((concat_p1 (cx pt))^ @
          ((concat_p1 (cx pt) @ dpoint_eq cx) @
           concat_p1 (ap f (point_eq i) @ point_eq f))))) @
 1) @ (dpoint_eq i)^ rewrite ap_pr1_path_sigma; hott_simpl.
Defined.

(** Truncation preserves complexes. *)
Definition iscomplex_ptr (n : trunc_index) {F X Y : pType}
  (i : F ->* X) (f : X ->* Y) (cx : IsComplex i f)
  : IsComplex (fmap (pTr n) i) (fmap (pTr n) f).
n: trunc_index
F, X, Y: pType
i: F ->* X
f: X ->* Y
cx: IsComplex i f
IsComplex (fmap (pTr n) i) (fmap (pTr n) f)
Proof.
n: trunc_index
F, X, Y: pType
i: F ->* X
f: X ->* Y
cx: IsComplex i f
IsComplex (fmap (pTr n) i) (fmap (pTr n) f)
  refine ((fmap_comp (pTr n) i f)^* @* _).
n: trunc_index
F, X, Y: pType
i: F ->* X
f: X ->* Y
cx: IsComplex i f
fmap (pTr n) (f $o i) ==* pconst
  refine (_ @* ptr_functor_pconst n).
n: trunc_index
F, X, Y: pType
i: F ->* X
f: X ->* Y
cx: IsComplex i f
fmap (pTr n) (f $o i) ==* fmap (pTr n) pconst
  rapply (fmap2 (pTr _)); assumption.
Defined.

(** Loop spaces preserve complexes. *)
Definition iscomplex_loops {F X Y : pType}
  (i : F ->* X) (f : X ->* Y) (cx : IsComplex i f)
  : IsComplex (fmap loops i) (fmap loops f).
F, X, Y: pType
i: F ->* X
f: X ->* Y
cx: IsComplex i f
IsComplex (fmap loops i) (fmap loops f)
Proof.
F, X, Y: pType
i: F ->* X
f: X ->* Y
cx: IsComplex i f
IsComplex (fmap loops i) (fmap loops f)
  refine ((fmap_comp loops i f)^$ $@ _ $@ fmap_zero_morphism _).
F, X, Y: pType
i: F ->* X
f: X ->* Y
cx: IsComplex i f
fmap loops (f $o i) $== fmap loops zero_morphism
  rapply (fmap2 loops); assumption.
Defined.

Definition iscomplex_iterated_loops {F X Y : pType}
  (i : F ->* X) (f : X ->* Y) (cx : IsComplex i f) (n : nat)
  : IsComplex (fmap (iterated_loops n) i) (fmap (iterated_loops n) f).
F, X, Y: pType
i: F ->* X
f: X ->* Y
cx: IsComplex i f
n: nat
IsComplex (fmap (iterated_loops n) i)
  (fmap (iterated_loops n) f)
Proof.
F, X, Y: pType
i: F ->* X
f: X ->* Y
cx: IsComplex i f
n: nat
IsComplex (fmap (iterated_loops n) i)
  (fmap (iterated_loops n) f)
  induction n as [|n IHn]; [ exact cx | ].
F, X, Y: pType
i: F ->* X
f: X ->* Y
cx: IsComplex i f
n: nat
IHn: IsComplex (fmap (iterated_loops n) i) (fmap (iterated_loops n) f)
IsComplex (fmap (iterated_loops n.+1) i)
  (fmap (iterated_loops n.+1) f)
  apply iscomplex_loops; assumption.
Defined.

(** Passage across homotopies preserves complexes. *)
Definition iscomplex_homotopic_i {F X Y : pType}
  {i i' : F ->* X} (ii : i' ==* i) (f : X ->* Y) (cx : IsComplex i f)
  : IsComplex i' f := pmap_postwhisker f ii @* cx.

Definition iscomplex_homotopic_f {F X Y : pType}
  (i : F ->* X) {f f' : X ->* Y} (ff : f' ==* f) (cx : IsComplex i f)
  : IsComplex i f'
  := pmap_prewhisker i ff @* cx.

Definition iscomplex_cancelL {F X Y Y' : pType}
  (i : F ->* X) (f : X ->* Y) (e : Y <~>* Y') (cx : IsComplex i (e o* f))
  : IsComplex i f.
F, X, Y, Y': pType
i: F ->* X
f: X ->* Y
e: Y <~>* Y'
cx: IsComplex i (e o* f)
IsComplex i f
Proof.
F, X, Y, Y': pType
i: F ->* X
f: X ->* Y
e: Y <~>* Y'
cx: IsComplex i (e o* f)
IsComplex i f
  refine (_ @* precompose_pconst e^-1*).
F, X, Y, Y': pType
i: F ->* X
f: X ->* Y
e: Y <~>* Y'
cx: IsComplex i (e o* f)
f o* i ==* e^-1* o* pconst
  refine ((compose_V_hh e (f o* i))^$ $@ _).
F, X, Y, Y': pType
i: F ->* X
f: X ->* Y
e: Y <~>* Y'
cx: IsComplex i (e o* f)
e^-1* $o (e $o (f o* i)) $== e^-1* o* pconst
  refine (cat_postwhisker e^-1* _).
F, X, Y, Y': pType
i: F ->* X
f: X ->* Y
e: Y <~>* Y'
cx: IsComplex i (e o* f)
e $o (f o* i) $== pconst
  refine ((cat_assoc _ _ _)^$ $@ _).
F, X, Y, Y': pType
i: F ->* X
f: X ->* Y
e: Y <~>* Y'
cx: IsComplex i (e o* f)
e $o f $o i $== pconst
  exact cx.
Defined.

(** And likewise passage across squares with equivalences *)
Definition iscomplex_equiv_i {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)
  (cx: IsComplex i f)
  : IsComplex i' (f o* h).
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
cx: IsComplex i f
IsComplex i' (f o* h)
Proof.
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
cx: IsComplex i f
IsComplex i' (f o* h)
  refine (pmap_compose_assoc _ _ _ @* _).
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
cx: IsComplex i f
f o* (h o* i') ==* pconst
  refine (pmap_postwhisker f p @* _).
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
cx: IsComplex i f
f o* (i o* g) ==* pconst
  refine ((pmap_compose_assoc _ _ _)^* @* _).
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
cx: IsComplex i f
f o* i o* g ==* pconst
  refine (pmap_prewhisker g cx @* _).
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
cx: IsComplex i f
pconst o* g ==* pconst
  apply postcompose_pconst.
Defined.

(** A special version with only an equivalence on the fiber. *)
Definition iscomplex_equiv_fiber {F F' X Y : pType}
  (i : F ->* X) (f : X ->* Y) (phi : F' <~>* F)
  `{cx : IsComplex i f}
  : IsComplex (i o* phi) f.
F, F', X, Y: pType
i: F ->* X
f: X ->* Y
phi: F' <~>* F
cx: IsComplex i f
IsComplex (i o* phi) f
Proof.
F, F', X, Y: pType
i: F ->* X
f: X ->* Y
phi: F' <~>* F
cx: IsComplex i f
IsComplex (i o* phi) f
  refine ((pmap_compose_assoc _ _ _)^* @* _).
F, F', X, Y: pType
i: F ->* X
f: X ->* Y
phi: F' <~>* F
cx: IsComplex i f
f o* i o* phi ==* pconst
  refine (pmap_prewhisker _ cx @* _).
F, F', X, Y: pType
i: F ->* X
f: X ->* Y
phi: F' <~>* F
cx: IsComplex i f
pconst o* phi ==* pconst
  apply postcompose_pconst.
Defined.

(** Any pointed map induces a trivial complex. *)
Definition iscomplex_trivial {X Y : pType} (f : X ->* Y)
  : IsComplex (@pconst pUnit X) f.
X, Y: pType
f: X ->* Y
IsComplex pconst f
Proof.
X, Y: pType
f: X ->* Y
IsComplex pconst f
  srapply Build_pHomotopy.
X, Y: pType
f: X ->* Y
f o* pconst == pconst
X, Y: pType
f: X ->* Y
?p pt = dpoint_eq (f o* pconst) @ (dpoint_eq pconst)^
  -
X, Y: pType
f: X ->* Y
f o* pconst == pconst intro x; cbn.
X, Y: pType
f: X ->* Y
x: pUnit
f pt = pt
    exact (point_eq f).
  -
X, Y: pType
f: X ->* Y
((fun x : pUnit =>
  point_eq f : (f o* pconst) x = pconst x)
 :
 f o* pconst == pconst) pt =
dpoint_eq (f o* pconst) @ (dpoint_eq pconst)^ cbn; symmetry.
X, Y: pType
f: X ->* Y
(1 @ point_eq f) @ 1 = point_eq f
    exact (concat_p1 _ @ concat_1p _).
Defined.

(** If Y is a set, then IsComplex is an HProp. *)
Global Instance ishprop_iscomplex_hset `{Funext} {F X Y : pType} `{IsHSet Y}
  (i : F ->* X) (f : X ->* Y)
  : IsHProp (IsComplex i f) := _.

(** ** Very short exact sequences and fiber sequences *)

(** A complex is [n]-exact if the induced map [cxfib] is [n]-connected.  *)
Cumulative Class IsExact (n : Modality) {F X Y : pType} (i : F ->* X) (f : X ->* Y) :=
{
  cx_isexact : IsComplex i f ;
  conn_map_isexact : IsConnMap n (cxfib cx_isexact)
}.

Global Existing Instance conn_map_isexact.

Definition issig_isexact (n : Modality) {F X Y : pType} (i : F ->* X) (f : X ->* Y)
  : _ <~> IsExact n i f := ltac:(issig).

(** If Y is a set, then IsExact is an HProp. *)
Global Instance ishprop_isexact_hset `{Univalence} {F X Y : pType} `{IsHSet Y}
  (n : Modality) (i : F ->* X) (f : X ->* Y)
  : IsHProp (IsExact n i f).
H: Univalence
F, X, Y: pType
IsHSet0: IsHSet Y
n: Modality
i: F ->* X
f: X ->* Y
IsHProp (IsExact n i f)
Proof.
H: Univalence
F, X, Y: pType
IsHSet0: IsHSet Y
n: Modality
i: F ->* X
f: X ->* Y
IsHProp (IsExact n i f)
  rapply (transport (fun A => IsHProp A) (x := { cx : IsComplex i f & IsConnMap n (cxfib cx) })).
H: Univalence
F, X, Y: pType
IsHSet0: IsHSet Y
n: Modality
i: F ->* X
f: X ->* Y
{cx : IsComplex i f & IsConnMap n (cxfib cx)} =
IsExact n i f
H: Univalence
F, X, Y: pType
IsHSet0: IsHSet Y
n: Modality
i: F ->* X
f: X ->* Y
IsHProp {cx : IsComplex i f & IsConnMap n (cxfib cx)}
  2: exact _.
H: Univalence
F, X, Y: pType
IsHSet0: IsHSet Y
n: Modality
i: F ->* X
f: X ->* Y
{cx : IsComplex i f & IsConnMap n (cxfib cx)} =
IsExact n i f
  apply path_universe_uncurried; issig.
Defined.

(** With exactness we can choose preimages. *)
Lemma isexact_preimage (O : Modality) {F X Y : pType}
  (i : F ->* X) (f : X ->* Y) `{IsExact O _ _ _ i f}
  (x : X) (p : f x = point Y)
  : O (hfiber i x).
O: Modality
F, X, Y: pType
i: F ->* X
f: X ->* Y
H: IsExact O i f
x: X
p: f x = pt
O (hfiber i x)
Proof.
O: Modality
F, X, Y: pType
i: F ->* X
f: X ->* Y
H: IsExact O i f
x: X
p: f x = pt
O (hfiber i x)
  rapply (O_functor O (A:=hfiber (cxfib cx_isexact) (x; p))).
O: Modality
F, X, Y: pType
i: F ->* X
f: X ->* Y
H: IsExact O i f
x: X
p: f x = pt
hfiber (cxfib cx_isexact) (x; p) -> hfiber i x
O: Modality
F, X, Y: pType
i: F ->* X
f: X ->* Y
H: IsExact O i f
x: X
p: f x = pt
O (hfiber (cxfib cx_isexact) (x; p))
  -
O: Modality
F, X, Y: pType
i: F ->* X
f: X ->* Y
H: IsExact O i f
x: X
p: f x = pt
hfiber (cxfib cx_isexact) (x; p) -> hfiber i x intros [z q].
O: Modality
F, X, Y: pType
i: F ->* X
f: X ->* Y
H: IsExact O i f
x: X
p: f x = pt
z: F
q: cxfib cx_isexact z = (x; p)
hfiber i x
    exact (z; ap pr1 q).
  -
O: Modality
F, X, Y: pType
i: F ->* X
f: X ->* Y
H: IsExact O i f
x: X
p: f x = pt
O (hfiber (cxfib cx_isexact) (x; p)) apply center, conn_map_isexact.
Defined.

(** Bundled version of the above. *)
Lemma isexact_preimage_hfiber (O : Modality) {F X Y : pType}
  (i : F ->* X) (f : X ->* Y) `{IsExact O _ _ _ i f}
  (x : hfiber f pt)
  : O (hfiber i x.1).
O: Modality
F, X, Y: pType
i: F ->* X
f: X ->* Y
H: IsExact O i f
x: hfiber f pt
O (hfiber i x.1)
Proof.
O: Modality
F, X, Y: pType
i: F ->* X
f: X ->* Y
H: IsExact O i f
x: hfiber f pt
O (hfiber i x.1)
  srapply isexact_preimage; exact x.2.
Defined.

(** If the base is contractible, then [i] is [O]-connected. *)
Definition isconnmap_O_isexact_base_contr (O : Modality@{u}) {F X Y : pType}
  `{Contr Y} (i : F ->* X) (f : X ->* Y)
  `{IsExact@{_ _ u u u} O _ _ _ i f}
  : IsConnMap O i
  := conn_map_compose@{u _ u _} O (cxfib@{u u _ _} cx_isexact) pr1.

(** Passage across homotopies preserves exactness. *)
Definition isexact_homotopic_i 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.
n: Modality
F, X, Y: pType
i, i': F ->* X
ii: i' ==* i
f: X ->* Y
H: IsExact n i f
IsExact n i' f
Proof.
n: Modality
F, X, Y: pType
i, i': F ->* X
ii: i' ==* i
f: X ->* Y
H: IsExact n i f
IsExact n i' f
  exists (iscomplex_homotopic_i ii f cx_isexact).
n: Modality
F, X, Y: pType
i, i': F ->* X
ii: i' ==* i
f: X ->* Y
H: IsExact n i f
IsConnMap n
  (cxfib (iscomplex_homotopic_i ii f cx_isexact))
  refine (conn_map_homotopic n (cxfib cx_isexact) _ _ _).
n: Modality
F, X, Y: pType
i, i': F ->* X
ii: i' ==* i
f: X ->* Y
H: IsExact n i f
cxfib cx_isexact ==
cxfib (iscomplex_homotopic_i ii f cx_isexact)
  intros u; cbn.
n: Modality
F, X, Y: pType
i, i': F ->* X
ii: i' ==* i
f: X ->* Y
H: IsExact n i f
u: F
(i u; cx_isexact u) =
(i' u; ap f (ii u) @ cx_isexact u)
  refine (path_sigma' _ (ii u)^ _).
n: Modality
F, X, Y: pType
i, i': F ->* X
ii: i' ==* i
f: X ->* Y
H: IsExact n i f
u: F
transport (fun x : X => f x = pt) (ii u)^
  (cx_isexact u) = ap f (ii u) @ cx_isexact u
  exact (transport_paths_Fl _ _ @ ((inverse2 (ap_V _ _) @ inv_V _) @@ 1)).
Defined.

Definition isexact_homotopic_f 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'.
n: Modality
F, X, Y: pType
i: F ->* X
f, f': X ->* Y
ff: f' ==* f
H: IsExact n i f
IsExact n i f'
Proof.
n: Modality
F, X, Y: pType
i: F ->* X
f, f': X ->* Y
ff: f' ==* f
H: IsExact n i f
IsExact n i f'
  exists (iscomplex_homotopic_f i ff cx_isexact).
n: Modality
F, X, Y: pType
i: F ->* X
f, f': X ->* Y
ff: f' ==* f
H: IsExact n i f
IsConnMap n
  (cxfib (iscomplex_homotopic_f i ff cx_isexact))
  pose (e := equiv_hfiber_homotopic _ _ ff pt).
n: Modality
F, X, Y: pType
i: F ->* X
f, f': X ->* Y
ff: f' ==* f
H: IsExact n i f
e:= equiv_hfiber_homotopic f' f ff pt: hfiber f' pt <~> hfiber f pt
IsConnMap n
  (cxfib (iscomplex_homotopic_f i ff cx_isexact))
  nrefine (cancelL_isequiv_conn_map n _ e).
n: Modality
F, X, Y: pType
i: F ->* X
f, f': X ->* Y
ff: f' ==* f
H: IsExact n i f
e:= equiv_hfiber_homotopic f' f ff pt: hfiber f' pt <~> hfiber f pt
IsEquiv e
n: Modality
F, X, Y: pType
i: F ->* X
f, f': X ->* Y
ff: f' ==* f
H: IsExact n i f
e:= equiv_hfiber_homotopic f' f ff pt: hfiber f' pt <~> hfiber f pt
IsConnMap n
  (fun x : F =>
   e (cxfib (iscomplex_homotopic_f i ff cx_isexact) x))
  1: apply equiv_isequiv.
n: Modality
F, X, Y: pType
i: F ->* X
f, f': X ->* Y
ff: f' ==* f
H: IsExact n i f
e:= equiv_hfiber_homotopic f' f ff pt: hfiber f' pt <~> hfiber f pt
IsConnMap n
  (fun x : F =>
   e (cxfib (iscomplex_homotopic_f i ff cx_isexact) x))
  refine (conn_map_homotopic n (cxfib (cx_isexact)) _ _ _).
n: Modality
F, X, Y: pType
i: F ->* X
f, f': X ->* Y
ff: f' ==* f
H: IsExact n i f
e:= equiv_hfiber_homotopic f' f ff pt: hfiber f' pt <~> hfiber f pt
cxfib cx_isexact ==
(fun x : F =>
 e (cxfib (iscomplex_homotopic_f i ff cx_isexact) x))
  intro u.
n: Modality
F, X, Y: pType
i: F ->* X
f, f': X ->* Y
ff: f' ==* f
H: IsExact n i f
e:= equiv_hfiber_homotopic f' f ff pt: hfiber f' pt <~> hfiber f pt
u: F
cxfib cx_isexact u =
e (cxfib (iscomplex_homotopic_f i ff cx_isexact) u) simpl.
n: Modality
F, X, Y: pType
i: F ->* X
f, f': X ->* Y
ff: f' ==* f
H: IsExact n i f
e:= equiv_hfiber_homotopic f' f ff pt: hfiber f' pt <~> hfiber f pt
u: F
(i u; cx_isexact u) =
(i u; (ff (i u))^ @ (ff (i u) @ cx_isexact u)) srapply path_hfiber.
n: Modality
F, X, Y: pType
i: F ->* X
f, f': X ->* Y
ff: f' ==* f
H: IsExact n i f
e:= equiv_hfiber_homotopic f' f ff pt: hfiber f' pt <~> hfiber f pt
u: F
(i u; cx_isexact u).1 =
(i u; (ff (i u))^ @ (ff (i u) @ cx_isexact u)).1
n: Modality
F, X, Y: pType
i: F ->* X
f, f': X ->* Y
ff: f' ==* f
H: IsExact n i f
e:= equiv_hfiber_homotopic f' f ff pt: hfiber f' pt <~> hfiber f pt
u: F
(i u; cx_isexact u).2 =
ap f ?q @
(i u; (ff (i u))^ @ (ff (i u) @ cx_isexact u)).2
  1: reflexivity.
n: Modality
F, X, Y: pType
i: F ->* X
f, f': X ->* Y
ff: f' ==* f
H: IsExact n i f
e:= equiv_hfiber_homotopic f' f ff pt: hfiber f' pt <~> hfiber f pt
u: F
(i u; cx_isexact u).2 =
ap f 1 @
(i u; (ff (i u))^ @ (ff (i u) @ cx_isexact u)).2
  refine (concat_1p _ @ concat_V_pp _ _)^.
Defined.

(** And also passage across squares with equivalences. *)
Definition isexact_equiv_i 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).
n: Modality
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
H: IsExact n i f
IsExact n i' (f o* h)
Proof.
n: Modality
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
H: IsExact n i f
IsExact n i' (f o* h)
  exists (iscomplex_equiv_i i i' g h p f cx_isexact); cbn.
n: Modality
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
H: IsExact n i f
IsConnMap n
  (fun x : F' =>
   (i' x;
   1 @ (ap f (p x) @ (1 @ (cx_isexact (g x) @ 1)))))
  snrefine (cancelL_equiv_conn_map n (C := pfiber f) _ _).
n: Modality
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
H: IsExact n i f
hfiber (fun x : X' => f (h x)) pt <~> pfiber f
n: Modality
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
H: IsExact n i f
IsConnMap n
  (?g
   o (fun x : F' =>
      (i' x;
      1 @ (ap f (p x) @ (1 @ (cx_isexact (g x) @ 1))))))
  -
n: Modality
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
H: IsExact n i f
hfiber (fun x : X' => f (h x)) pt <~> pfiber f exact (@equiv_functor_hfiber _ _ _ _ (f o h) f h equiv_idmap
             (fun x => 1%path) (point Y)).
  -
n: Modality
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
H: IsExact n i f
IsConnMap n
  (equiv_functor_hfiber (fun x : X' => 1) pt
   o (fun x : F' =>
      (i' x;
      1 @ (ap f (p x) @ (1 @ (cx_isexact (g x) @ 1)))))) cbn; unfold functor_hfiber, functor_sigma; cbn.
n: Modality
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
H: IsExact n i f
IsConnMap n
  (fun x : F' =>
   (h (i' x);
   1 @
   ap idmap
     (1 @ (ap f (p x) @ (1 @ (cx_isexact (g x) @ 1))))))
    refine (conn_map_homotopic n (@cxfib _ _ _ i f cx_isexact o g) _ _ _).
n: Modality
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
H: IsExact n i f
(fun x : F' => cxfib cx_isexact (g x)) ==
(fun x : F' =>
 (h (i' x);
 1 @
 ap idmap
   (1 @ (ap f (p x) @ (1 @ (cx_isexact (g x) @ 1))))))
    intros u; cbn.
n: Modality
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
H: IsExact n i f
u: F'
(i (g u); cx_isexact (g u)) =
(h (i' u);
1 @
ap idmap
  (1 @ (ap f (p u) @ (1 @ (cx_isexact (g u) @ 1)))))
    refine (path_sigma' _ (p u)^ _).
n: Modality
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
H: IsExact n i f
u: F'
transport (fun x : X => f x = pt) (p u)^
  (cx_isexact (g u)) =
1 @
ap idmap
  (1 @ (ap f (p u) @ (1 @ (cx_isexact (g u) @ 1))))
    abstract (
        rewrite transport_paths_Fl, ap_V, inv_V,
        !concat_1p, concat_p1, ap_idmap;
        reflexivity
      ).
Defined.

(** In particular, we can transfer exactness across equivalences of the total space. *)
Definition moveL_isexact_equiv n {F X X' Y : pType}
  (i : F ->* X) (f : X' ->* Y) (phi : X <~>* X')
  `{IsExact n _ _ _ (phi o* i) f}
  : IsExact n i (f o* phi).
n: Modality
F, X, X', Y: pType
i: F ->* X
f: X' ->* Y
phi: X <~>* X'
H: IsExact n (phi o* i) f
IsExact n i (f o* phi)
Proof.
n: Modality
F, X, X', Y: pType
i: F ->* X
f: X' ->* Y
phi: X <~>* X'
H: IsExact n (phi o* i) f
IsExact n i (f o* phi)
  rapply (isexact_equiv_i _ _ _ pequiv_pmap_idmap phi); cbn.
n: Modality
F, X, X', Y: pType
i: F ->* X
f: X' ->* Y
phi: X <~>* X'
H: IsExact n (phi o* i) f
phi o* i ==* phi o* i o* pmap_idmap
  exact (pmap_precompose_idmap _)^*.
Defined.

(** Similarly, we can cancel equivalences on the fiber. *)
Definition isexact_equiv_fiber 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.
n: Modality
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.
n: Modality
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
  snrapply Build_IsExact.
n: Modality
F, F', X, Y: pType
i: F ->* X
f: X ->* Y
phi: F' <~>* F
E: IsExact n i f
IsComplex (i o* phi) f
n: Modality
F, F', X, Y: pType
i: F ->* X
f: X ->* Y
phi: F' <~>* F
E: IsExact n i f
IsConnMap n (cxfib ?cx_isexact)
  1: apply iscomplex_equiv_fiber, cx_isexact.
n: Modality
F, F', X, Y: pType
i: F ->* X
f: X ->* Y
phi: F' <~>* F
E: IsExact n i f
IsConnMap n (cxfib (iscomplex_equiv_fiber i f phi))
  apply (conn_map_homotopic _ (cxfib cx_isexact o* phi)).
n: Modality
F, F', X, Y: pType
i: F ->* X
f: X ->* Y
phi: F' <~>* F
E: IsExact n i f
cxfib cx_isexact o* phi ==
cxfib (iscomplex_equiv_fiber i f phi)
n: Modality
F, F', X, Y: pType
i: F ->* X
f: X ->* Y
phi: F' <~>* F
E: IsExact n i f
IsConnMap n (cxfib cx_isexact o* phi)
  {
n: Modality
F, F', X, Y: pType
i: F ->* X
f: X ->* Y
phi: F' <~>* F
E: IsExact n i f
cxfib cx_isexact o* phi ==
cxfib (iscomplex_equiv_fiber i f phi) intro x; cbn.
n: Modality
F, F', X, Y: pType
i: F ->* X
f: X ->* Y
phi: F' <~>* F
E: IsExact n i f
x: F'
(i (phi x); cx_isexact (phi x)) =
(i (phi x); 1 @ (cx_isexact (phi x) @ 1))
    by rewrite concat_p1, concat_1p. }
n: Modality
F, F', X, Y: pType
i: F ->* X
f: X ->* Y
phi: F' <~>* F
E: IsExact n i f
IsConnMap n (cxfib cx_isexact o* phi)
  exact _.
Defined.

(** An equivalence of short sequences preserves exactness. *)
Definition isexact_square_if 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'.
n: Modality
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
H: IsExact n i f
IsExact n i' f'
Proof.
n: Modality
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
H: IsExact n i f
IsExact n i' f'
  pose (I := isexact_equiv_i n i i' g h p f).
n: Modality
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
H: IsExact n i f
I:= isexact_equiv_i n i i' g h p f: IsExact n i' (f o* h)
IsExact n i' f'
  pose (I2 := isexact_homotopic_f n i' q).
n: Modality
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
H: IsExact n i f
I:= isexact_equiv_i n i i' g h p f: IsExact n i' (f o* h)
I2:= isexact_homotopic_f n i' q: IsExact n i' (k o* f')
IsExact n i' f'
  exists (iscomplex_cancelL i' f' k cx_isexact).
n: Modality
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
H: IsExact n i f
I:= isexact_equiv_i n i i' g h p f: IsExact n i' (f o* h)
I2:= isexact_homotopic_f n i' q: IsExact n i' (k o* f')
IsConnMap n
  (cxfib (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'))).
n: Modality
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
H: IsExact n i f
I:= isexact_equiv_i n i i' g h p f: IsExact n i' (f o* h)
I2:= isexact_homotopic_f n i' q: IsExact n i' (k o* f')
e:= pequiv_pfiber pequiv_pmap_idmap k
  (pmap_precompose_idmap (k o* f'))^*
:
pfiber f' <~>* pfiber (k o* f'): pfiber f' <~>* pfiber (k o* f')
IsConnMap n
  (cxfib (iscomplex_cancelL i' f' k cx_isexact))
  nrefine (cancelL_isequiv_conn_map n _ e).
n: Modality
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
H: IsExact n i f
I:= isexact_equiv_i n i i' g h p f: IsExact n i' (f o* h)
I2:= isexact_homotopic_f n i' q: IsExact n i' (k o* f')
e:= pequiv_pfiber pequiv_pmap_idmap k
  (pmap_precompose_idmap (k o* f'))^*
:
pfiber f' <~>* pfiber (k o* f'): pfiber f' <~>* pfiber (k o* f')
IsEquiv e
n: Modality
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
H: IsExact n i f
I:= isexact_equiv_i n i i' g h p f: IsExact n i' (f o* h)
I2:= isexact_homotopic_f n i' q: IsExact n i' (k o* f')
e:= pequiv_pfiber pequiv_pmap_idmap k
  (pmap_precompose_idmap (k o* f'))^*
:
pfiber f' <~>* pfiber (k o* f'): pfiber f' <~>* pfiber (k o* f')
IsConnMap n
  (fun x : F' =>
   e (cxfib (iscomplex_cancelL i' f' k cx_isexact) x))
  1: apply pointed_isequiv.
n: Modality
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
H: IsExact n i f
I:= isexact_equiv_i n i i' g h p f: IsExact n i' (f o* h)
I2:= isexact_homotopic_f n i' q: IsExact n i' (k o* f')
e:= pequiv_pfiber pequiv_pmap_idmap k
  (pmap_precompose_idmap (k o* f'))^*
:
pfiber f' <~>* pfiber (k o* f'): pfiber f' <~>* pfiber (k o* f')
IsConnMap n
  (fun x : F' =>
   e (cxfib (iscomplex_cancelL i' f' k cx_isexact) x))
  refine (conn_map_homotopic n (cxfib (cx_isexact)) _ _ _).
n: Modality
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
H: IsExact n i f
I:= isexact_equiv_i n i i' g h p f: IsExact n i' (f o* h)
I2:= isexact_homotopic_f n i' q: IsExact n i' (k o* f')
e:= pequiv_pfiber pequiv_pmap_idmap k
  (pmap_precompose_idmap (k o* f'))^*
:
pfiber f' <~>* pfiber (k o* f'): pfiber f' <~>* pfiber (k o* f')
cxfib cx_isexact ==
(fun x : F' =>
 e (cxfib (iscomplex_cancelL i' f' k cx_isexact) x))
  intro u.
n: Modality
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
H: IsExact n i f
I:= isexact_equiv_i n i i' g h p f: IsExact n i' (f o* h)
I2:= isexact_homotopic_f n i' q: IsExact n i' (k o* f')
e:= pequiv_pfiber pequiv_pmap_idmap k
  (pmap_precompose_idmap (k o* f'))^*
:
pfiber f' <~>* pfiber (k o* f'): pfiber f' <~>* pfiber (k o* f')
u: F'
cxfib cx_isexact u =
e (cxfib (iscomplex_cancelL i' f' k cx_isexact) u) srapply path_hfiber.
n: Modality
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
H: IsExact n i f
I:= isexact_equiv_i n i i' g h p f: IsExact n i' (f o* h)
I2:= isexact_homotopic_f n i' q: IsExact n i' (k o* f')
e:= pequiv_pfiber pequiv_pmap_idmap k
  (pmap_precompose_idmap (k o* f'))^*
:
pfiber f' <~>* pfiber (k o* f'): pfiber f' <~>* pfiber (k o* f')
u: F'
(cxfib cx_isexact u).1 =
(e (cxfib (iscomplex_cancelL i' f' k cx_isexact) u)).1
n: Modality
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
H: IsExact n i f
I:= isexact_equiv_i n i i' g h p f: IsExact n i' (f o* h)
I2:= isexact_homotopic_f n i' q: IsExact n i' (k o* f')
e:= pequiv_pfiber pequiv_pmap_idmap k
  (pmap_precompose_idmap (k o* f'))^*
:
pfiber f' <~>* pfiber (k o* f'): pfiber f' <~>* pfiber (k o* f')
u: F'
(cxfib cx_isexact u).2 =
ap (k o* f') ?q @
(e (cxfib (iscomplex_cancelL i' f' k cx_isexact) u)).2
  {
n: Modality
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
H: IsExact n i f
I:= isexact_equiv_i n i i' g h p f: IsExact n i' (f o* h)
I2:= isexact_homotopic_f n i' q: IsExact n i' (k o* f')
e:= pequiv_pfiber pequiv_pmap_idmap k
  (pmap_precompose_idmap (k o* f'))^*
:
pfiber f' <~>* pfiber (k o* f'): pfiber f' <~>* pfiber (k o* f')
u: F'
(cxfib cx_isexact u).1 =
(e (cxfib (iscomplex_cancelL i' f' k cx_isexact) u)).1 reflexivity. }
n: Modality
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
H: IsExact n i f
I:= isexact_equiv_i n i i' g h p f: IsExact n i' (f o* h)
I2:= isexact_homotopic_f n i' q: IsExact n i' (k o* f')
e:= pequiv_pfiber pequiv_pmap_idmap k
  (pmap_precompose_idmap (k o* f'))^*
:
pfiber f' <~>* pfiber (k o* f'): pfiber f' <~>* pfiber (k o* f')
u: F'
(cxfib cx_isexact u).2 =
ap (k o* f') 1 @
(e (cxfib (iscomplex_cancelL i' f' k cx_isexact) u)).2
  cbn.
n: Modality
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
H: IsExact n i f
I:= isexact_equiv_i n i i' g h p f: IsExact n i' (f o* h)
I2:= isexact_homotopic_f n i' q: IsExact n i' (k o* f')
e:= pequiv_pfiber pequiv_pmap_idmap k
  (pmap_precompose_idmap (k o* f'))^*
:
pfiber f' <~>* pfiber (k o* f'): pfiber f' <~>* pfiber (k o* f')
u: F'
q (i' u) @
(1 @ (ap f (p u) @ (1 @ (cx_isexact (g u) @ 1)))) =
1 @
((1 @
  ap k
    ((((1 @ (1 @ eissect k (f' (i' u)))) @ 1)^ @
      ap k^-1
        (1 @
         (q (i' u) @
          (1 @
           (ap f (p u) @ (1 @ (cx_isexact (g u) @ 1))))))) @
     moveR_equiv_V pt pt (point_eq k)^)) @ point_eq k) unfold moveR_equiv_V.
n: Modality
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
H: IsExact n i f
I:= isexact_equiv_i n i i' g h p f: IsExact n i' (f o* h)
I2:= isexact_homotopic_f n i' q: IsExact n i' (k o* f')
e:= pequiv_pfiber pequiv_pmap_idmap k
  (pmap_precompose_idmap (k o* f'))^*
:
pfiber f' <~>* pfiber (k o* f'): pfiber f' <~>* pfiber (k o* f')
u: F'
q (i' u) @
(1 @ (ap f (p u) @ (1 @ (cx_isexact (g u) @ 1)))) =
1 @
((1 @
  ap k
    ((((1 @ (1 @ eissect k (f' (i' u)))) @ 1)^ @
      ap k^-1
        (1 @
         (q (i' u) @
          (1 @
           (ap f (p u) @ (1 @ (cx_isexact (g u) @ 1))))))) @
     (ap k^-1 (point_eq k)^ @ eissect k pt))) @
 point_eq k) rewrite !concat_1p, !concat_p1, ap_pp_p, ap_pp, (ap_pp k _ (eissect k (point Y'))), ap_V, <- !eisadj.
n: Modality
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
H: IsExact n i f
I:= isexact_equiv_i n i i' g h p f: IsExact n i' (f o* h)
I2:= isexact_homotopic_f n i' q: IsExact n i' (k o* f')
e:= pequiv_pfiber pequiv_pmap_idmap k
  (pmap_precompose_idmap (k o* f'))^*
:
pfiber f' <~>* pfiber (k o* f'): pfiber f' <~>* pfiber (k o* f')
u: F'
q (i' u) @ (ap f (p u) @ cx_isexact (g u)) =
((eisretr k (k (f' (i' u))))^ @
 ap k
   (ap k^-1
      (q (i' u) @ (ap f (p u) @ cx_isexact (g u))))) @
((ap k (ap k^-1 (point_eq k)^) @ eisretr k (k pt)) @
 point_eq k) 
  rewrite <- !ap_compose, concat_pp_p.
n: Modality
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
H: IsExact n i f
I:= isexact_equiv_i n i i' g h p f: IsExact n i' (f o* h)
I2:= isexact_homotopic_f n i' q: IsExact n i' (k o* f')
e:= pequiv_pfiber pequiv_pmap_idmap k
  (pmap_precompose_idmap (k o* f'))^*
:
pfiber f' <~>* pfiber (k o* f'): pfiber f' <~>* pfiber (k o* f')
u: F'
q (i' u) @ (ap f (p u) @ cx_isexact (g u)) =
(eisretr k (k (f' (i' u))))^ @
(ap (fun x : Y => k (k^-1 x))
   (q (i' u) @ (ap f (p u) @ cx_isexact (g u))) @
 ((ap (fun x : Y => k (k^-1 x)) (point_eq k)^ @
   eisretr k (k pt)) @ point_eq k)) 
  rewrite (concat_A1p (eisretr k)), concat_pV_p.
n: Modality
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
H: IsExact n i f
I:= isexact_equiv_i n i i' g h p f: IsExact n i' (f o* h)
I2:= isexact_homotopic_f n i' q: IsExact n i' (k o* f')
e:= pequiv_pfiber pequiv_pmap_idmap k
  (pmap_precompose_idmap (k o* f'))^*
:
pfiber f' <~>* pfiber (k o* f'): pfiber f' <~>* pfiber (k o* f')
u: F'
q (i' u) @ (ap f (p u) @ cx_isexact (g u)) =
(eisretr k (k (f' (i' u))))^ @
(ap (fun x : Y => k (k^-1 x))
   (q (i' u) @ (ap f (p u) @ cx_isexact (g u))) @
 eisretr k pt)
  rewrite (concat_A1p (eisretr k)), concat_V_pp.
n: Modality
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
H: IsExact n i f
I:= isexact_equiv_i n i i' g h p f: IsExact n i' (f o* h)
I2:= isexact_homotopic_f n i' q: IsExact n i' (k o* f')
e:= pequiv_pfiber pequiv_pmap_idmap k
  (pmap_precompose_idmap (k o* f'))^*
:
pfiber f' <~>* pfiber (k o* f'): pfiber f' <~>* pfiber (k o* f')
u: F'
q (i' u) @ (ap f (p u) @ cx_isexact (g u)) =
q (i' u) @ (ap f (p u) @ cx_isexact (g u)) reflexivity.
Defined.

(** If a complex [F -> E -> B] is [O]-exact, the map [F -> B] is [O]-local, and path types in [Y] are [O]-local, then the induced map [cxfib] is an equivalence. *)
Global Instance isequiv_cxfib {O : Modality} {F X Y : pType} {i : F ->* X} {f : X ->* Y}
  `{forall y y' : Y, In O (y = y')} `{MapIn O _ _ i} (ex : IsExact O i f)
  : IsEquiv (cxfib cx_isexact).
O: Modality
F, X, Y: pType
i: F ->* X
f: X ->* Y
H: forall y y' : Y, In O (y = y')
H0: MapIn O i
ex: IsExact O i f
IsEquiv (cxfib cx_isexact)
Proof.
O: Modality
F, X, Y: pType
i: F ->* X
f: X ->* Y
H: forall y y' : Y, In O (y = y')
H0: MapIn O i
ex: IsExact O i f
IsEquiv (cxfib cx_isexact)
  rapply isequiv_conn_ino_map.
O: Modality
F, X, Y: pType
i: F ->* X
f: X ->* Y
H: forall y y' : Y, In O (y = y')
H0: MapIn O i
ex: IsExact O i f
IsConnMap ?Goal (cxfib cx_isexact)
O: Modality
F, X, Y: pType
i: F ->* X
f: X ->* Y
H: forall y y' : Y, In O (y = y')
H0: MapIn O i
ex: IsExact O i f
MapIn ?Goal (cxfib cx_isexact)
  1: apply ex.
O: Modality
F, X, Y: pType
i: F ->* X
f: X ->* Y
H: forall y y' : Y, In O (y = y')
H0: MapIn O i
ex: IsExact O i f
MapIn O (cxfib cx_isexact)
  rapply (cancelL_mapinO _ _ pr1).
Defined.

Definition equiv_cxfib {O : Modality} {F X Y : pType} {i : F ->* X} {f : X ->* Y}
  `{forall y y' : Y, In O (y = y')} `{MapIn O _ _ i} (ex : IsExact O i f)
  : F <~>* pfiber f
  := Build_pEquiv _ _ _ (isequiv_cxfib ex).

Proposition equiv_cxfib_beta {F X Y : pType} {i : F ->* X} {f : X ->* Y}
  `{forall y y' : Y, In O (y = y')} `{MapIn O _ _ i} (ex : IsExact O i f)
  : i o pequiv_inverse (equiv_cxfib ex) == pfib _.
F, X, Y: pType
i: F ->* X
f: X ->* Y
H: forall y y' : Y, In (Tr 0%nat) (y = y')
H0: MapIn (Tr 0%nat) i
ex: IsExact (Tr 0%nat) i f
i o pequiv_inverse (equiv_cxfib ex) == pfib f
Proof.
F, X, Y: pType
i: F ->* X
f: X ->* Y
H: forall y y' : Y, In (Tr 0%nat) (y = y')
H0: MapIn (Tr 0%nat) i
ex: IsExact (Tr 0%nat) i f
i o pequiv_inverse (equiv_cxfib ex) == pfib f
  rapply equiv_ind.
F, X, Y: pType
i: F ->* X
f: X ->* Y
H: forall y y' : Y, In (Tr 0%nat) (y = y')
H0: MapIn (Tr 0%nat) i
ex: IsExact (Tr 0%nat) i f
IsEquiv ?Goal0
F, X, Y: pType
i: F ->* X
f: X ->* Y
H: forall y y' : Y, In (Tr 0%nat) (y = y')
H0: MapIn (Tr 0%nat) i
ex: IsExact (Tr 0%nat) i f
forall x : ?Goal,
i (pequiv_inverse (equiv_cxfib ex) (?Goal0 x)) =
pfib f (?Goal0 x)
  1: exact (isequiv_cxfib ex).
F, X, Y: pType
i: F ->* X
f: X ->* Y
H: forall y y' : Y, In (Tr 0%nat) (y = y')
H0: MapIn (Tr 0%nat) i
ex: IsExact (Tr 0%nat) i f
forall x : F,
i
  (pequiv_inverse (equiv_cxfib ex)
     (cxfib cx_isexact x)) =
pfib f (cxfib cx_isexact x)
  intro x.
F, X, Y: pType
i: F ->* X
f: X ->* Y
H: forall y y' : Y, In (Tr 0%nat) (y = y')
H0: MapIn (Tr 0%nat) i
ex: IsExact (Tr 0%nat) i f
x: F
i
  (pequiv_inverse (equiv_cxfib ex)
     (cxfib cx_isexact x)) =
pfib f (cxfib cx_isexact x)
  exact (ap (fun g => i g) (eissect _ x)).
Defined.

(** A purely exact sequence is [O]-exact for any modality [O]. *)
Definition isexact_purely_O {O : Modality} {F X Y : pType}
  (i : F ->* X) (f : X ->* Y) `{IsExact purely _ _ _ i f}
  : IsExact O i f.
O: Modality
F, X, Y: pType
i: F ->* X
f: X ->* Y
H: IsExact purely i f
IsExact O i f
Proof.
O: Modality
F, X, Y: pType
i: F ->* X
f: X ->* Y
H: IsExact purely i f
IsExact O i f
  srapply Build_IsExact.
O: Modality
F, X, Y: pType
i: F ->* X
f: X ->* Y
H: IsExact purely i f
IsComplex i f
O: Modality
F, X, Y: pType
i: F ->* X
f: X ->* Y
H: IsExact purely i f
IsConnMap O (cxfib ?cx_isexact)
  1: apply cx_isexact.
O: Modality
F, X, Y: pType
i: F ->* X
f: X ->* Y
H: IsExact purely i f
IsConnMap O (cxfib cx_isexact)
  exact _.
Defined.

(** When [n] is the identity modality [purely], so that [cxfib] is an equivalence, we get simply a fiber sequence.  In particular, the fiber of a given map yields an purely-exact sequence. *)

Definition iscomplex_pfib {X Y} (f : X ->* Y)
  : IsComplex (pfib f) f.
X, Y: pType
f: X ->* Y
IsComplex (pfib f) f
Proof.
X, Y: pType
f: X ->* Y
IsComplex (pfib f) f
  srapply Build_pHomotopy.
X, Y: pType
f: X ->* Y
f o* pfib f == pconst
X, Y: pType
f: X ->* Y
?p pt = dpoint_eq (f o* pfib f) @ (dpoint_eq pconst)^
  -
X, Y: pType
f: X ->* Y
f o* pfib f == pconst intros [x p]; exact p.
  -
X, Y: pType
f: X ->* Y
((fun x0 : pfiber f => (fun x : X => idmap) x0.1 x0.2)
 :
 f o* pfib f == pconst) pt =
dpoint_eq (f o* pfib f) @ (dpoint_eq pconst)^ cbn.
X, Y: pType
f: X ->* Y
point_eq f = (1 @ point_eq f) @ 1 exact (concat_p1 _ @ concat_1p _)^.
Defined.

Global Instance isexact_pfib {X Y} (f : X ->* Y)
  : IsExact purely (pfib f) f.
X, Y: pType
f: X ->* Y
IsExact purely (pfib f) f
Proof.
X, Y: pType
f: X ->* Y
IsExact purely (pfib f) f
  exists (iscomplex_pfib f).
X, Y: pType
f: X ->* Y
IsConnMap purely (cxfib (iscomplex_pfib f))
  exact _.
Defined.

(** Fiber sequences can alternatively be defined as an equivalence to the fiber of some map. *)
Definition FiberSeq (F X Y : pType) := { f : X ->* Y & F <~>* pfiber f }.

Definition i_fiberseq {F X Y} (fs : FiberSeq F X Y)
  : F ->* X
  := pfib fs.1 o* fs.2.

Global Instance isexact_purely_fiberseq {F X Y : pType} (fs : FiberSeq F X Y)
  : IsExact purely (i_fiberseq fs) fs.1.
F, X, Y: pType
fs: FiberSeq F X Y
IsExact purely (i_fiberseq fs) fs.1
Proof.
F, X, Y: pType
fs: FiberSeq F X Y
IsExact purely (i_fiberseq fs) fs.1
  srapply Build_IsExact; [ srapply Build_pHomotopy | ].
F, X, Y: pType
fs: FiberSeq F X Y
fs.1 o* i_fiberseq fs == pconst
F, X, Y: pType
fs: FiberSeq F X Y
?p pt =
dpoint_eq (fs.1 o* i_fiberseq fs) @
(dpoint_eq pconst)^
F, X, Y: pType
fs: FiberSeq F X Y
IsConnMap purely (cxfib (Build_pHomotopy ?p ?q))
  -
F, X, Y: pType
fs: FiberSeq F X Y
fs.1 o* i_fiberseq fs == pconst intros u; cbn.
F, X, Y: pType
fs: FiberSeq F X Y
u: F
fs.1 (fs.2 u).1 = pt 
    exact ((fs.2 u).2).
  -
F, X, Y: pType
fs: FiberSeq F X Y
((fun u : F =>
  (fs.2 u).2 : (fs.1 o* i_fiberseq fs) u = pconst u)
 :
 fs.1 o* i_fiberseq fs == pconst) pt =
dpoint_eq (fs.1 o* i_fiberseq fs) @
(dpoint_eq pconst)^ apply moveL_pV.
F, X, Y: pType
fs: FiberSeq F X Y
(fs.2 pt).2 @ dpoint_eq pconst =
dpoint_eq (fs.1 o* i_fiberseq fs) cbn.
F, X, Y: pType
fs: FiberSeq F X Y
(fs.2 pt).2 @ 1 =
ap fs.1 (ap pr1 (point_eq fs.2) @ 1) @ point_eq fs.1
    refine (concat_p1 _ @ _).
F, X, Y: pType
fs: FiberSeq F X Y
(fs.2 pt).2 =
ap fs.1 (ap pr1 (point_eq fs.2) @ 1) @ point_eq fs.1
    apply moveL_Mp.
F, X, Y: pType
fs: FiberSeq F X Y
(ap fs.1 (ap pr1 (point_eq fs.2) @ 1))^ @ (fs.2 pt).2 =
point_eq fs.1
    refine (_ @ (point_eq fs.2)..2).
F, X, Y: pType
fs: FiberSeq F X Y
(ap fs.1 (ap pr1 (point_eq fs.2) @ 1))^ @ (fs.2 pt).2 =
transport (fun x : X => fs.1 x = pt)
  (point_eq fs.2) ..1 (fs.2 pt).2
    refine (_ @ (transport_paths_Fl _ _)^).
F, X, Y: pType
fs: FiberSeq F X Y
(ap fs.1 (ap pr1 (point_eq fs.2) @ 1))^ @ (fs.2 pt).2 =
(ap fs.1 (point_eq fs.2) ..1)^ @ (fs.2 pt).2
    apply whiskerR, inverse2, ap, concat_p1.
  -
F, X, Y: pType
fs: FiberSeq F X Y
IsConnMap purely
  (cxfib
     (Build_pHomotopy
        ((fun u : F =>
          (fs.2 u).2
          :
          (fs.1 o* i_fiberseq fs) u = pconst u)
         :
         fs.1 o* i_fiberseq fs == pconst)
        (moveL_pV (dpoint_eq pconst) (fs.2 pt).2
           (dpoint_eq (fs.1 o* i_fiberseq fs))
           (concat_p1 (fs.2 pt).2 @
            moveL_Mp (point_eq fs.1) (fs.2 pt).2
              (ap fs.1 (ap pr1 (point_eq fs.2) @ 1))
              ((whiskerR
                  (inverse2
                     (ap (ap fs.1)
                        (concat_p1 (point_eq fs.2) ..1)))
                  (fs.2 pt).2 @
                (transport_paths_Fl
                   (point_eq fs.2) ..1 (fs.2 pt).2)^) @
               (point_eq fs.2) ..2)
            :
            (fs.2 pt).2 @ dpoint_eq pconst =
            dpoint_eq (fs.1 o* i_fiberseq fs))))) intros [x p].
F, X, Y: pType
fs: FiberSeq F X Y
x: X
p: fs.1 x = pt
IsConnected purely
  (hfiber
     (cxfib
        (Build_pHomotopy (fun u : F => (fs.2 u).2)
           (moveL_pV (dpoint_eq pconst) (fs.2 pt).2
              (dpoint_eq (fs.1 o* i_fiberseq fs))
              (concat_p1 (fs.2 pt).2 @
               moveL_Mp (point_eq fs.1) (fs.2 pt).2
                 (ap fs.1 (ap pr1 (point_eq fs.2) @ 1))
                 ((whiskerR
                     (inverse2
                        (ap (ap fs.1)
                           (concat_p1
                              (point_eq fs.2) ..1)))
                     (fs.2 pt).2 @
                   (transport_paths_Fl
                      (point_eq fs.2) ..1 (fs.2 pt).2)^) @
                  (point_eq fs.2) ..2))))) (x; p))
    apply contr_map_isequiv.
F, X, Y: pType
fs: FiberSeq F X Y
x: X
p: fs.1 x = pt
IsEquiv
  (cxfib
     (Build_pHomotopy (fun u : F => (fs.2 u).2)
        (moveL_pV (dpoint_eq pconst) (fs.2 pt).2
           (dpoint_eq (fs.1 o* i_fiberseq fs))
           (concat_p1 (fs.2 pt).2 @
            moveL_Mp (point_eq fs.1) (fs.2 pt).2
              (ap fs.1 (ap pr1 (point_eq fs.2) @ 1))
              ((whiskerR
                  (inverse2
                     (ap (ap fs.1)
                        (concat_p1 (point_eq fs.2) ..1)))
                  (fs.2 pt).2 @
                (transport_paths_Fl
                   (point_eq fs.2) ..1 (fs.2 pt).2)^) @
               (point_eq fs.2) ..2)))))
    change (IsEquiv fs.2); exact _.
Defined.

Definition pequiv_cxfib {F X Y : pType} {i : F ->* X} {f : X ->* Y}
  `{IsExact purely F X Y i f}
  : F <~>* pfiber f
  := Build_pEquiv _ _ (cxfib cx_isexact) _.

Definition fiberseq_isexact_purely {F X Y : pType} (i : F ->* X) (f : X ->* Y)
  `{IsExact purely F X Y i f} : FiberSeq F X Y
  := (f; pequiv_cxfib).

(** It's easier to show that [loops] preserves fiber sequences than that it preserves purely-exact sequences. *)
Definition fiberseq_loops {F X Y} (fs : FiberSeq F X Y)
  : FiberSeq (loops F) (loops X) (loops Y).
F, X, Y: pType
fs: FiberSeq F X Y
FiberSeq (loops F) (loops X) (loops Y)
Proof.
F, X, Y: pType
fs: FiberSeq F X Y
FiberSeq (loops F) (loops X) (loops Y)
  (** TODO: doesn't work?! *)
(*   exists (fmap loops fs.1). *)
  refine (fmap loops fs.1; _).
F, X, Y: pType
fs: FiberSeq F X Y
loops F <~>* pfiber (fmap loops fs.1)
  refine (_ o*E emap loops fs.2).
F, X, Y: pType
fs: FiberSeq F X Y
loops (pfiber fs.1) <~>* pfiber (fmap loops fs.1)
  exact (pfiber_fmap_loops fs.1)^-1*.
Defined.

(** Now we can deduce that [loops] preserves purely-exact sequences. The hardest part is modifying the first map back to [fmap loops i]. *)
Global Instance isexact_loops {F X Y} (i : F ->* X) (f : X ->* Y)
  `{IsExact purely F X Y i f}
  : IsExact purely (fmap loops i) (fmap loops f).
F, X, Y: pType
i: F ->* X
f: X ->* Y
H: IsExact purely i f
IsExact purely (fmap loops i) (fmap loops f)
Proof.
F, X, Y: pType
i: F ->* X
f: X ->* Y
H: IsExact purely i f
IsExact purely (fmap loops i) (fmap loops f)
  refine (@isexact_homotopic_i purely _ _ _ _ (fmap loops i) _ (fmap loops f)
    (isexact_purely_fiberseq (fiberseq_loops (fiberseq_isexact_purely i f)))).
F, X, Y: pType
i: F ->* X
f: X ->* Y
H: IsExact purely i f
fmap loops i ==*
i_fiberseq
  (fiberseq_loops (fiberseq_isexact_purely i f))
  transitivity (fmap loops (pfib f) o* fmap loops (cxfib cx_isexact)).
F, X, Y: pType
i: F ->* X
f: X ->* Y
H: IsExact purely i f
fmap loops i ==*
fmap loops (pfib f) o* fmap loops (cxfib cx_isexact)
F, X, Y: pType
i: F ->* X
f: X ->* Y
H: IsExact purely i f
fmap loops (pfib f) o* fmap loops (cxfib cx_isexact) ==*
i_fiberseq
  (fiberseq_loops (fiberseq_isexact_purely i f))
  -
F, X, Y: pType
i: F ->* X
f: X ->* Y
H: IsExact purely i f
fmap loops i ==*
fmap loops (pfib f) o* fmap loops (cxfib cx_isexact) refine (_ @* fmap_comp loops _ _).
F, X, Y: pType
i: F ->* X
f: X ->* Y
H: IsExact purely i f
fmap loops i ==*
fmap loops (pfib f $o cxfib cx_isexact)
    rapply (fmap2 loops).
F, X, Y: pType
i: F ->* X
f: X ->* Y
H: IsExact purely i f
i $== pfib f $o cxfib cx_isexact
    symmetry; apply pfib_cxfib.
  -
F, X, Y: pType
i: F ->* X
f: X ->* Y
H: IsExact purely i f
fmap loops (pfib f) o* fmap loops (cxfib cx_isexact) ==*
i_fiberseq
  (fiberseq_loops (fiberseq_isexact_purely i f)) refine (_ @* pmap_compose_assoc _ _ _).
F, X, Y: pType
i: F ->* X
f: X ->* Y
H: IsExact purely i f
fmap loops (pfib f) o* fmap loops (cxfib cx_isexact) ==*
pfib (fiberseq_loops (fiberseq_isexact_purely i f)).1
o* (pfiber_fmap_loops (fiberseq_isexact_purely i f).1)^-1*
o* emap loops (fiberseq_isexact_purely i f).2
    refine (pmap_prewhisker (fmap loops (cxfib cx_isexact)) _).
F, X, Y: pType
i: F ->* X
f: X ->* Y
H: IsExact purely i f
fmap loops (pfib f) ==*
pfib (fiberseq_loops (fiberseq_isexact_purely i f)).1
o* (pfiber_fmap_loops (fiberseq_isexact_purely i f).1)^-1*
    apply moveR_pequiv_fV.
F, X, Y: pType
i: F ->* X
f: X ->* Y
H: IsExact purely i f
fmap loops (pfib f)
o* pfiber_fmap_loops (fiberseq_isexact_purely i f).1 ==*
pfib (fiberseq_loops (fiberseq_isexact_purely i f)).1
    apply pr1_pfiber_fmap_loops.
Defined.

Global Instance isexact_iterated_loops {F X Y}
  (i : F ->* X) (f : X ->* Y) `{IsExact purely F X Y i f} (n : nat)
  : IsExact purely (fmap (iterated_loops n) i) (fmap (iterated_loops n) f).
F, X, Y: pType
i: F ->* X
f: X ->* Y
H: IsExact purely i f
n: nat
IsExact purely (fmap (iterated_loops n) i)
  (fmap (iterated_loops n) f)
Proof.
F, X, Y: pType
i: F ->* X
f: X ->* Y
H: IsExact purely i f
n: nat
IsExact purely (fmap (iterated_loops n) i)
  (fmap (iterated_loops n) f)
  induction n as [|n IHn]; [ assumption | apply isexact_loops; assumption ].
Defined.

(** (n.+1)-truncation preserves n-exactness. *)
Global Instance isexact_ptr `{Univalence} (n : trunc_index)
  {F X Y : pType} (i : F ->* X) (f : X ->* Y)
  `{IsExact (Tr n) F X Y i f}
  : IsExact (Tr n) (fmap (pTr n.+1) i) (fmap (pTr n.+1) f).
H: Univalence
n: trunc_index
F, X, Y: pType
i: F ->* X
f: X ->* Y
H0: IsExact (Tr n) i f
IsExact (Tr n) (fmap (pTr n.+1) i) (fmap (pTr n.+1) f)
Proof.
H: Univalence
n: trunc_index
F, X, Y: pType
i: F ->* X
f: X ->* Y
H0: IsExact (Tr n) i f
IsExact (Tr n) (fmap (pTr n.+1) i) (fmap (pTr n.+1) f)
  exists (iscomplex_ptr n.+1 i f cx_isexact).
H: Univalence
n: trunc_index
F, X, Y: pType
i: F ->* X
f: X ->* Y
H0: IsExact (Tr n) i f
IsConnMap (Tr n)
  (cxfib (iscomplex_ptr n.+1 i f cx_isexact))
  srefine (cancelR_conn_map (Tr n) (@tr n.+1 F) 
    (@cxfib _ _ _ (fmap (pTr n.+1) i) (fmap (pTr n.+1) f) _)).
H: Univalence
n: trunc_index
F, X, Y: pType
i: F ->* X
f: X ->* Y
H0: IsExact (Tr n) i f
IsConnMap (Tr n) tr
H: Univalence
n: trunc_index
F, X, Y: pType
i: F ->* X
f: X ->* Y
H0: IsExact (Tr n) i f
IsConnMap (Tr n)
  (cxfib (iscomplex_ptr n.+1 i f cx_isexact) o tr)
  {
H: Univalence
n: trunc_index
F, X, Y: pType
i: F ->* X
f: X ->* Y
H0: IsExact (Tr n) i f
IsConnMap (Tr n) tr intros x; rapply isconnected_pred. }
H: Univalence
n: trunc_index
F, X, Y: pType
i: F ->* X
f: X ->* Y
H0: IsExact (Tr n) i f
IsConnMap (Tr n)
  (cxfib (iscomplex_ptr n.+1 i f cx_isexact) o tr)
  nrapply conn_map_homotopic.
H: Univalence
n: trunc_index
F, X, Y: pType
i: F ->* X
f: X ->* Y
H0: IsExact (Tr n) i f
?Goal ==
(fun x : F =>
 cxfib (iscomplex_ptr n.+1 i f cx_isexact) (tr x))
H: Univalence
n: trunc_index
F, X, Y: pType
i: F ->* X
f: X ->* Y
H0: IsExact (Tr n) i f
IsConnMap (Tr n) ?Goal
  2:nrapply (conn_map_compose _ (cxfib _)
               (functor_hfiber (fun y => (to_O_natural (Tr n.+1) f y)^)
                               (point Y))).
H: Univalence
n: trunc_index
F, X, Y: pType
i: F ->* X
f: X ->* Y
H0: IsExact (Tr n) i f
(fun x : F =>
 functor_hfiber
   (fun y : X => (to_O_natural (Tr n.+1) f y)^) pt
   (cxfib ?Goal1 x)) ==
(fun x : F =>
 cxfib (iscomplex_ptr n.+1 i f cx_isexact) (tr x))
H: Univalence
n: trunc_index
F, X, Y: pType
i: F ->* X
f: X ->* Y
H0: IsExact (Tr n) i f
IsConnMap (Tr n) (cxfib ?Goal1)
H: Univalence
n: trunc_index
F, X, Y: pType
i: F ->* X
f: X ->* Y
H0: IsExact (Tr n) i f
IsConnMap (Tr n)
  (functor_hfiber
     (fun y : X => (to_O_natural (Tr n.+1) f y)^) pt)
  3:pose @O_lex_leq_Tr; rapply (OO_conn_map_functor_hfiber_to_O).
H: Univalence
n: trunc_index
F, X, Y: pType
i: F ->* X
f: X ->* Y
H0: IsExact (Tr n) i f
(fun x : F =>
 functor_hfiber
   (fun y : X => (to_O_natural (Tr n.+1) f y)^) pt
   (cxfib ?Goal1 x)) ==
(fun x : F =>
 cxfib (iscomplex_ptr n.+1 i f cx_isexact) (tr x))
H: Univalence
n: trunc_index
F, X, Y: pType
i: F ->* X
f: X ->* Y
H0: IsExact (Tr n) i f
IsConnMap (Tr n) (cxfib ?Goal1)
  -
H: Univalence
n: trunc_index
F, X, Y: pType
i: F ->* X
f: X ->* Y
H0: IsExact (Tr n) i f
(fun x : F =>
 functor_hfiber
   (fun y : X => (to_O_natural (Tr n.+1) f y)^) pt
   (cxfib ?Goal1 x)) ==
(fun x : F =>
 cxfib (iscomplex_ptr n.+1 i f cx_isexact) (tr x)) intros x; refine (path_sigma' _ 1 _); cbn.
H: Univalence
n: trunc_index
F, X, Y: pType
i: F ->* X
f: X ->* Y
H0: IsExact (Tr n) i f
x: F
((to_O_natural (Tr n.+1) f (i x))^)^ @ ap tr (?Goal x) =
1 @ (ap tr (cx_isexact x) @ 1)
    (* This is even simpler than it looks, because for truncations [to_O_natural n.+1 := 1], [to n.+1 := tr], and [cx_const := H]. *)
    exact (1 @@ (concat_p1 _)^).
  -
H: Univalence
n: trunc_index
F, X, Y: pType
i: F ->* X
f: X ->* Y
H0: IsExact (Tr n) i f
IsConnMap (Tr n) (cxfib cx_isexact) exact _.
Defined.

(** In particular, (n.+1)-truncation takes fiber sequences to n-exact ones. *)
Global Instance isexact_ptr_purely `{Univalence} (n : trunc_index)
  {F X Y : pType} (i : F ->* X) (f : X ->* Y) `{IsExact purely F X Y i f}
  : IsExact (Tr n) (fmap (pTr n.+1) i) (fmap (pTr n.+1) f).
H: Univalence
n: trunc_index
F, X, Y: pType
i: F ->* X
f: X ->* Y
H0: IsExact purely i f
IsExact (Tr n) (fmap (pTr n.+1) i) (fmap (pTr n.+1) f)
Proof.
H: Univalence
n: trunc_index
F, X, Y: pType
i: F ->* X
f: X ->* Y
H0: IsExact purely i f
IsExact (Tr n) (fmap (pTr n.+1) i) (fmap (pTr n.+1) f)
  rapply isexact_ptr.
H: Univalence
n: trunc_index
F, X, Y: pType
i: F ->* X
f: X ->* Y
H0: IsExact purely i f
IsExact (Tr n) i f
  exists cx_isexact.
H: Univalence
n: trunc_index
F, X, Y: pType
i: F ->* X
f: X ->* Y
H0: IsExact purely i f
IsConnMap (Tr n) (cxfib cx_isexact)
  intros z; apply isconnected_contr.
H: Univalence
n: trunc_index
F, X, Y: pType
i: F ->* X
f: X ->* Y
H0: IsExact purely i f
z: pfiber f
Contr (hfiber (cxfib cx_isexact) z)
  exact (conn_map_isexact (f := f) (i := i) z).
Defined.

(** ** Connecting maps *)

(** It's useful to see [pfib_cxfib] as a degenerate square. *)
Definition square_pfib_pequiv_cxfib {F X Y : pType}
  (i : F ->* X) (f : X ->* Y) `{IsExact purely F X Y i f}
  : pequiv_pmap_idmap o* i ==* pfib f o* pequiv_cxfib.
F, X, Y: pType
i: F ->* X
f: X ->* Y
H: IsExact purely i f
pequiv_pmap_idmap o* i ==* pfib f o* pequiv_cxfib
Proof.
F, X, Y: pType
i: F ->* X
f: X ->* Y
H: IsExact purely i f
pequiv_pmap_idmap o* i ==* pfib f o* pequiv_cxfib
  unfold Square.
F, X, Y: pType
i: F ->* X
f: X ->* Y
H: IsExact purely i f
pequiv_pmap_idmap o* i ==* pfib f o* pequiv_cxfib
  refine (pmap_postcompose_idmap _ @* _).
F, X, Y: pType
i: F ->* X
f: X ->* Y
H: IsExact purely i f
i ==* pfib f o* pequiv_cxfib
  symmetry; apply pfib_cxfib.
Defined.

(** The connecting maps for the long exact sequence of loop spaces, defined as an extension to a fiber sequence. *)
Definition connect_fiberseq {F X Y}
  (i : F ->* X) (f : X ->* Y) `{IsExact purely F X Y i f}
  : FiberSeq (loops Y) F X.
F, X, Y: pType
i: F ->* X
f: X ->* Y
H: IsExact purely i f
FiberSeq (loops Y) F X
Proof.
F, X, Y: pType
i: F ->* X
f: X ->* Y
H: IsExact purely i f
FiberSeq (loops Y) F X
  exists i.
F, X, Y: pType
i: F ->* X
f: X ->* Y
H: IsExact purely i f
loops Y <~>* pfiber i
  exact (((pfiber2_loops f) o*E (pequiv_pfiber _ _ (square_pfib_pequiv_cxfib i f)))^-1*).
Defined.

Definition connecting_map {F X Y}
  (i : F ->* X) (f : X ->* Y) `{IsExact purely F X Y i f}
  : loops Y ->* F
  := i_fiberseq (connect_fiberseq i f).

Global Instance isexact_connect_R {F X Y}
  (i : F ->* X) (f : X ->* Y) `{IsExact purely F X Y i f}
  : IsExact purely (fmap loops f) (connecting_map i f).
F, X, Y: pType
i: F ->* X
f: X ->* Y
H: IsExact purely i f
IsExact purely (fmap loops f) (connecting_map i f)
Proof.
F, X, Y: pType
i: F ->* X
f: X ->* Y
H: IsExact purely i f
IsExact purely (fmap loops f) (connecting_map i f)
  refine (isexact_equiv_i (Y := F) purely
          (pfib (pfib i)) (fmap loops f)
          (((loops_inv X) o*E
            (pfiber2_loops (pfib f)) o*E
           (pequiv_pfiber _ _ (square_pequiv_pfiber _ _ (square_pfib_pequiv_cxfib i f))))^-1*)
          (((pfiber2_loops f) o*E (pequiv_pfiber _ _ (square_pfib_pequiv_cxfib i f)))^-1*)
          _ (pfib i)).
F, X, Y: pType
i: F ->* X
f: X ->* Y
H: IsExact purely i f
(pfiber2_loops f
 o*E pequiv_pfiber pequiv_cxfib pequiv_pmap_idmap
       (square_pfib_pequiv_cxfib i f))^-1*
o* fmap loops f ==*
pfib (pfib i)
o* (loops_inv X o*E pfiber2_loops (pfib f)
    o*E pequiv_pfiber
          (pequiv_pfiber pequiv_cxfib
             pequiv_pmap_idmap
             (square_pfib_pequiv_cxfib i f))
          pequiv_cxfib
          (square_pequiv_pfiber pequiv_cxfib
             pequiv_pmap_idmap
             (square_pfib_pequiv_cxfib i f)))^-1*
  refine (vinverse 
            ((loops_inv X) o*E
             (pfiber2_loops (pfib f)) o*E
             (pequiv_pfiber _ _ (square_pequiv_pfiber _ _ (square_pfib_pequiv_cxfib i f))))
            ((pfiber2_loops f) o*E (pequiv_pfiber _ _ (square_pfib_pequiv_cxfib i f))) _).
F, X, Y: pType
i: F ->* X
f: X ->* Y
H: IsExact purely i f
Square
  (loops_inv X o*E pfiber2_loops (pfib f)
   o*E pequiv_pfiber
         (pequiv_pfiber pequiv_cxfib pequiv_pmap_idmap
            (square_pfib_pequiv_cxfib i f))
         pequiv_cxfib
         (square_pequiv_pfiber pequiv_cxfib
            pequiv_pmap_idmap
            (square_pfib_pequiv_cxfib i f)))
  (pfiber2_loops f
   o*E pequiv_pfiber pequiv_cxfib pequiv_pmap_idmap
         (square_pfib_pequiv_cxfib i f))
  (pfib (pfib i)) (fmap loops f)
  refine (vconcat (f03 := loops_inv X o* pfiber2_loops (pfib f))
                  (f01 := pequiv_pfiber _ _ (square_pequiv_pfiber _ _ (square_pfib_pequiv_cxfib i f)))
                  (f23 := pfiber2_loops f)
                  (f21 := pequiv_pfiber _ _ (square_pfib_pequiv_cxfib i f)) _ _).
F, X, Y: pType
i: F ->* X
f: X ->* Y
H: IsExact purely i f
Square
  (pequiv_pfiber
     (pequiv_pfiber pequiv_cxfib pequiv_pmap_idmap
        (square_pfib_pequiv_cxfib i f)) pequiv_cxfib
     (square_pequiv_pfiber pequiv_cxfib
        pequiv_pmap_idmap
        (square_pfib_pequiv_cxfib i f)))
  (pequiv_pfiber pequiv_cxfib pequiv_pmap_idmap
     (square_pfib_pequiv_cxfib i f)) (pfib (pfib i))
  ?Goal
F, X, Y: pType
i: F ->* X
f: X ->* Y
H: IsExact purely i f
Square (loops_inv X o* pfiber2_loops (pfib f))
  (pfiber2_loops f) ?Goal (fmap loops f)
  -
F, X, Y: pType
i: F ->* X
f: X ->* Y
H: IsExact purely i f
Square
  (pequiv_pfiber
     (pequiv_pfiber pequiv_cxfib pequiv_pmap_idmap
        (square_pfib_pequiv_cxfib i f)) pequiv_cxfib
     (square_pequiv_pfiber pequiv_cxfib
        pequiv_pmap_idmap
        (square_pfib_pequiv_cxfib i f)))
  (pequiv_pfiber pequiv_cxfib pequiv_pmap_idmap
     (square_pfib_pequiv_cxfib i f)) (pfib (pfib i))
  ?Goal exact (square_pequiv_pfiber _ _ (square_pequiv_pfiber _ _ (square_pfib_pequiv_cxfib i f))).
  -
F, X, Y: pType
i: F ->* X
f: X ->* Y
H: IsExact purely i f
Square (loops_inv X o* pfiber2_loops (pfib f))
  (pfiber2_loops f) (pfib (pfib (pfib f)))
  (fmap loops f) exact (pfiber2_fmap_loops f).
Defined.

(** The connecting map associated to a pointed family. *)
Definition connecting_map_family {Y : pType} (P : pFam Y)
  : loops Y ->* [P pt, dpoint P].
Y: pType
P: pFam Y
loops Y ->* [P pt, dpoint P]
Proof.
Y: pType
P: pFam Y
loops Y ->* [P pt, dpoint P]
  srapply Build_pMap.
Y: pType
P: pFam Y
loops Y -> [P pt, dpoint P]
Y: pType
P: pFam Y
?Goal pt = pt
  -
Y: pType
P: pFam Y
loops Y -> [P pt, dpoint P] intro l.
Y: pType
P: pFam Y
l: loops Y
[P pt, dpoint P]
    apply (transport P l).
Y: pType
P: pFam Y
l: loops Y
P pt
    apply P.
  -
Y: pType
P: pFam Y
(fun l : loops Y =>
 transport P l (let X := dpoint P in X)) pt = pt reflexivity.
Defined.

(** ** Long exact sequences *)

Record LongExactSequence (k : Modality) (N : SuccStr) : Type :=
{
  les_carrier : N -> pType;
  les_fn : forall n, les_carrier n.+1 ->* les_carrier n;
  les_isexact : forall n, IsExact k (les_fn n.+1) (les_fn n)
}.

Coercion les_carrier : LongExactSequence >-> Funclass.
Arguments les_fn {k N} S n : rename.
Global Existing Instance les_isexact.

(** Long exact sequences are preserved by truncation. *)
Definition trunc_les `{Univalence} (k : trunc_index) {N : SuccStr}
  (S : LongExactSequence purely N)
  : LongExactSequence (Tr k) N
  := Build_LongExactSequence
       (Tr k) N (fun n => pTr k.+1 (S n))
       (fun n => fmap (pTr k.+1) (les_fn S n)) _.


(** ** LES of loop spaces and homotopy groups *)

Definition loops_carrier (F X Y : pType) (n : N3) : pType :=
  match n with
  | (n, inl (inl (inl x))) => Empty_ind _ x
  | (n, inl (inl (inr tt))) => iterated_loops n Y
  | (n, inl (inr tt)) => iterated_loops n X
  | (n, inr tt) => iterated_loops n F
  end.

(** Starting from a fiber sequence, we can obtain a long purely-exact sequence of loop spaces. *)
Definition loops_les {F X Y : pType}
  (i : F ->* X) (f : X ->* Y) `{IsExact purely F X Y i f}
  : LongExactSequence purely (N3).
F, X, Y: pType
i: F ->* X
f: X ->* Y
H: IsExact purely i f
LongExactSequence purely (N3)
Proof.
F, X, Y: pType
i: F ->* X
f: X ->* Y
H: IsExact purely i f
LongExactSequence purely (N3)
  srefine (Build_LongExactSequence purely (N3) (loops_carrier F X Y) _ _).
F, X, Y: pType
i: F ->* X
f: X ->* Y
H: IsExact purely i f
forall n : N3,
loops_carrier F X Y n.+1 ->* loops_carrier F X Y n
F, X, Y: pType
i: F ->* X
f: X ->* Y
H: IsExact purely i f
forall n : N3,
IsExact purely (?les_fn n.+1) (?les_fn n)
  all:intros [n [[[[]|[]]|[]]|[]]]; cbn.
F, X, Y: pType
i: F ->* X
f: X ->* Y
H: IsExact purely i f
n: +N
(fix F (m : nat) : pType :=
   match m with
   | 0%nat => X
   | (m'.+1)%nat => loops (F m')
   end) n ->*
(fix F (m : nat) : pType :=
   match m with
   | 0%nat => Y
   | (m'.+1)%nat => loops (F m')
   end) n
F, X, Y: pType
i: F ->* X
f: X ->* Y
H: IsExact purely i f
n: +N
(fix F (m : nat) : pType :=
   match m with
   | 0%nat => F
   | (m'.+1)%nat => loops (F m')
   end) n ->*
(fix F (m : nat) : pType :=
   match m with
   | 0%nat => X
   | (m'.+1)%nat => loops (F m')
   end) n
F, X, Y: pType
i: F ->* X
f: X ->* Y
H: IsExact purely i f
n: +N
loops
  ((fix F (m : nat) : pType :=
      match m with
      | 0%nat => Y
      | (m'.+1)%nat => loops (F m')
      end) n) ->*
(fix F (m : nat) : pType :=
   match m with
   | 0%nat => F
   | (m'.+1)%nat => loops (F m')
   end) n
F, X, Y: pType
i: F ->* X
f: X ->* Y
H: IsExact purely i f
n: +N
IsExact purely ?Goal0 ?Goal
F, X, Y: pType
i: F ->* X
f: X ->* Y
H: IsExact purely i f
n: +N
IsExact purely ?Goal1 ?Goal0
F, X, Y: pType
i: F ->* X
f: X ->* Y
H: IsExact purely i f
n: +N
IsExact purely ?Goal@{n:=(n.+1)%nat} ?Goal1
  {
F, X, Y: pType
i: F ->* X
f: X ->* Y
H: IsExact purely i f
n: +N
(fix F (m : nat) : pType :=
   match m with
   | 0%nat => X
   | (m'.+1)%nat => loops (F m')
   end) n ->*
(fix F (m : nat) : pType :=
   match m with
   | 0%nat => Y
   | (m'.+1)%nat => loops (F m')
   end) n exact (fmap (iterated_loops n) f). }
F, X, Y: pType
i: F ->* X
f: X ->* Y
H: IsExact purely i f
n: +N
(fix F (m : nat) : pType :=
   match m with
   | 0%nat => F
   | (m'.+1)%nat => loops (F m')
   end) n ->*
(fix F (m : nat) : pType :=
   match m with
   | 0%nat => X
   | (m'.+1)%nat => loops (F m')
   end) n
F, X, Y: pType
i: F ->* X
f: X ->* Y
H: IsExact purely i f
n: +N
loops
  ((fix F (m : nat) : pType :=
      match m with
      | 0%nat => Y
      | (m'.+1)%nat => loops (F m')
      end) n) ->*
(fix F (m : nat) : pType :=
   match m with
   | 0%nat => F
   | (m'.+1)%nat => loops (F m')
   end) n
F, X, Y: pType
i: F ->* X
f: X ->* Y
H: IsExact purely i f
n: +N
IsExact purely ?Goal (fmap (iterated_loops n) f)
F, X, Y: pType
i: F ->* X
f: X ->* Y
H: IsExact purely i f
n: +N
IsExact purely ?Goal0 ?Goal
F, X, Y: pType
i: F ->* X
f: X ->* Y
H: IsExact purely i f
n: +N
IsExact purely (fmap (iterated_loops n.+1) f) ?Goal0
  {
F, X, Y: pType
i: F ->* X
f: X ->* Y
H: IsExact purely i f
n: +N
(fix F (m : nat) : pType :=
   match m with
   | 0%nat => F
   | (m'.+1)%nat => loops (F m')
   end) n ->*
(fix F (m : nat) : pType :=
   match m with
   | 0%nat => X
   | (m'.+1)%nat => loops (F m')
   end) n exact (fmap (iterated_loops n) i). }
F, X, Y: pType
i: F ->* X
f: X ->* Y
H: IsExact purely i f
n: +N
loops
  ((fix F (m : nat) : pType :=
      match m with
      | 0%nat => Y
      | (m'.+1)%nat => loops (F m')
      end) n) ->*
(fix F (m : nat) : pType :=
   match m with
   | 0%nat => F
   | (m'.+1)%nat => loops (F m')
   end) n
F, X, Y: pType
i: F ->* X
f: X ->* Y
H: IsExact purely i f
n: +N
IsExact purely (fmap (iterated_loops n) i)
  (fmap (iterated_loops n) f)
F, X, Y: pType
i: F ->* X
f: X ->* Y
H: IsExact purely i f
n: +N
IsExact purely ?Goal (fmap (iterated_loops n) i)
F, X, Y: pType
i: F ->* X
f: X ->* Y
H: IsExact purely i f
n: +N
IsExact purely (fmap (iterated_loops n.+1) f) ?Goal
  {
F, X, Y: pType
i: F ->* X
f: X ->* Y
H: IsExact purely i f
n: +N
loops
  ((fix F (m : nat) : pType :=
      match m with
      | 0%nat => Y
      | (m'.+1)%nat => loops (F m')
      end) n) ->*
(fix F (m : nat) : pType :=
   match m with
   | 0%nat => F
   | (m'.+1)%nat => loops (F m')
   end) n exact (connecting_map (fmap (iterated_loops n) i)
                          (fmap (iterated_loops n) f)). }
F, X, Y: pType
i: F ->* X
f: X ->* Y
H: IsExact purely i f
n: +N
IsExact purely (fmap (iterated_loops n) i)
  (fmap (iterated_loops n) f)
F, X, Y: pType
i: F ->* X
f: X ->* Y
H: IsExact purely i f
n: +N
IsExact purely
  (connecting_map (fmap (iterated_loops n) i)
     (fmap (iterated_loops n) f))
  (fmap (iterated_loops n) i)
F, X, Y: pType
i: F ->* X
f: X ->* Y
H: IsExact purely i f
n: +N
IsExact purely (fmap (iterated_loops n.+1) f)
  (connecting_map (fmap (iterated_loops n) i)
     (fmap (iterated_loops n) f))
  all:exact _.
Defined.

(** And from that, a long exact sequence of homotopy groups (though for now it is just a sequence of pointed sets). *)
Definition Pi_les `{Univalence} {F X Y : pType}
  (i : F ->* X) (f : X ->* Y) `{IsExact purely F X Y i f}
  : LongExactSequence (Tr (-1)) (N3)
  := trunc_les (-1) (loops_les i f).

(** * Classifying fiber sequences *)

(** Fiber sequences correspond to pointed maps into the universe. *)
Definition classify_fiberseq `{Univalence} {Y F : pType@{u}}
  : (Y ->* [Type@{u}, F]) <~> { X : pType@{u} & FiberSeq F X Y }.
H: Univalence
Y, F: pType
(Y ->* [Type, F]) <~> {X : pType & FiberSeq F X Y}
Proof.
H: Univalence
Y, F: pType
(Y ->* [Type, F]) <~> {X : pType & FiberSeq F X Y}
  refine (_ oE _).
H: Univalence
Y, F: pType
?Goal <~> {X : pType & FiberSeq F X Y}
H: Univalence
Y, F: pType
(Y ->* [Type, F]) <~> ?Goal
  (** To apply [equiv_sigma_pfibration] we need to invert the equivalence on the fiber. *)
  {
H: Univalence
Y, F: pType
?Goal <~> {X : pType & FiberSeq F X Y} do 2 (rapply equiv_functor_sigma_id; intro).
H: Univalence
Y, F, a: pType
a0: a ->* Y
?Goal0 a0 <~> (F <~>* pfiber a0)
    apply equiv_pequiv_inverse. }
H: Univalence
Y, F: pType
(Y ->* [Type, F]) <~>
{a : pType & {a0 : a ->* Y & pfiber a0 <~>* F}}
  exact ((equiv_sigma_assoc _ _)^-1 oE equiv_sigma_pfibration).
Defined.