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

Local Open Scope pointed_scope.

(** ** Pointed fibers *)

Global 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 (pfiber f) A pr1 1.

(** 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.
A, B: pType
f: A ->* B
pfiber (pfib f) <~>* loops B
Proof.
A, B: pType
f: A ->* B
pfiber (pfib f) <~>* loops B
  pointed_reduce_pmap f.
A: pType
B: Type
f: A -> B
pfiber (pfib {| pointed_fun := f; dpoint_eq := 1 |}) <~>*
loops [B, f pt]
  snrapply Build_pEquiv'.
A: pType
B: Type
f: A -> B
pfiber (pfib {| pointed_fun := f; dpoint_eq := 1 |}) <~>
loops [B, f pt]
A: pType
B: Type
f: A -> B
?f pt = pt
  1: make_equiv_contr_basedpaths.
A: pType
B: Type
f: A -> B
equiv_adjointify
  (fun
     H : pfiber
           (pfib
              {| pointed_fun := f; dpoint_eq := 1 |})
   =>
   (fun H0 : hfiber f (f pt) =>
    (fun (H1 : A) (H2 : f H1 = f pt)
       (H3 : (H1; H2).1 = pt) =>
     paths_ind_r pt
       (fun (y : A) (_ : y = pt) =>
        f y = f pt -> loops [B, f pt])
       (fun H4 : f pt = f pt => H4 : loops [B, f pt])
       H1 H3 H2) H0.1 H0.2) H.1 H.2)
  (fun H : loops [B, f pt] =>
   ((let H0 := pt in H0;
    H : f (let H0 := pt in H0) = f pt)
    :
    hfiber f (f pt);
   1
   :
   ((let H0 := pt in H0;
    H : f (let H0 := pt in H0) = f pt)
    :
    hfiber f (f pt)).1 = pt)
   :
   pfiber
     (pfib {| pointed_fun := f; dpoint_eq := 1 |}))
  ((fun H : loops [B, f pt] => 1)
   :
   (fun
      H : pfiber
            (pfib
               {| pointed_fun := f; dpoint_eq := 1 |})
    =>
    (fun H0 : hfiber f (f pt) =>
     (fun (H1 : A) (H2 : f H1 = f pt)
        (H3 : (H1; H2).1 = pt) =>
      paths_ind_r pt
        (fun (y : A) (_ : y = pt) =>
         f y = f pt -> loops [B, f pt])
        (fun H4 : f pt = f pt => H4 : loops [B, f pt])
        H1 H3 H2) H0.1 H0.2) H.1 H.2)
   o (fun H : loops [B, f pt] =>
      ((let H0 := pt in H0;
       H : f (let H0 := pt in H0) = f pt)
       :
       hfiber f (f pt);
      1
      :
      ((let H0 := pt in H0;
       H : f (let H0 := pt in H0) = f pt)
       :
       hfiber f (f pt)).1 = pt)
      :
      pfiber
        (pfib {| pointed_fun := f; dpoint_eq := 1 |})) ==
   idmap)
  ((fun
      H : pfiber
            (pfib
               {| pointed_fun := f; dpoint_eq := 1 |})
    =>
    (fun H0 : hfiber f (f pt) =>
     (fun (H1 : A) (H2 : f H1 = f pt)
        (H3 : (H1; H2).1 = pt) =>
      paths_ind_r pt
        (fun (y : A) (p : y = pt) =>
         forall H4 : f y = f pt,
         ((let H5 := pt in H5;
          paths_ind_r pt
            (fun (y0 : A) (_ : y0 = pt) =>
             f y0 = f pt -> loops [B, f pt]) idmap y p
            H4); 1) = ((y; H4); p))
        (fun H4 : f pt = f pt => 1) H1 H3 H2) H0.1
       H0.2) H.1 H.2)
   :
   (fun H : loops [B, f pt] =>
    ((let H0 := pt in H0;
     H : f (let H0 := pt in H0) = f pt)
     :
     hfiber f (f pt);
    1
    :
    ((let H0 := pt in H0;
     H : f (let H0 := pt in H0) = f pt)
     :
     hfiber f (f pt)).1 = pt)
    :
    pfiber
      (pfib {| pointed_fun := f; dpoint_eq := 1 |}))
   o (fun
        H : pfiber
              (pfib
                 {|
                   pointed_fun := f; dpoint_eq := 1
                 |}) =>
      (fun H0 : hfiber f (f pt) =>
       (fun (H1 : A) (H2 : f H1 = f pt)
          (H3 : (H1; H2).1 = pt) =>
        paths_ind_r pt
          (fun (y : A) (_ : y = pt) =>
           f y = f pt -> loops [B, f pt])
          (fun H4 : f pt = f pt =>
           H4 : loops [B, f pt]) H1 H3 H2) H0.1 H0.2)
        H.1 H.2) == idmap) pt = pt
  reflexivity.
Defined.

Definition pfiber_fmap_loops {A B : pType} (f : A ->* B)
  : pfiber (fmap loops f) <~>* loops (pfiber f).
A, B: pType
f: A ->* B
pfiber (fmap loops f) <~>* loops (pfiber f)
Proof.
A, B: pType
f: A ->* B
pfiber (fmap loops f) <~>* loops (pfiber f)
  srapply Build_pEquiv'.
A, B: pType
f: A ->* B
pfiber (fmap loops f) <~> loops (pfiber f)
A, B: pType
f: A ->* B
?f pt = pt
  {
A, B: pType
f: A ->* B
pfiber (fmap loops f) <~> loops (pfiber f) etransitivity.
A, B: pType
f: A ->* B
pfiber (fmap loops f) <~> ?Goal
A, B: pType
f: A ->* B
?Goal <~> loops (pfiber f)
    2: srapply equiv_path_sigma.
A, B: pType
f: A ->* B
pfiber (fmap loops f) <~>
{p : pt.1 = pt.1 &
transport (fun x : A => f x = pt) p pt.2 = pt.2}
    simpl; unfold hfiber.
A, B: pType
f: A ->* B
{x : pt = pt &
(point_eq f)^ @ (ap f x @ point_eq f) = pt} <~>
{p : pt = pt &
transport (fun x : A => f x = pt) p (point_eq f) =
point_eq f}
    srapply equiv_functor_sigma_id.
A, B: pType
f: A ->* B
forall a : pt = pt,
(fun x : pt = pt =>
 (point_eq f)^ @ (ap f x @ point_eq f) = pt) a <~>
(fun p : pt = pt =>
 transport (fun x : A => f x = pt) p (point_eq f) =
 point_eq f) a
    intro p; cbn.
A, B: pType
f: A ->* B
p: pt = pt
(point_eq f)^ @ (ap f p @ point_eq f) = pt <~>
transport (fun x : A => f x = pt) p (point_eq f) =
point_eq f
    refine (_ oE equiv_moveL_Mp _ _ _).
A, B: pType
f: A ->* B
p: pt = pt
ap f p @ point_eq f = point_eq f @ pt <~>
transport (fun x : A => f x = pt) p (point_eq f) =
point_eq f
    refine (_ oE equiv_concat_r (concat_p1 _) _).
A, B: pType
f: A ->* B
p: pt = pt
ap f p @ point_eq f = point_eq f <~>
transport (fun x : A => f x = pt) p (point_eq f) =
point_eq f
    refine (_ oE equiv_moveL_Vp _ _ _).
A, B: pType
f: A ->* B
p: pt = pt
point_eq f = (ap f p)^ @ point_eq f <~>
transport (fun x : A => f x = pt) p (point_eq f) =
point_eq f
    refine (_ oE equiv_path_inverse _ _).
A, B: pType
f: A ->* B
p: pt = pt
(ap f p)^ @ point_eq f = point_eq f <~>
transport (fun x : A => f x = pt) p (point_eq f) =
point_eq f
    apply equiv_concat_l.
A, B: pType
f: A ->* B
p: pt = pt
transport (fun x : A => f x = pt) p (point_eq f) =
(ap f p)^ @ point_eq f
    apply transport_paths_Fl. }
A, B: pType
f: A ->* B
(fun (x y z : Type) (f : x <~> y) (g : y <~> z) =>
 equiv_compose g f) (pfiber (fmap loops f))
  {p : pt.1 = pt.1 &
  transport (fun x : A => f x = pt) p pt.2 = pt.2}
  (loops (pfiber f))
  ((equiv_functor_sigma_id
      (fun p : pt = pt =>
       equiv_concat_l
         (transport_paths_Fl p (point_eq f))
         (point_eq f)
       oE equiv_path_inverse (point_eq f)
            ((ap f p)^ @ point_eq f)
       oE equiv_moveL_Vp (point_eq f) (point_eq f)
            (ap f p)
       oE equiv_concat_r (concat_p1 (point_eq f))
            (ap f p @ point_eq f)
       oE equiv_moveL_Mp pt (ap f p @ point_eq f)
            (point_eq f)
       :
       (fun x : pt = pt =>
        (point_eq f)^ @ (ap f x @ point_eq f) = pt) p <~>
       (fun p0 : pt = pt =>
        transport (fun x : A => f x = pt) p0
          (point_eq f) = point_eq f) p)
    :
    hfiber
      (fun p : pt = pt =>
       (point_eq f)^ @ (ap f p @ point_eq f)) pt <~>
    {p : pt = pt &
    transport (fun x : A => f x = pt) p (point_eq f) =
    point_eq f})
   :
   pfiber (fmap loops f) <~>
   {p : pt.1 = pt.1 &
   transport (fun x : A => f x = pt) p pt.2 = pt.2})
  (equiv_path_sigma (fun x : A => f x = pt) pt pt) pt =
pt
  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).
