Library HoTT.Pointed.pFiber
From HoTT Require Import Basics Types.
From HoTT.WildCat Require Import Core Equiv.
Require Import HFiber.
Require Import Pointed.Core.
Require Import Pointed.pEquiv.
Require Import Pointed.Loops.
Local Open Scope pointed_scope.
From HoTT.WildCat Require Import Core Equiv.
Require Import HFiber.
Require Import Pointed.Core.
Require Import Pointed.pEquiv.
Require Import Pointed.Loops.
Local Open Scope pointed_scope.
Instance ispointed_fiber {A B : pType} (f : A ->* B) : IsPointed (hfiber f (point B))
:= (point A; point_eq f).
Definition pfiber {A B : pType} (f : A ->* B) : pType := [hfiber f (point B), _].
Definition pfib {A B : pType} (f : A ->* B) : pfiber f ->* A
:= Build_pMap pr1 1.
Definition pfiber_fmap_loops {A B : pType} (f : A ->* B)
: pfiber (fmap loops f) <~>* loops (pfiber f).
Proof.
srapply Build_pEquiv'.
{ etransitivity.
2: srapply equiv_path_sigma.
simpl; unfold hfiber.
srapply equiv_functor_sigma_id.
intro p; cbn.
refine (_ oE equiv_moveL_Mp _ _ _).
refine (_ oE equiv_concat_r (concat_p1 _) _).
refine (_ oE equiv_moveL_Vp _ _ _).
refine (_ oE equiv_path_inverse _ _).
apply equiv_concat_l.
apply transport_paths_Fl. }
by pointed_reduce.
Defined.
Definition pr1_pfiber_fmap_loops {A B} (f : A ->* B)
: fmap loops (pfib f) o× pfiber_fmap_loops f
==* pfib (fmap loops f).
Proof.
srapply Build_pHomotopy.
- intros [u v].
refine (concat_1p _ @ concat_p1 _ @ _).
exact (@ap_pr1_path_sigma _ _ (point A; point_eq f) (point A; point_eq f) _ _).
- abstract (pointed_reduce_rewrite; reflexivity).
Defined.
Definition pfiber_fmap_iterated_loops {A B : pType} (n : nat) (f : A ->* B)
: pfiber (fmap (iterated_loops n) f) <~>* iterated_loops n (pfiber f).
Proof.
induction n.
1: reflexivity.
refine (_ o×E pfiber_fmap_loops _ ).
tapply (emap loops).
exact IHn.
Defined.
Definition functor_pfiber {A B C D}
{f : A ->* B} {g : C ->* D} {h : A ->* C} {k : B ->* D}
(p : k o× f ==* g o× h)
: pfiber f ->* pfiber g.
Proof.
srapply Build_pMap.
+ cbn. exact (functor_hfiber2 p (point_eq k)).
A shorter proof of this component via path_hfiber is possible, but this path_sigma' form compiles faster.
+ snapply path_sigma'.
- exact (point_eq h).
- lhs napply transport_paths_Fl.
lhs napply (whiskerL _ (concat_pp_p _ _ _)).
lhs napply (whiskerL _ (whiskerL _ (point_htpy p)^)).
lhs napply (whiskerL _ (concat_V_pp _ _)).
napply concat_V_pp.
Defined.
Definition pequiv_pfiber {A B C D}
{f : A ->* B} {g : C ->* D} (h : A <~>* C) (k : B <~>* D)
(p : k o× f ==* g o× h)
: pfiber f $<~> pfiber g
:= Build_pEquiv (functor_pfiber p) _.
Definition square_functor_pfiber {A B C D}
{f : A ->* B} {g : C ->* D} {h : A ->* C} {k : B ->* D}
(p : k o× f ==* g o× h)
: h o× pfib f ==* pfib g o× functor_pfiber p.
Proof.
srapply Build_pHomotopy.
- intros x; reflexivity.
- apply moveL_pV. cbn.
refine (1 @@ (concat_p1 _ @ _)).
exact (ap_pr1_path_sigma
(u := functor_hfiber2 p (point_eq k) (ispointed_fiber f))
(v := ispointed_fiber g) (point_eq h) _).
Defined.
Definition square_pequiv_pfiber {A B C D}
{f : A ->* B} {g : C ->* D} (h : A <~>* C) (k : B <~>* D)
(p : k o× f ==* g o× h)
: h o× pfib f ==* pfib g o× pequiv_pfiber h k p
:= square_functor_pfiber p.
- exact (point_eq h).
- lhs napply transport_paths_Fl.
lhs napply (whiskerL _ (concat_pp_p _ _ _)).
lhs napply (whiskerL _ (whiskerL _ (point_htpy p)^)).
lhs napply (whiskerL _ (concat_V_pp _ _)).
napply concat_V_pp.
Defined.
Definition pequiv_pfiber {A B C D}
{f : A ->* B} {g : C ->* D} (h : A <~>* C) (k : B <~>* D)
(p : k o× f ==* g o× h)
: pfiber f $<~> pfiber g
:= Build_pEquiv (functor_pfiber p) _.
Definition square_functor_pfiber {A B C D}
{f : A ->* B} {g : C ->* D} {h : A ->* C} {k : B ->* D}
(p : k o× f ==* g o× h)
: h o× pfib f ==* pfib g o× functor_pfiber p.
Proof.
srapply Build_pHomotopy.
- intros x; reflexivity.
- apply moveL_pV. cbn.
refine (1 @@ (concat_p1 _ @ _)).
exact (ap_pr1_path_sigma
(u := functor_hfiber2 p (point_eq k) (ispointed_fiber f))
(v := ispointed_fiber g) (point_eq h) _).
Defined.
Definition square_pequiv_pfiber {A B C D}
{f : A ->* B} {g : C ->* D} (h : A <~>* C) (k : B <~>* D)
(p : k o× f ==* g o× h)
: h o× pfib f ==* pfib g o× pequiv_pfiber h k p
:= square_functor_pfiber p.
The double fiber object is equivalent to loops on the base.
Definition pfiber2_loops {A B : pType} (f : A ->* B)
: pfiber (pfib f) <~>* loops B.
Proof.
pointed_reduce_pmap f.
snapply Build_pEquiv'.
1: make_equiv_contr_basedpaths.
reflexivity.
Defined.
: pfiber (pfib f) <~>* loops B.
Proof.
pointed_reduce_pmap f.
snapply Build_pEquiv'.
1: make_equiv_contr_basedpaths.
reflexivity.
Defined.
The value of pfiber2_loops on a general element of the double fiber.
Definition pfiber2_loops_beta {A B : pType} (f : A ->* B)
(a : A) (w : f a = pt) (v : a = pt)
: pfiber2_loops f ((a; w); v) = (point_eq f)^ @ (ap f v)^ @ w.
Proof.
pointed_reduce_pmap f.
destruct v; cbn.
exact (concat_1p w)^.
Defined.
(a : A) (w : f a = pt) (v : a = pt)
: pfiber2_loops f ((a; w); v) = (point_eq f)^ @ (ap f v)^ @ w.
Proof.
pointed_reduce_pmap f.
destruct v; cbn.
exact (concat_1p w)^.
Defined.
The triple-fiber functor is equal to the negative of the loop space functor.
Definition pfiber2_fmap_loops {A B : pType} (f : A ->* B)
: pfiber2_loops f o× pfib (pfib (pfib f))
==* fmap loops f o× (loops_inv _ o× pfiber2_loops (pfib f)).
Proof.
pointed_reduce.
simple refine (Build_pHomotopy _ _).
- intros [[[x p] q] r]. simpl in ×.
(* Apparently destruct q isn't smart enough to generalize over p. *)
move q before x; revert dependent x;
refine (paths_ind_r _ _ _); intros p r; cbn.
rewrite !concat_1p, concat_p1.
rewrite paths_ind_r_transport.
rewrite transport_arrow_toconst, transport_paths_Fl.
rewrite concat_p1, inv_V, ap_V.
refine (((r^)..2)^ @ _).
rewrite transport_paths_Fl; cbn.
rewrite pr1_path_V, !ap_V, !inv_V.
apply concat_p1.
- reflexivity.
Qed.
: pfiber2_loops f o× pfib (pfib (pfib f))
==* fmap loops f o× (loops_inv _ o× pfiber2_loops (pfib f)).
Proof.
pointed_reduce.
simple refine (Build_pHomotopy _ _).
- intros [[[x p] q] r]. simpl in ×.
(* Apparently destruct q isn't smart enough to generalize over p. *)
move q before x; revert dependent x;
refine (paths_ind_r _ _ _); intros p r; cbn.
rewrite !concat_1p, concat_p1.
rewrite paths_ind_r_transport.
rewrite transport_arrow_toconst, transport_paths_Fl.
rewrite concat_p1, inv_V, ap_V.
refine (((r^)..2)^ @ _).
rewrite transport_paths_Fl; cbn.
rewrite pr1_path_V, !ap_V, !inv_V.
apply concat_p1.
- reflexivity.
Qed.
The path algebra underlying the pointwise part of pfiber2_loops_natural_functor, with all endpoints free.
Local Definition pfiber2_loops_natural_functor_helper {D : Type} {x y z : D}
(p : x = y) (q : y = z)
: (p^ @ 1) @ (((1 @ (1 @ p)^)^ @ q) @ 1) = 1 @ (q @ 1).
Proof.
by destruct p, q.
Defined.
(p : x = y) (q : y = z)
: (p^ @ 1) @ (((1 @ (1 @ p)^)^ @ q) @ 1) = 1 @ (q @ 1).
Proof.
by destruct p, q.
Defined.
pfiber2_loops commutes with the fiber functor of a square, for an arbitrary square of pointed maps. TODO: The second half of this proof and the Defined line are a bit slow.
Definition pfiber2_loops_natural_functor {A B C D : pType}
{f : A ->* B} {g : C ->* D} {h : A ->* C} {k : B ->* D}
(p : k o× f ==* g o× h)
: pfiber2_loops g o× functor_pfiber (square_functor_pfiber p)
==* fmap loops k o× pfiber2_loops f.
Proof.
pointed_reduce.
cbn in H.
snapply Build_pHomotopy.
- intros [[c w] v].
cbn in c, w, v.
destruct v.
lhs napply pfiber2_loops_beta.
cbn.
destruct H^; clear H p.
exact (pfiber2_loops_natural_functor_helper dpoint_eq1 (ap k w)).
- cbn; cbv delta
[point_htpy square_functor_pfiber
functor_hfiber2 functor_sigma
functor_pfiber];
cbn.
(* The next two lines are essentially destruct H^, with H also replaced by idpath. *)
generalize dependent (p point2).
napply paths_ind_r.
destruct dpoint_eq1.
reflexivity.
Defined.
{f : A ->* B} {g : C ->* D} {h : A ->* C} {k : B ->* D}
(p : k o× f ==* g o× h)
: pfiber2_loops g o× functor_pfiber (square_functor_pfiber p)
==* fmap loops k o× pfiber2_loops f.
Proof.
pointed_reduce.
cbn in H.
snapply Build_pHomotopy.
- intros [[c w] v].
cbn in c, w, v.
destruct v.
lhs napply pfiber2_loops_beta.
cbn.
destruct H^; clear H p.
exact (pfiber2_loops_natural_functor_helper dpoint_eq1 (ap k w)).
- cbn; cbv delta
[point_htpy square_functor_pfiber
functor_hfiber2 functor_sigma
functor_pfiber];
cbn.
(* The next two lines are essentially destruct H^, with H also replaced by idpath. *)
generalize dependent (p point2).
napply paths_ind_r.
destruct dpoint_eq1.
reflexivity.
Defined.
The same for an equivalence square; the underlying double-fiber map is functor_pfiber of the same square.