Timings for ExactSequence.v
From HoTT Require Import Basics Types.
Require Import SuccessorStructure.
Require Import Spaces.Finite.Tactics.
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 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.
exact (fun x => (i x; cx x)).
refine (path_sigma' _ (point_eq i) _); cbn.
refine (transport_paths_Fl _ _ @ _).
exact ((concat_p1 _)^ @ point_htpy cx).
(** ...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.
rewrite ap_pr1_path_sigma; hott_simpl.
(** 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).
refine ((fmap_comp (pTr n) i f)^* @* _).
refine (_ @* ptr_functor_pconst n).
tapply (fmap2 (pTr _)); assumption.
(** 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).
refine ((fmap_comp loops i f)^$ $@ _ $@ fmap_zero_morphism _).
tapply (fmap2 loops); assumption.
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).
induction n as [|n IHn]; [ exact cx | ].
apply iscomplex_loops; assumption.
(** 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.
refine (_ @* precompose_pconst e^-1*).
refine ((compose_V_hh e (f o* i))^$ $@ _).
refine (cat_postwhisker e^-1* _).
refine ((cat_assoc _ _ _)^$ $@ _).
(** 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).
refine (pmap_compose_assoc _ _ _ @* _).
refine (pmap_postwhisker f p @* _).
refine ((pmap_compose_assoc _ _ _)^* @* _).
refine (pmap_prewhisker g cx @* _).
apply postcompose_pconst.
(** 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.
refine ((pmap_compose_assoc _ _ _)^* @* _).
refine (pmap_prewhisker _ cx @* _).
apply postcompose_pconst.
(** Any pointed map induces a trivial complex. *)
Definition iscomplex_trivial {X Y : pType} (f : X ->* Y)
: IsComplex (@pconst pUnit X) f.
exact (concat_p1 _ @ concat_1p _).
(** 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).
rapply (transport (fun A => IsHProp A) (x := { cx : IsComplex i f & IsConnMap n (cxfib cx) })).
apply path_universe_uncurried; issig.
(** 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).
rapply (O_functor O (A:=hfiber (cxfib cx_isexact) (x; p))).
apply center, conn_map_isexact.
(** 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).
srapply isexact_preimage; exact x.2.
(** If the base is contractible, then [i] is [O]-connected. When [O] is [Tr (-1)], this says that [i] is a surjection. *)
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.
exists (iscomplex_homotopic_i ii f cx_isexact).
refine (conn_map_homotopic n (cxfib cx_isexact) _ _ _).
refine (path_sigma' _ (ii u)^ _).
exact (transport_paths_Fl _ _ @ ((inverse2 (ap_V _ _) @ inv_V _) @@ 1)).
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'.
exists (iscomplex_homotopic_f i ff cx_isexact).
pose (e := equiv_hfiber_homotopic _ _ ff pt).
nrefine (cancelL_isequiv_conn_map n _ e).
refine (conn_map_homotopic n (cxfib (cx_isexact)) _ _ _).
exact (concat_1p _ @ concat_V_pp _ _)^.
(** 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).
exists (iscomplex_equiv_i i i' g h p f cx_isexact); cbn.
snrefine (cancelL_equiv_conn_map n (C := pfiber f) _ _).
exact (@equiv_functor_hfiber _ _ _ _ (f o h) f h equiv_idmap
(fun x => 1%path) (point Y)).
cbn; unfold functor_hfiber, functor_sigma; cbn.
refine (conn_map_homotopic n (@cxfib _ _ _ i f cx_isexact o g) _ _ _).
refine (path_sigma' _ (p u)^ _).
abstract (
rewrite transport_paths_Fl, ap_V, inv_V,
!concat_1p, concat_p1, ap_idmap;
reflexivity
).
(** 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).
rapply (isexact_equiv_i _ _ _ pequiv_pmap_idmap phi); cbn.
exact (pmap_precompose_idmap _)^*.
(** 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.
1: apply iscomplex_equiv_fiber, cx_isexact.
apply (conn_map_homotopic _ (cxfib cx_isexact o* phi)).
by rewrite concat_p1, concat_1p.
(** 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'.
pose (I := isexact_equiv_i n i i' g h p f).
pose (I2 := isexact_homotopic_f n i' q).
exists (iscomplex_cancelL i' f' k cx_isexact).
epose (e := (pequiv_pfiber pequiv_pmap_idmap k (pmap_precompose_idmap (k o* f'))^*
: pfiber f' <~>* pfiber (k o* f'))).
nrefine (cancelL_isequiv_conn_map n _ e).
1: apply pointed_isequiv.
refine (conn_map_homotopic n (cxfib (cx_isexact)) _ _ _).
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.
(** 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).
rapply isequiv_conn_ino_map.
rapply (cancelL_mapinO _ _ pr1).
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 _.
1: exact (isequiv_cxfib ex).
exact (ap (fun g => i g) (eissect _ x)).
(** 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.
(** 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.
exact (concat_p1 _ @ concat_1p _)^.
Instance isexact_pfib {X Y} (f : X ->* Y)
: IsExact purely (pfib f) f.
exists (iscomplex_pfib f).
(** When applied to the standard fiber, [cxfib] is the identity map. *)
Definition cxfib_pfib {X Y : pType} (f : X ->* Y)
: cxfib (iscomplex_pfib f) ==* pmap_idmap.
(** 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.
srapply Build_IsExact; [ srapply Build_pHomotopy | ].
refine (concat_p1 _ @ _).
refine (_ @ (point_eq fs.2)..2).
refine (_ @ (transport_paths_Fl _ _)^).
apply whiskerR, inverse2, ap, concat_p1.
change (IsEquiv fs.2); exact _.
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).
(** 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*.
(** 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).
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 _ _).
symmetry; apply pfib_cxfib.
refine (_ @* pmap_compose_assoc _ _ _).
refine (pmap_prewhisker (fmap loops (cxfib cx_isexact)) _).
apply pr1_pfiber_fmap_loops.
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).
induction n as [|n IHn]; [ assumption | apply isexact_loops; assumption ].
(** (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).
exists (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.
napply conn_map_homotopic.
2:napply (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 _)^).
(** 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).
intros z; apply isconnected_contr.
exact (conn_map_isexact (f := f) (i := i) z).
(** ** 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.
refine (pmap_postcompose_idmap _ @* _).
symmetry; apply pfib_cxfib.
(** 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.
exact (((pfiber2_loops f) o*E (pequiv_pfiber _ _ (square_pfib_pequiv_cxfib i f)))^-1*).
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).
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).
(** The connecting map associated to a pointed family. *)
Definition connecting_map_family {Y : pType} (P : pFam Y)
: loops Y ->* [P pt, dpoint P].
(** ** Naturality and rotation of the connecting map *)
(** The fiber functor of the tautological [cxfib] square is the identity. This should also follow from the fact that [pequiv_cxfib] is homotopic to [pmap_idmap] ([cxfib_pfib]). *)
Definition pequiv_pfiber_cxfib_taut {X Y : pType} (f : X ->* Y)
: pequiv_pfiber pequiv_cxfib pequiv_pmap_idmap
(square_pfib_pequiv_cxfib (pfib f) f)
==* pmap_idmap.
exact (concat_p1 _ @ concat_1p _ @ ap_idmap v).
(** TODO: The next two results are proved for the tautological fiber sequence. It would be nice to extend them to any [FiberSeq] or equivalently any purely-exact sequence. *)
(** The connecting map of the tautological fiber sequence is natural in arbitrary squares of pointed maps. *)
Definition connecting_map_natural_functor {X Y X' Y' : pType}
{f : X ->* Y} {f' : X' ->* Y'} {h : X' ->* X} {k : Y' ->* Y}
(q : k o* f' ==* f o* h)
: functor_pfiber q o* connecting_map (pfib f') f'
==* connecting_map (pfib f) f o* fmap loops k.
unfold connecting_map, i_fiberseq, connect_fiberseq, ".1", ".2".
lhs_V' napply pmap_compose_assoc.
lhs' napply (pmap_prewhisker _
(square_functor_pfiber (square_functor_pfiber q))).
lhs' napply pmap_compose_assoc.
rhs' napply pmap_compose_assoc.
lhs_V' napply pmap_compose_assoc.
lhs' napply (pmap_prewhisker _
(pmap_postwhisker _ (pequiv_pfiber_cxfib_taut f)
@* pmap_precompose_idmap _)).
rhs' napply (pmap_postwhisker _
(pmap_postwhisker _ (pequiv_pfiber_cxfib_taut f')
@* pmap_precompose_idmap _)).
exact (pfiber2_loops_natural_functor q).
(** The same for an equivalence square. *)
Definition connecting_map_natural {X Y X' Y' : pType}
{f : X ->* Y} {f' : X' ->* Y'} (h : X' <~>* X) (k : Y' <~>* Y)
(q : k o* f' ==* f o* h)
: pequiv_pfiber h k q o* connecting_map (pfib f') f'
==* connecting_map (pfib f) f o* fmap loops k
:= connecting_map_natural_functor q.
(** Through [cxfib], the connecting map of an exact sequence agrees with the connecting map of the tautological fiber sequence. *)
Definition connecting_map_cxfib {F X Y : pType}
(i : F ->* X) (f : X ->* Y) `{IsExact purely F X Y i f}
: pequiv_cxfib o* connecting_map i f ==* connecting_map (pfib f) f.
unfold connecting_map, i_fiberseq, connect_fiberseq, ".1", ".2".
lhs_V' napply pmap_compose_assoc.
lhs' napply (pmap_prewhisker _
(square_pequiv_pfiber _ _ (square_pfib_pequiv_cxfib i f))).
lhs' napply pmap_compose_assoc.
lhs' napply pmap_compose_assoc.
lhs' napply (pmap_prewhisker _ (pequiv_pfiber_cxfib_taut f)).
napply pmap_postcompose_idmap.
(** Through [pfiber2_loops], the connecting map of the doubly-iterated tautological fiber sequence is loop inversion followed by [loops] of the map. *)
Definition connecting_map_pfib2 {F X : pType} (i : F ->* X)
: pfiber2_loops i o* connecting_map (pfib (pfib i)) (pfib i)
==* fmap loops i o* loops_inv F.
unfold connecting_map, i_fiberseq, connect_fiberseq, ".1", ".2".
lhs_V' napply pmap_compose_assoc.
lhs' napply (pfiber2_fmap_loops i).
rhs' napply pmap_compose_assoc.
napply (pmap_postwhisker _ (pequiv_pfiber_cxfib_taut (pfib i))
@* pmap_precompose_idmap _)^*.
(** Through [pfiber2_loops], the double fiber projection of an exact sequence is loop inversion followed by [loops] of the projection. *)
Definition pfiber2_loops_pfib2 {F X Y : pType}
(i : F ->* X) (f : X ->* Y) `{IsExact purely F X Y i f}
: pfiber2_loops f
o* pequiv_pfiber _ _ (square_pfib_pequiv_cxfib i f)
o* pfib (pfib i)
==* fmap loops f o* (loops_inv X o* pfiber2_loops i).
lhs' napply pmap_compose_assoc.
lhs' napply (pmap_postwhisker _
(square_pequiv_pfiber _ _
(square_pequiv_pfiber _ _
(square_pfib_pequiv_cxfib i f)))).
lhs_V' napply pmap_compose_assoc.
lhs' napply (pmap_prewhisker _ (pfiber2_fmap_loops f)).
lhs' napply pmap_compose_assoc.
lhs' napply (pmap_postwhisker _ (pmap_compose_assoc _ _ _)).
lhs' napply (pmap_postwhisker _ (pmap_postwhisker _
(pfiber2_loops_natural pequiv_cxfib pequiv_pmap_idmap
(square_pfib_pequiv_cxfib i f)))).
lhs' refine (pmap_prewhisker _ (fmap_id loops X)).
napply pmap_postcompose_idmap.
(** ** 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)) _.
(** A long exact sequence can be replaced by an objectwise pointed equivalent one, provided we are given maps [g] making the squares commute. *)
Definition les_pequiv {O : Modality} {N : SuccStr} (S : LongExactSequence O N)
(C : N -> pType) (e : forall n, C n <~>* S n)
(g : forall n, C n.+1 ->* C n)
(p : forall n, e n o* g n ==* les_fn S n o* e n.+1)
: LongExactSequence O N
:= Build_LongExactSequence O N C g
(fun n => isexact_square_if O (e n.+1.+1) (e n.+1) (e n) (p n.+1) (p 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.
srefine (Build_LongExactSequence purely N3 (loops_carrier F X Y) _ _).
all: intros [n x]; FinIndOn x; 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)).
(** And from that, a long exact sequence of homotopy groups, expressed as a sequence of pointed sets. In [Homotopy.HomotopyGroup] this is converted into the equivalent sequence [Pi_les], whose maps are expressed using [fmap (pPi n)]. *)
Definition Pi_les_pset `{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 }.
(** To apply [equiv_sigma_pfibration] we need to invert the equivalence on the fiber. *)
do 2 (rapply equiv_functor_sigma_id; intro).
exact equiv_pequiv_inverse.
exact ((equiv_sigma_assoc _ _)^-1 oE equiv_sigma_pfibration).