A, B: pType
f: A ->* B
fmap loops (pfib f) o* pfiber_fmap_loops f ==*
pfib (fmap loops f)
Proof.
A, B: pType
f: A ->* B
fmap loops (pfib f) o* pfiber_fmap_loops f ==*
pfib (fmap loops f)
  srapply Build_pHomotopy.
A, B: pType
f: A ->* B
fmap loops (pfib f) o* pfiber_fmap_loops f ==
pfib (fmap loops f)
A, B: pType
f: A ->* B
?p pt =
dpoint_eq (fmap loops (pfib f) o* pfiber_fmap_loops f) @
(dpoint_eq (pfib (fmap loops f)))^
  -
A, B: pType
f: A ->* B
fmap loops (pfib f) o* pfiber_fmap_loops f ==
pfib (fmap loops f) intros [u v].
A, B: pType
f: A ->* B
u: loops A
v: fmap loops f u = pt
(fmap loops (pfib f) o* pfiber_fmap_loops f) (u; v) =
pfib (fmap loops f) (u; v)
    refine (concat_1p _ @ concat_p1 _ @ _).
A, B: pType
f: A ->* B
u: loops A
v: fmap loops f u = pt
ap (pfib f) (pfiber_fmap_loops f (u; v)) =
pfib (fmap loops f) (u; v)
    exact (@ap_pr1_path_sigma _ _ (point A; point_eq f) (point A;point_eq f) _ _).
  -
