Library HoTT.Homotopy.ExactSequence

Require Import Basics Types.
Require Import SuccessorStructure.
Require Import WildCat.
Require Import Pointed.
Require Import Modalities.Identity Modalities.Descent.
Require Import Truncations.
Require Import HFiber.
Require Import ObjectClassifier.

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.
Proof.
  srapply Build_pMap.
  - exact (fun x ⇒ (i x ; cx x )).
  - cbn. refine (path_sigma' _ (point_eq i) _); cbn.
    refine (transport_paths_Fl _ _ @ _).
    apply moveR_Vp.
    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.
Proof.
  srapply Build_pHomotopy.
  - reflexivity.
  - cbn. 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).
Proof.
  refine ((fmap_comp (pTr n) i f)^* @* _).
  refine (_ @* ptr_functor_pconst n).
  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).
Proof.
  refine ((fmap_comp loops i f)^$ $@ _ $@ fmap_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).
Proof.
  induction n as [|n IHn]; [ exact cx | ].
  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.
Proof.
  refine (_ @* precompose_pconst e^-1*).
  refine ((compose_V_hh e (f o × i))^$ $@ _).
  refine (cat_postwhisker e^-1* _).
  refine ((cat_assoc _ _ _)^$ $@ _).
  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).
Proof.
  refine (pmap_compose_assoc _ _ _ @* _).
  refine (pmap_postwhisker f p @* _).
  refine ((pmap_compose_assoc _ _ _)^* @* _).
  refine (pmap_prewhisker g cx @* _).
  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.
Proof.
  refine ((pmap_compose_assoc _ _ _)^* @* _).
  refine (pmap_prewhisker _ cx @* _).
  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.
Proof.
  srapply Build_pHomotopy.
  - intro x; cbn.
    exact (point_eq f).
  - cbn; symmetry.
    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).
Proof.
  rapply (transport (fun A ⇒ IsHProp A) (x := { cx : IsComplex i f & IsConnMap n (cxfib cx) })).
  2: exact _.
  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).
Proof.
  rapply (O_functor O (A:=hfiber (cxfib cx_isexact) (x; p))).
  - intros [z q].
    exact (z; ap pr1 q).
  - 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).
Proof.
  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.
Proof.
  ∃ (iscomplex_homotopic_i ii f cx_isexact).
  refine (conn_map_homotopic n (cxfib cx_isexact) _ _ _).
  intros u; cbn.
  refine (path_sigma' _ (ii 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'.
Proof.
  ∃ (iscomplex_homotopic_f i ff cx_isexact).
  pose (e := equiv_hfiber_homotopic _ _ ff pt).
  nrefine (cancelL_isequiv_conn_map n _ e).
  1: apply equiv_isequiv.
  refine (conn_map_homotopic n (cxfib (cx_isexact)) _ _ _).
  intro u. simpl. srapply path_hfiber.
  1: reflexivity.
  refine (concat_1p _ @ concat_V_pp _ _)^.
Defined.

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

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

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}
  `{∀ y y' : Y , In O (y = y')} `{MapIn O _ _ i} (ex : IsExact O i f)
  : IsEquiv (cxfib cx_isexact).
Proof.
  rapply isequiv_conn_ino_map.
  1: apply ex.
  rapply (cancelL_mapinO _ _ pr1).
Defined.

Definition equiv_cxfib {O : Modality} {F X Y : pType} {i : F ->* X} {f : X ->* Y}
  `{∀ 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}
  `{∀ y y' : Y , In O (y = y')} `{MapIn O _ _ i} (ex : IsExact O i f)
  : i o pequiv_inverse (equiv_cxfib ex) == pfib _.
Proof.
  rapply equiv_ind.
  1: exact (isequiv_cxfib ex).
  intro 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.
Proof.
  srapply Build_IsExact.
  1: apply 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.
Proof.
  srapply Build_pHomotopy.
  - intros [x p]; exact p.
  - cbn. exact (concat_p1 _ @ concat_1p _)^.
Defined.

Global Instance isexact_pfib {X Y} (f : X ->* Y)
  : IsExact purely (pfib f) f.
Proof.
  ∃ (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.
Proof.
  srapply Build_IsExact; [ srapply Build_pHomotopy | ].
  - intros u; cbn.
    exact ((fs.2 u ).2).
  - apply moveL_pV. cbn.
    refine (concat_p1 _ @ _).
    apply moveL_Mp.
    refine (_ @ (point_eq fs.2 )..2).
    refine (_ @ (transport_paths_Fl _ _)^).
    apply whiskerR, inverse2, ap, concat_p1.
  - intros [x p].
    apply contr_map_isequiv.
    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).
Proof.

TODO: doesn't work?!

(*   exists (fmap loops fs.1). *)
  refine (fmap loops fs.1 ; _).
  refine (_ o ×E emap loops fs.2).
  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).
Proof.
  refine (@isexact_homotopic_i purely _ _ _ _ (fmap loops i) _ (fmap loops f)
    (isexact_purely_fiberseq (fiberseq_loops (fiberseq_isexact_purely i f)))).
  transitivity (fmap loops (pfib f) o × fmap loops (cxfib cx_isexact)).
  - refine (_ @* fmap_comp loops _ _).
    rapply (fmap2 loops).
    symmetry; apply pfib_cxfib.
  - refine (_ @* pmap_compose_assoc _ _ _).
    refine (pmap_prewhisker (fmap loops (cxfib cx_isexact)) _).
    apply moveR_pequiv_fV.
    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).
Proof.
  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).
Proof.
  ∃ (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) _)).
  { intros x; rapply isconnected_pred. }
  nrapply conn_map_homotopic.
  2:nrapply (conn_map_compose _ (cxfib _)
               (functor_hfiber (fun y ⇒ (to_O_natural (Tr n.+1) f y )^)
                               (point Y))).
  3:pose @O_lex_leq_Tr; rapply (OO_conn_map_functor_hfiber_to_O).
  - intros x; refine (path_sigma' _ 1 _); cbn.
    (* 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 _)^).
  - 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).
Proof.
  rapply isexact_ptr.
  ∃ cx_isexact.
  intros z; apply isconnected_contr.
  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.
Proof.
  unfold Square.
  refine (pmap_postcompose_idmap _ @* _).
  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.
Proof.
  ∃ 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).
Proof.
  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)).
  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))) _).
  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)) _ _).
  - exact (square_pequiv_pfiber _ _ (square_pequiv_pfiber _ _ (square_pfib_pequiv_cxfib i 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 ].
Proof.
  srapply Build_pMap.
  - intro l.
    apply (transport P l).
    apply P.
  - reflexivity.
Defined.

Long exact sequences

Record LongExactSequence (k : Modality) (N : SuccStr) : Type :=
{
  les_carrier : N → pType;
  les_fn : ∀ n , les_carrier n .+1 ->* les_carrier n;
  les_isexact : ∀ 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).
Proof.
  srefine (Build_LongExactSequence purely (N3) (loops_carrier F X Y) _ _).
  all:intros [n [[[[]|[]]|[]]|[]]]; cbn.
  { exact (fmap (iterated_loops n) f). }
  { exact (fmap (iterated_loops n) i). }
  { exact (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 }.
Proof.
refine (_ oE _).

To apply equiv_sigma_pfibration we need to invert the equivalence on the fiber.

  { do 2 (rapply equiv_functor_sigma_id; intro).
    apply equiv_pequiv_inverse. }
  exact ((equiv_sigma_assoc _ _)^-1 oE equiv_sigma_pfibration).
Defined.