Require Import Basics Types Pointed.Core Pointed.pEquiv.
[Loading ML file number_string_notation_plugin.cmxs (using legacy method) ... done]

(** * Pointed sections of pointed maps *)

Local Open Scope pointed_scope.

(* The type of pointed sections of a pointed map. *)
Definition pSect {A B : pType} (f : A ->* B)
  := { s : B ->* A & f o* s ==* pmap_idmap }.

Definition issig_psect { A B : pType } (f : A ->* B)
  : { s : B -> A & { p : s pt = pt
                        & { H : f o s == idmap
                                & H pt = ap f p @ (point_eq f) } } }
  <~> pSect f.
A, B: pType
f: A ->* B
{s : B -> A &
{p : s pt = pt &
{H : f o s == idmap & H pt = ap f p @ point_eq f}}} <~>
pSect f
Proof.
A, B: pType
f: A ->* B
{s : B -> A &
{p : s pt = pt &
{H : f o s == idmap & H pt = ap f p @ point_eq f}}} <~>
pSect f
  transitivity
    {s : B -> A & {p : s pt = pt
                      & {H : f o s == idmap
                             & H pt = ap f p @ (point_eq f) @ 1 }}}.
A, B: pType
f: A ->* B
{s : B -> A &
{p : s pt = pt &
{H : f o s == idmap & H pt = ap f p @ point_eq f}}} <~>
{s : B -> A &
{p : s pt = pt &
{H : f o s == idmap &
H pt = (ap f p @ point_eq f) @ 1}}}
A, B: pType
f: A ->* B
{s : B -> A &
{p : s pt = pt &
{H : f o s == idmap &
H pt = (ap f p @ point_eq f) @ 1}}} <~> pSect f
  2: make_equiv.
A, B: pType
f: A ->* B
{s : B -> A &
{p : s pt = pt &
{H : f o s == idmap & H pt = ap f p @ point_eq f}}} <~>
{s : B -> A &
{p : s pt = pt &
{H : f o s == idmap &
H pt = (ap f p @ point_eq f) @ 1}}}
  do 3 (napply equiv_functor_sigma_id; intro).
A, B: pType
f: A ->* B
a: B -> A
a0: a pt = pt
a1: (fun x : B => f (a x)) == idmap
a1 pt = ap f a0 @ point_eq f <~>
a1 pt = (ap f a0 @ point_eq f) @ 1
  rapply equiv_concat_r.
A, B: pType
f: A ->* B
a: B -> A
a0: a pt = pt
a1: (fun x : B => f (a x)) == idmap
ap f a0 @ point_eq f = (ap f a0 @ point_eq f) @ 1
  exact (concat_p1 _)^.
Defined.

(** Any pointed equivalence over [A] induces an equivalence between pointed sections. *)
Definition equiv_pequiv_pslice_psect `{Funext} {A B C : pType}
  (f : B ->* A) (g : C ->* A) (t : B <~>* C) (h : f ==* g o* t)
  : pSect f <~> pSect g.
H: Funext
A, B, C: pType
f: B ->* A
g: C ->* A
t: B <~>* C
h: f ==* g o* t
pSect f <~> pSect g
Proof.
H: Funext
A, B, C: pType
f: B ->* A
g: C ->* A
t: B <~>* C
h: f ==* g o* t
pSect f <~> pSect g
  srapply equiv_functor_sigma'.
H: Funext
A, B, C: pType
f: B ->* A
g: C ->* A
t: B <~>* C
h: f ==* g o* t
(A ->* B) <~> (A ->* C)
H: Funext
A, B, C: pType
f: B ->* A
g: C ->* A
t: B <~>* C
h: f ==* g o* t
forall a : A ->* B,
(fun s : A ->* B => f o* s ==* pmap_idmap) a <~>
(fun s : A ->* C => g o* s ==* pmap_idmap) (?f a)
  1: exact (pequiv_pequiv_postcompose t).
H: Funext
A, B, C: pType
f: B ->* A
g: C ->* A
t: B <~>* C
h: f ==* g o* t
forall a : A ->* B,
(fun s : A ->* B => f o* s ==* pmap_idmap) a <~>
(fun s : A ->* C => g o* s ==* pmap_idmap)
  (pequiv_pequiv_postcompose t a)
  intro s; cbn.
H: Funext
A, B, C: pType
f: B ->* A
g: C ->* A
t: B <~>* C
h: f ==* g o* t
s: A ->* B
f o* s ==* pmap_idmap <~> g o* (t o* s) ==* pmap_idmap
  apply equiv_phomotopy_concat_l.
H: Funext
A, B, C: pType
f: B ->* A
g: C ->* A
t: B <~>* C
h: f ==* g o* t
s: A ->* B
g o* (t o* s) ==* f o* s
  refine ((pmap_compose_assoc _ _ _)^* @* _).
H: Funext
A, B, C: pType
f: B ->* A
g: C ->* A
t: B <~>* C
h: f ==* g o* t
s: A ->* B
g o* t o* s ==* f o* s
  apply pmap_prewhisker.
H: Funext
A, B, C: pType
f: B ->* A
g: C ->* A
t: B <~>* C
h: f ==* g o* t
s: A ->* B
g o* t ==* f
  exact h^*.
Defined.

(** Pointed sections of [psnd : A * B ->* B] correspond to pointed maps [B ->* A]. *)
Definition equiv_psect_psnd `{Funext} {A B : pType}
  : pSect (@psnd A B) <~> (B ->* A).