A, B: pType
f: A ->* B
((fun x : pfiber (fmap loops f) =>
  (fun (u : loops A) (v : fmap loops f u = pt) =>
   (concat_1p
      (ap (pfib f) (pfiber_fmap_loops f (u; v)) @ 1) @
    concat_p1
      (ap (pfib f) (pfiber_fmap_loops f (u; v)))) @
   ap_pr1_path_sigma (1%equiv (u; v).1)
     ((fun p : pt = pt =>
       equiv_concat_l
         (transport_paths_Fl p (point_eq f))
         (point_eq f)
       oE equiv_path_inverse (point_eq f)
            ((ap f p)^ @ point_eq f)
       oE equiv_moveL_Vp (point_eq f) (point_eq f)
            (ap f p)
       oE equiv_concat_r (concat_p1 (point_eq f))
            (ap f p @ point_eq f)
       oE equiv_moveL_Mp pt (ap f p @ point_eq f)
            (point_eq f)
       :
       (fun x0 : pt = pt =>
        (point_eq f)^ @ (ap f x0 @ point_eq f) = pt) p <~>
       (fun p0 : pt = pt =>
        transport (fun x0 : A => f x0 = pt) p0
          (point_eq f) = point_eq f) p) (u; v).1
        (u; v).2)) x.1 x.2)
 :
 fmap loops (pfib f) o* pfiber_fmap_loops f ==
 pfib (fmap loops f)) pt =
