From HoTT Require Import Basics Types.From HoTT Require Import Basics Types.
Require Import SuccessorStructure.
From HoTT.WildCat Require Import Core PointedCat Square Equiv.
From HoTT.Pointed Require Import Core pMap pEquiv pFiber pTrunc Loops.
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
?f 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
  tapply (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
  tapply (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]. *)
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)
}.

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]. *)
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
  exact (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
  snapply 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. *)
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: exact 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.

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.

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]. *)
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)
    tapply (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.

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. *)
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)
  napply 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:napply (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. *)
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
  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).

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
?f 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.

(** 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 F0 (m : nat) : pType :=
   match m with
   | 0%nat => X
   | m'.+1%nat => loops (F0 m')
   end)
  n ->*
(fix F0 (m : nat) : pType :=
   match m with
   | 0%nat => Y
   | m'.+1%nat => loops (F0 m')
   end)
  n
F, X, Y: pType
i: F ->* X
f: X ->* Y
H: IsExact purely i f
n: +N
(fix F0 (m : nat) : pType :=
   match m with
   | 0%nat => F
   | m'.+1%nat => loops (F0 m')
   end)
  n ->*
(fix F0 (m : nat) : pType :=
   match m with
   | 0%nat => X
   | m'.+1%nat => loops (F0 m')
   end)
  n
F, X, Y: pType
i: F ->* X
f: X ->* Y
H: IsExact purely i f
n: +N
loops
  ((fix F0 (m : nat) : pType :=
      match m with
      | 0%nat => Y
      | m'.+1%nat => loops (F0 m')
      end)
     n) ->*
(fix F0 (m : nat) : pType :=
   match m with
   | 0%nat => F
   | m'.+1%nat => loops (F0 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 F0 (m : nat) : pType :=
   match m with
   | 0%nat => X
   | m'.+1%nat => loops (F0 m')
   end)
  n ->*
(fix F0 (m : nat) : pType :=
   match m with
   | 0%nat => Y
   | m'.+1%nat => loops (F0 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 F0 (m : nat) : pType :=
   match m with
   | 0%nat => F
   | m'.+1%nat => loops (F0 m')
   end)
  n ->*
(fix F0 (m : nat) : pType :=
   match m with
   | 0%nat => X
   | m'.+1%nat => loops (F0 m')
   end)
  n
F, X, Y: pType
i: F ->* X
f: X ->* Y
H: IsExact purely i f
n: +N
loops
  ((fix F0 (m : nat) : pType :=
      match m with
      | 0%nat => Y
      | m'.+1%nat => loops (F0 m')
      end)
     n) ->*
(fix F0 (m : nat) : pType :=
   match m with
   | 0%nat => F
   | m'.+1%nat => loops (F0 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 F0 (m : nat) : pType :=
   match m with
   | 0%nat => F
   | m'.+1%nat => loops (F0 m')
   end)
  n ->*
(fix F0 (m : nat) : pType :=
   match m with
   | 0%nat => X
   | m'.+1%nat => loops (F0 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 F0 (m : nat) : pType :=
      match m with
      | 0%nat => Y
      | m'.+1%nat => loops (F0 m')
      end)
     n) ->*
(fix F0 (m : nat) : pType :=
   match m with
   | 0%nat => F
   | m'.+1%nat => loops (F0 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 F0 (m : nat) : pType :=
      match m with
      | 0%nat => Y
      | m'.+1%nat => loops (F0 m')
      end)
     n) ->*
(fix F0 (m : nat) : pType :=
   match m with
   | 0%nat => F
   | m'.+1%nat => loops (F0 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)
    exact 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.