H: Funext
A, B: pType
pSect psnd <~> (B ->* A)
Proof.
H: Funext
A, B: pType
pSect psnd <~> (B ->* A)
  unfold pSect.
H: Funext
A, B: pType
{s : B ->* A * B & psnd o* s ==* pmap_idmap} <~>
(B ->* A)
  transitivity {s : (B ->* A) * (B ->* B) & snd s ==* pmap_idmap}.
H: Funext
A, B: pType
{s : B ->* A * B & psnd o* s ==* pmap_idmap} <~>
{s : (B ->* A) * (B ->* B) & snd s ==* pmap_idmap}
H: Funext
A, B: pType
{s : (B ->* A) * (B ->* B) & snd s ==* pmap_idmap} <~>
(B ->* A)
  {
H: Funext
A, B: pType
{s : B ->* A * B & psnd o* s ==* pmap_idmap} <~>
{s : (B ->* A) * (B ->* B) & snd s ==* pmap_idmap} snrefine (equiv_functor_sigma'
                (equiv_pprod_coind (pfam_const A) (pfam_const B))^-1%equiv _).
H: Funext
A, B: pType
forall
a : pForall B
      {|
        pfam_pr1 :=
          fun a : B =>
          (pfam_const A a * pfam_const B a)%type;
        dpoint :=
          (dpoint (pfam_const A),
          dpoint (pfam_const B))
      |},
(fun s : B ->* A * B => psnd o* s ==* pmap_idmap) a <~>
(fun s : (B ->* A) * (B ->* B) => snd s ==* pmap_idmap)
  ((equiv_pprod_coind (pfam_const A) (pfam_const B))^-1%equiv
     a)
    cbn.
H: Funext
A, B: pType
forall
a : pForall B
      {|
        pfam_pr1 := fun _ : B => (A * B)%type;
        dpoint := (pt, pt)
      |},
psnd o* a ==* pmap_idmap <~>
{|
  pointed_fun := fun x : B => snd (a x);
  dpoint_eq := ap snd (dpoint_eq a)
|} ==* pmap_idmap intro s.
H: Funext
A, B: pType
s: pForall B
  {|
    pfam_pr1 := fun _ : B => (A * B)%type;
    dpoint := (pt, pt)
  |}
psnd o* s ==* pmap_idmap <~>
{|
  pointed_fun := fun x : B => snd (s x);
  dpoint_eq := ap snd (dpoint_eq s)
|} ==* pmap_idmap
    apply equiv_phomotopy_concat_l.
H: Funext
A, B: pType
s: pForall B
  {|
    pfam_pr1 := fun _ : B => (A * B)%type;
    dpoint := (pt, pt)
  |}
{|
  pointed_fun := fun x : B => snd (s x);
  dpoint_eq := ap snd (dpoint_eq s)
|} ==* psnd o* s
    srapply Build_pHomotopy.
H: Funext
A, B: pType
s: pForall B
  {|
    pfam_pr1 := fun _ : B => (A * B)%type;
    dpoint := (pt, pt)
  |}
{|
  pointed_fun := fun x : B => snd (s x);
  dpoint_eq := ap snd (dpoint_eq s)
|} == psnd o* s
H: Funext
A, B: pType
s: pForall B
  {|
    pfam_pr1 := fun _ : B => (A * B)%type;
    dpoint := (pt, pt)
  |}
?p pt =
dpoint_eq
  {|
    pointed_fun := fun x : B => snd (s x);
    dpoint_eq := ap snd (dpoint_eq s)
  |} @ (dpoint_eq (psnd o* s))^
    1: reflexivity.
H: Funext
A, B: pType
s: pForall B
  {|
    pfam_pr1 := fun _ : B => (A * B)%type;
    dpoint := (pt, pt)
  |}
(fun x0 : B => 1) pt =
dpoint_eq
  {|
    pointed_fun := fun x : B => snd (s x);
    dpoint_eq := ap snd (dpoint_eq s)
  |} @ (dpoint_eq (psnd o* s))^
    cbn.
H: Funext
A, B: pType
s: pForall B
  {|
    pfam_pr1 := fun _ : B => (A * B)%type;
    dpoint := (pt, pt)
  |}
1 = ap snd (dpoint_eq s) @ (ap snd (point_eq s) @ 1)^
    apply moveL_pV.
H: Funext
A, B: pType
s: pForall B
  {|
    pfam_pr1 := fun _ : B => (A * B)%type;
    dpoint := (pt, pt)
  |}
1 @ (ap snd (point_eq s) @ 1) = ap snd (dpoint_eq s)
    exact (concat_1p _ @ concat_p1 _). }
H: Funext
A, B: pType
{s : (B ->* A) * (B ->* B) & snd s ==* pmap_idmap} <~>
(B ->* A)
  snrefine (_ oE equiv_functor_sigma_id (fun s => equiv_path_pforall _ _)).
H: Funext
A, B: pType
{s : (B ->* A) * (B ->* B) & snd s = pmap_idmap} <~>
(B ->* A)
  snrefine (_ oE (equiv_functor_sigma_pb (equiv_sigma_prod0 _ _))^-1%equiv); cbn.
H: Funext
A, B: pType
{x : {_ : B ->* A & B ->* B} & x.2 = pmap_idmap} <~>
(B ->* A)
  refine (_ oE (equiv_sigma_assoc _ _)^-1%equiv).
H: Funext
A, B: pType
{_ : B ->* A & {p : B ->* B & p = pmap_idmap}} <~>
(B ->* A)
  rapply equiv_sigma_contr.
Defined.