dpoint_eq (fmap loops (pfib f) o* pfiber_fmap_loops f) @
(dpoint_eq (pfib (fmap loops 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).
A, B: pType
n: nat
f: A ->* B
pfiber (fmap (iterated_loops n) f) <~>*
iterated_loops n (pfiber f)
Proof.
A, B: pType
n: nat
f: A ->* B
pfiber (fmap (iterated_loops n) f) <~>*
iterated_loops n (pfiber f)
  induction n.
A, B: pType
f: A ->* B
pfiber (fmap (iterated_loops 0) f) <~>*
iterated_loops 0 (pfiber f)
A, B: pType
n: nat
f: A ->* B
IHn: pfiber (fmap (iterated_loops n) f) <~>* iterated_loops n (pfiber f)
pfiber (fmap (iterated_loops n.+1) f) <~>*
iterated_loops n.+1 (pfiber f)
  1: reflexivity.
A, B: pType
n: nat
f: A ->* B
IHn: pfiber (fmap (iterated_loops n) f) <~>* iterated_loops n (pfiber f)
pfiber (fmap (iterated_loops n.+1) f) <~>*
iterated_loops n.+1 (pfiber f)
  refine (_ o*E pfiber_fmap_loops _ ).
A, B: pType
n: nat
f: A ->* B
IHn: pfiber (fmap (iterated_loops n) f) <~>* iterated_loops n (pfiber f)
loops (pfiber (fmap (iterated_loops n) f)) <~>*
iterated_loops n.+1 (pfiber f)
  rapply (emap loops).
A, B: pType
n: nat
f: A ->* B
IHn: pfiber (fmap (iterated_loops n) f) <~>* iterated_loops n (pfiber f)
pfiber (fmap (iterated_loops n) f) $<~>
(fix F (m : nat) : pType :=
   match m with
   | 0%nat => pfiber f
   | (m'.+1)%nat => loops (F m')
   end) n
  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.
A, B, C, D: pType
f: A ->* B
g: C ->* D
h: A ->* C
k: B ->* D
p: k o* f ==* g o* h
pfiber f ->* pfiber g
Proof.
A, B, C, D: pType
f: A ->* B
g: C ->* D
h: A ->* C
k: B ->* D
p: k o* f ==* g o* h
pfiber f ->* pfiber g
  srapply Build_pMap.
A, B, C, D: pType
f: A ->* B
g: C ->* D
h: A ->* C
k: B ->* D
p: k o* f ==* g o* h
pfiber f -> pfiber g
A, B, C, D: pType
f: A ->* B
g: C ->* D
h: A ->* C
k: B ->* D
p: k o* f ==* g o* h
?Goal pt = pt
  +
A, B, C, D: pType
f: A ->* B
g: C ->* D
h: A ->* C
k: B ->* D
p: k o* f ==* g o* h
pfiber f -> pfiber g cbn.
A, B, C, D: pType
f: A ->* B
g: C ->* D
h: A ->* C
k: B ->* D
p: k o* f ==* g o* h
hfiber f pt -> hfiber g pt refine (functor_hfiber2 p (point_eq k)).
  +
A, B, C, D: pType
f: A ->* B
g: C ->* D
h: A ->* C
k: B ->* D
p: k o* f ==* g o* h
(functor_hfiber2 p (point_eq k) : pfiber f -> pfiber g)
  pt = pt srapply path_hfiber.
A, B, C, D: pType
f: A ->* B
g: C ->* D
h: A ->* C
k: B ->* D
p: k o* f ==* g o* h
(functor_hfiber2 p (point_eq k) pt).1 = pt.1
A, B, C, D: pType
f: A ->* B
g: C ->* D
h: A ->* C
k: B ->* D
p: k o* f ==* g o* h
(functor_hfiber2 p (point_eq k) pt).2 = ap g ?q @ pt.2 
    -
A, B, C, D: pType
f: A ->* B
g: C ->* D
h: A ->* C
k: B ->* D
p: k o* f ==* g o* h
(functor_hfiber2 p (point_eq k) pt).1 = pt.1 apply point_eq.
    -
A, B, C, D: pType
f: A ->* B
g: C ->* D
h: A ->* C
k: B ->* D
p: k o* f ==* g o* h
(functor_hfiber2 p (point_eq k) pt).2 =
ap g (point_eq h) @ pt.2 refine (concat_pp_p _ _ _ @ _).
A, B, C, D: pType
f: A ->* B
g: C ->* D
h: A ->* C
k: B ->* D
p: k o* f ==* g o* h
(p pt.1)^ @ (ap k pt.2 @ point_eq k) =
ap g (point_eq h) @ pt.2 apply moveR_Vp.
A, B, C, D: pType
f: A ->* B
g: C ->* D
h: A ->* C
k: B ->* D
p: k o* f ==* g o* h
ap k pt.2 @ point_eq k =
p pt.1 @ (ap g (point_eq h) @ pt.2) apply (point_htpy p)^.
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.
A, B, C, D: pType
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.
A, B, C, D: pType
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
  srapply Build_pHomotopy.
A, B, C, D: pType
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
A, B, C, D: pType
f: A ->* B
g: C ->* D
h: A ->* C
k: B ->* D
p: k o* f ==* g o* h
?p pt =
dpoint_eq (h o* pfib f) @
(dpoint_eq (pfib g o* functor_pfiber p))^
  -
A, B, C, D: pType
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 intros x; reflexivity.
  -
A, B, C, D: pType
f: A ->* B
g: C ->* D
h: A ->* C
k: B ->* D
p: k o* f ==* g o* h
((fun x : pfiber f => 1)
 :
 h o* pfib f == pfib g o* functor_pfiber p) pt =
dpoint_eq (h o* pfib f) @
(dpoint_eq (pfib g o* functor_pfiber p))^ apply moveL_pV.
A, B, C, D: pType
f: A ->* B
g: C ->* D
h: A ->* C
k: B ->* D
p: k o* f ==* g o* h
1 @ dpoint_eq (pfib g o* functor_pfiber p) =
dpoint_eq (h o* pfib f) cbn; unfold functor_sigma; cbn.
A, B, C, D: pType
f: A ->* B
g: C ->* D
h: A ->* C
k: B ->* D
p: k o* f ==* g o* h
1 @
(ap pr1
   (path_sigma_uncurried (fun x : C => g x = pt)
      (functor_hfiber2 p (point_eq k)
         (ispointed_fiber f)) (ispointed_fiber g)
      (point_eq h;
      transport_paths_Fl (point_eq h)
        (((p pt)^ @ ap k (point_eq f)) @ point_eq k) @
      moveR_Vp
        (((p pt)^ @ ap k (point_eq f)) @ point_eq k)
        (point_eq g) (ap g (point_eq h))
        (concat_pp_p (p pt)^ (ap k (point_eq f))
           (point_eq k) @
         moveR_Vp (ap k (point_eq f) @ point_eq k)
           (ap g (point_eq h) @ point_eq g) (p pt)
           (point_htpy p)^))) @ 1) = 1 @ point_eq h
    abstract (rewrite ap_pr1_path_sigma, concat_p1; reflexivity).
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 triple-fiber functor is equal to the negative of the loopspace 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)).
A, B: pType
f: A ->* B
pfiber2_loops f o* pfib (pfib (pfib f)) ==*
fmap loops f
o* (loops_inv A o* pfiber2_loops (pfib f))
Proof.
A, B: pType
f: A ->* B
pfiber2_loops f o* pfib (pfib (pfib f)) ==*
fmap loops f
o* (loops_inv A o* pfiber2_loops (pfib f))
  pointed_reduce.
A: Type
point0: IsPointed A
B: Type
f: A -> B
Build_pMap
  (pfiber
     (pfib {| pointed_fun := f; dpoint_eq := 1 |}))
  (loops [B, f point0])
  (fun H : hfiber pr1 point0 =>
   paths_ind_r point0
     (fun (y : A) (_ : y = point0) =>
      f y = f point0 -> f point0 = f point0) idmap
     (H.1).1 H.2 (H.1).2) 1
o* pfib
     (pfib
        (pfib {| pointed_fun := f; dpoint_eq := 1 |})) ==*
Build_pMap (loops [A, point0]) (loops [B, f point0])
  (fun p : point0 = point0 => 1 @ (ap f p @ 1)) 1
o* (Build_pMap (loops [A, point0]) (loops [A, point0])
      inverse 1
    o* Build_pMap
         (pfiber
            (pfib
               {|
                 pointed_fun := pr1; dpoint_eq := 1
               |})) (loops [A, point0])
         (fun
            H : hfiber pr1
                  (ispointed_fiber
                     {|
                       pointed_fun := f;
                       dpoint_eq := 1
                     |}) =>
          paths_ind_r
            (ispointed_fiber
               {| pointed_fun := f; dpoint_eq := 1 |})
            (fun (y : hfiber f (f point0))
               (_ : y =
                    ispointed_fiber
                      {|
                        pointed_fun := f;
                        dpoint_eq := 1
                      |}) =>
             y.1 = point0 -> point0 = point0) idmap
            (H.1).1 H.2 (H.1).2) 1)
  simple refine (Build_pHomotopy _ _).
A: Type
point0: IsPointed A
B: Type
f: A -> B
Build_pMap
  (pfiber
     (pfib {| pointed_fun := f; dpoint_eq := 1 |}))
  (loops [B, f point0])
  (fun H : hfiber pr1 point0 =>
   paths_ind_r point0
     (fun (y : A) (_ : y = point0) =>
      f y = f point0 -> f point0 = f point0) idmap
     (H.1).1 H.2 (H.1).2) 1
o* pfib
     (pfib
        (pfib {| pointed_fun := f; dpoint_eq := 1 |})) ==
Build_pMap (loops [A, point0]) 
  (loops [B, f point0])
  (fun p : point0 = point0 => 1 @ (ap f p @ 1)) 1
o* (Build_pMap (loops [A, point0]) 
      (loops [A, point0]) inverse 1
    o* Build_pMap
         (pfiber
            (pfib
               {|
                 pointed_fun := pr1; dpoint_eq := 1
               |})) (loops [A, point0])
         (fun
            H : hfiber pr1
                  (ispointed_fiber
                     {|
                       pointed_fun := f;
                       dpoint_eq := 1
                     |}) =>
          paths_ind_r
            (ispointed_fiber
               {| pointed_fun := f; dpoint_eq := 1 |})
            (fun (y : hfiber f (f point0))
               (_ : y =
                    ispointed_fiber
                      {|
                       pointed_fun := f;
                       dpoint_eq := 1
                      |}) =>
             y.1 = point0 -> point0 = point0) idmap
            (H.1).1 H.2 
            (H.1).2) 1)
A: Type
point0: IsPointed A
B: Type
f: A -> B
?p pt =
dpoint_eq
  (Build_pMap
     (pfiber
        (pfib {| pointed_fun := f; dpoint_eq := 1 |}))
     (loops [B, f point0])
     (fun H : hfiber pr1 point0 =>
      paths_ind_r point0
        (fun (y : A) (_ : y = point0) =>
         f y = f point0 -> f point0 = f point0) idmap
        (H.1).1 H.2 (H.1).2) 1
   o* pfib
        (pfib
           (pfib
              {| pointed_fun := f; dpoint_eq := 1 |}))) @
(dpoint_eq
   (Build_pMap (loops [A, point0])
      (loops [B, f point0])
      (fun p : point0 = point0 => 1 @ (ap f p @ 1)) 1
    o* (Build_pMap (loops [A, point0])
          (loops [A, point0]) inverse 1
        o* Build_pMap
             (pfiber
                (pfib
                   {|
                     pointed_fun := pr1;
                     dpoint_eq := 1
                   |})) 
             (loops [A, point0])
             (fun
                H : hfiber pr1
                      (ispointed_fiber
                       {|
                       pointed_fun := f;
                       dpoint_eq := 1
                       |}) =>
              paths_ind_r
                (ispointed_fiber
                   {|
                     pointed_fun := f; dpoint_eq := 1
                   |})
                (fun (y : hfiber f (f point0))
                   (_ : 
                    y =
                    ispointed_fiber
                      {|
                       pointed_fun := f;
                       dpoint_eq := 1
                      |}) =>
                 y.1 = point0 -> point0 = point0)
                idmap (H.1).1 H.2 
                (H.1).2) 1)))^
  -
A: Type
point0: IsPointed A
B: Type
f: A -> B
Build_pMap
  (pfiber
     (pfib {| pointed_fun := f; dpoint_eq := 1 |}))
  (loops [B, f point0])
  (fun H : hfiber pr1 point0 =>
   paths_ind_r point0
     (fun (y : A) (_ : y = point0) =>
      f y = f point0 -> f point0 = f point0) idmap
     (H.1).1 H.2 (H.1).2) 1
o* pfib
     (pfib
        (pfib {| pointed_fun := f; dpoint_eq := 1 |})) ==
Build_pMap (loops [A, point0]) 
  (loops [B, f point0])
  (fun p : point0 = point0 => 1 @ (ap f p @ 1)) 1
o* (Build_pMap (loops [A, point0]) 
      (loops [A, point0]) inverse 1
    o* Build_pMap
         (pfiber
            (pfib
               {|
                 pointed_fun := pr1; dpoint_eq := 1
               |})) (loops [A, point0])
         (fun
            H : hfiber pr1
                  (ispointed_fiber
                     {|
                       pointed_fun := f;
                       dpoint_eq := 1
                     |}) =>
          paths_ind_r
            (ispointed_fiber
               {| pointed_fun := f; dpoint_eq := 1 |})
            (fun (y : hfiber f (f point0))
               (_ : y =
                    ispointed_fiber
                      {|
                       pointed_fun := f;
                       dpoint_eq := 1
                      |}) =>
             y.1 = point0 -> point0 = point0) idmap
            (H.1).1 H.2 
            (H.1).2) 1) intros [[[x p] q] r].
A: Type
point0: IsPointed A
B: Type
f: A -> B
x: [A, point0]
p: {| pointed_fun := f; dpoint_eq := 1 |} x = pt
q: pfib {| pointed_fun := f; dpoint_eq := 1 |} (x; p) =
pt
r: pfib (pfib {| pointed_fun := f; dpoint_eq := 1 |})
  ((x; p); q) = pt
(Build_pMap
   (pfiber
      (pfib {| pointed_fun := f; dpoint_eq := 1 |}))
   (loops [B, f point0])
   (fun H : hfiber pr1 point0 =>
    paths_ind_r point0
      (fun (y : A) (_ : y = point0) =>
       f y = f point0 -> f point0 = f point0) idmap
      (H.1).1 H.2 (H.1).2) 1
 o* pfib
      (pfib
         (pfib {| pointed_fun := f; dpoint_eq := 1 |})))
  (((x; p); q); r) =
(Build_pMap (loops [A, point0]) 
   (loops [B, f point0])
   (fun p : point0 = point0 => 1 @ (ap f p @ 1)) 1
 o* (Build_pMap (loops [A, point0])
       (loops [A, point0]) inverse 1
     o* Build_pMap
          (pfiber
             (pfib
                {|
                  pointed_fun := pr1; dpoint_eq := 1
                |})) (loops [A, point0])
          (fun
             H : hfiber pr1
                   (ispointed_fiber
                      {|
                       pointed_fun := f;
                       dpoint_eq := 1
                      |}) =>
           paths_ind_r
             (ispointed_fiber
                {| pointed_fun := f; dpoint_eq := 1 |})
             (fun (y : hfiber f (f point0))
                (_ : y =
                     ispointed_fiber
                       {|
                       pointed_fun := f;
                       dpoint_eq := 1
                       |}) =>
              y.1 = point0 -> point0 = point0) idmap
             (H.1).1 H.2 
             (H.1).2) 1)) 
  (((x; p); q); r) simpl in *.
A: Type
point0: IsPointed A
B: Type
f: A -> B
x: A
p: f x = pt
q: x = pt
r: (x; p) = pt
paths_ind_r point0
  (fun (y : A) (_ : y = point0) =>
   f y = f point0 -> f point0 = f point0) idmap x q p =
1 @
(ap f
   (paths_ind_r
      (ispointed_fiber
         {| pointed_fun := f; dpoint_eq := 1 |})
      (fun (y : hfiber f (f point0))
         (_ : y =
              ispointed_fiber
                {| pointed_fun := f; dpoint_eq := 1 |})
       => y.1 = point0 -> point0 = point0) idmap
      (x; p) r q)^ @ 1)
    (** 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.
A: Type
point0: IsPointed A
B: Type
f: A -> B
p: f pt = pt
r: (pt; p) = pt
p =
1 @
(ap f
   (paths_ind_r
      (ispointed_fiber
         {| pointed_fun := f; dpoint_eq := 1 |})
      (fun (y : hfiber f (f point0))
         (_ : y =
              ispointed_fiber
                {| pointed_fun := f; dpoint_eq := 1 |})
       => y.1 = point0 -> point0 = point0) idmap
      (pt; p) r 1)^ @ 1)
    rewrite !concat_1p, concat_p1.
A: Type
point0: IsPointed A
B: Type
f: A -> B
p: f pt = pt
r: (pt; p) = pt
p =
ap f
  (paths_ind_r
     (ispointed_fiber
        {| pointed_fun := f; dpoint_eq := 1 |})
     (fun (y : hfiber f (f point0))
        (_ : y =
             ispointed_fiber
               {| pointed_fun := f; dpoint_eq := 1 |})
      => y.1 = point0 -> point0 = point0) idmap
     (pt; p) r 1)^
    rewrite paths_ind_r_transport.
A: Type
point0: IsPointed A
B: Type
f: A -> B
p: f pt = pt
r: (pt; p) = pt
p =
ap f
  (transport
     (fun b : hfiber f (f point0) =>
      b.1 = point0 -> point0 = point0) r^ idmap 1)^
    rewrite transport_arrow_toconst, transport_paths_Fl.
A: Type
point0: IsPointed A
B: Type
f: A -> B
p: f pt = pt
r: (pt; p) = pt
p =
ap f
  ((ap (fun x : hfiber f (f point0) => x.1) (r^)^)^ @
   1)^ 
    rewrite concat_p1, inv_V, ap_V.
A: Type
point0: IsPointed A
B: Type
f: A -> B
p: f pt = pt
r: (pt; p) = pt
p = ap f (ap (fun x : hfiber f (f point0) => x.1) r^)^
    refine (((r^)..2)^ @ _).
A: Type
point0: IsPointed A
B: Type
f: A -> B
p: f pt = pt
r: (pt; p) = pt
transport (fun x : A => f x = pt) (r^) ..1 pt.2 =
ap f (ap (fun x : hfiber f (f point0) => x.1) r^)^
    rewrite transport_paths_Fl; cbn.
A: Type
point0: IsPointed A
B: Type
f: A -> B
p: f pt = pt
r: (pt; p) = pt
(ap f (r^) ..1)^ @ 1 =
ap f (ap (fun x : hfiber f (f point0) => x.1) r^)^
    rewrite pr1_path_V, !ap_V, !inv_V.
A: Type
point0: IsPointed A
B: Type
f: A -> B
p: f pt = pt
r: (pt; p) = pt
ap f r ..1 @ 1 =
ap f (ap (fun x : hfiber f (f point0) => x.1) r)
    apply concat_p1.
  -
A: Type
point0: IsPointed A
B: Type
f: A -> B
((fun
    x0 : pfiber
           (pfib
              (pfib
                 {|
                   pointed_fun := f; dpoint_eq := 1
                 |})) =>
  (fun
     proj2 : pfiber
               (pfib
                  {|
                    pointed_fun := f; dpoint_eq := 1
                  |}) =>
   (fun
      proj3 : pfiber
                {| pointed_fun := f; dpoint_eq := 1 |}
    =>
    (fun (x : [A, point0])
       (p : {| pointed_fun := f; dpoint_eq := 1 |} x =
            pt)
       (q : pfib
              {| pointed_fun := f; dpoint_eq := 1 |}
              (x; p) = pt)
       (r : pfib
              (pfib
                 {|
                   pointed_fun := f; dpoint_eq := 1
                 |}) ((x; p); q) = pt) =>
     paths_ind_r pt
       (fun (y : A) (p0 : y = pt) =>
        forall (p1 : f y = pt) 
        (r0 : (y; p1) = pt),
        paths_ind_r point0
          (fun (y0 : A) (_ : y0 = point0) =>
           f y0 = f point0 -> f point0 = f point0)
          idmap y p0 p1 =
        1 @
        (ap f (paths_ind_r ... ... idmap ... r0 p0)^ @
         1))
       (fun (p0 : f pt = pt) (r0 : (pt; p0) = pt) =>
        internal_paths_rew_r
          (fun p1 : f point0 = f point0 => p0 = p1)
          (internal_paths_rew_r
             (fun p1 : ... => p0 = p1)
             (internal_paths_rew_r 
                (... => ...)
                (internal_paths_rew_r ... ... ...)
                (paths_ind_r_transport ... r0 idmap))
             (concat_p1 (ap f ...^)))
          (concat_1p (ap f (...)^ @ 1))
        :
        paths_ind_r point0
          (fun (y : A) (_ : y = point0) =>
           f y = f point0 -> f point0 = f point0)
          idmap pt 1 p0 =
        1 @
        (ap f (paths_ind_r ... ... idmap ... r0 1)^ @
         1)) x q p r
     :
     (Build_pMap (pfiber (pfib {| ...; ... |}))
        (loops [B, f point0])
        (fun H : hfiber pr1 point0 =>
         paths_ind_r point0
           (fun ... ... => ... -> ...) idmap 
           (H.1).1 H.2 (H.1).2) 1
      o* pfib (pfib (pfib {| ...; ... |})))
       (((x; p); q); r) =
     (Build_pMap (loops [A, point0])
        (loops [B, f point0])
        (fun p0 : point0 = point0 => 1 @ (ap f p0 @ 1))
        1
      o* (Build_pMap (loops [A, point0])
            (loops [A, point0]) inverse 1
          o* Build_pMap 
               (pfiber (pfib ...)) 
               (loops [A, point0])
               (fun H : ... =>
                paths_ind_r 
                  (...) 
                  (...) idmap 
                  (H.1).1 H.2 
                  (H.1).2) 1)) 
       (((x; p); q); r)) proj3.1 proj3.2) proj2.1
     proj2.2) x0.1 x0.2)
 :
 Build_pMap
   (pfiber
      (pfib {| pointed_fun := f; dpoint_eq := 1 |}))
   (loops [B, f point0])
   (fun H : hfiber pr1 point0 =>
    paths_ind_r point0
      (fun (y : A) (_ : y = point0) =>
       f y = f point0 -> f point0 = f point0) idmap
      (H.1).1 H.2 (H.1).2) 1
 o* pfib
      (pfib
         (pfib {| pointed_fun := f; dpoint_eq := 1 |})) ==
 Build_pMap (loops [A, point0]) 
   (loops [B, f point0])
   (fun p : point0 = point0 => 1 @ (ap f p @ 1)) 1
 o* (Build_pMap (loops [A, point0])
       (loops [A, point0]) inverse 1
     o* Build_pMap
          (pfiber
             (pfib
                {|
                  pointed_fun := pr1; dpoint_eq := 1
                |})) (loops [A, point0])
          (fun
             H : hfiber pr1
                   (ispointed_fiber
                      {|
                       pointed_fun := f;
                       dpoint_eq := 1
                      |}) =>
           paths_ind_r
             (ispointed_fiber
                {| pointed_fun := f; dpoint_eq := 1 |})
             (fun (y : hfiber f (f point0))
                (_ : y =
                     ispointed_fiber
                       {|
                       pointed_fun := f;
                       dpoint_eq := 1
                       |}) =>
              y.1 = point0 -> point0 = point0) idmap
             (H.1).1 H.2 
             (H.1).2) 1)) pt =
dpoint_eq
  (Build_pMap
     (pfiber
        (pfib {| pointed_fun := f; dpoint_eq := 1 |}))
     (loops [B, f point0])
     (fun H : hfiber pr1 point0 =>
      paths_ind_r point0
        (fun (y : A) (_ : y = point0) =>
         f y = f point0 -> f point0 = f point0) idmap
        (H.1).1 H.2 (H.1).2) 1
   o* pfib
        (pfib
           (pfib
              {| pointed_fun := f; dpoint_eq := 1 |}))) @
(dpoint_eq
   (Build_pMap (loops [A, point0])
      (loops [B, f point0])
      (fun p : point0 = point0 => 1 @ (ap f p @ 1)) 1
    o* (Build_pMap (loops [A, point0])
          (loops [A, point0]) inverse 1
        o* Build_pMap
             (pfiber
                (pfib
                   {|
                     pointed_fun := pr1;
                     dpoint_eq := 1
                   |})) 
             (loops [A, point0])
             (fun
                H : hfiber pr1
                      (ispointed_fiber
                       {|
                       pointed_fun := f;
                       dpoint_eq := 1
                       |}) =>
              paths_ind_r
                (ispointed_fiber
                   {|
                     pointed_fun := f; dpoint_eq := 1
                   |})
                (fun (y : hfiber f (f point0))
                   (_ : 
                    y =
                    ispointed_fiber
                      {|
                       pointed_fun := f;
                       dpoint_eq := 1
                      |}) =>
                 y.1 = point0 -> point0 = point0)
                idmap (H.1).1 H.2 
                (H.1).2) 1)))^ reflexivity.
Qed.