From HoTT Require Import Basics Types.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.

(** ** Pointed fibers *)

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).
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) (f0 : x <~> y) (g : y <~> z) => equiv_compose g f0)
  (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)
  tapply (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
?f 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 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. *)
  +
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 snapply path_sigma'.
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 pt.1 = 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
transport (fun x : C => g x = pt) ?p (((p pt.1)^ @ ap k pt.2) @ point_eq k) =
point_eq 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
h pt.1 = pt exact (point_eq h).
    -
A, B, C, D: pType
f: A ->* B
g: C ->* D
h: A ->* C
k: B ->* D
p: k o* f ==* g o* h
transport (fun x : C => g x = pt) (point_eq h)
  (((p pt.1)^ @ ap k pt.2) @ point_eq k) =
point_eq g lhs napply transport_paths_Fl.
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 g (point_eq h))^ @ (((p pt.1)^ @ ap k pt.2) @ point_eq k) = point_eq g
      lhs napply (whiskerL _ (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
(ap g (point_eq h))^ @ ((p pt.1)^ @ (ap k pt.2 @ point_eq k)) = point_eq g
      lhs napply (whiskerL _ (whiskerL _ (point_htpy 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
(ap g (point_eq h))^ @ ((p pt.1)^ @ (p pt @ dpoint_eq (g o* h))) = point_eq g
      lhs napply (whiskerL _ (concat_V_pp _ _)).
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 g (point_eq h))^ @ dpoint_eq (g o* h) = point_eq g
      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.
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.
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' (fun x : C => g x = pt) (point_eq h)
      (transport_paths_Fl (point_eq h)
         (((p pt)^ @ ap k (point_eq f)) @ point_eq k) @
       (whiskerL (ap g (point_eq h))^
          (concat_pp_p (p pt)^ (ap k (point_eq f)) (point_eq k)) @
        (whiskerL (ap g (point_eq h))^ (whiskerL (p pt)^ (point_htpy p)^) @
         (whiskerL (ap g (point_eq h))^
            (concat_V_pp (p pt) (ap g (point_eq h) @ point_eq g)) @
          concat_V_pp (ap g (point_eq h)) (point_eq g)))))) @
 1) =
1 @ point_eq h
    refine (1 @@ (concat_p1 _ @ _)).
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 pr1
  (path_sigma' (fun x : C => g x = pt) (point_eq h)
     (transport_paths_Fl (point_eq h)
        (((p pt)^ @ ap k (point_eq f)) @ point_eq k) @
      (whiskerL (ap g (point_eq h))^
         (concat_pp_p (p pt)^ (ap k (point_eq f)) (point_eq k)) @
       (whiskerL (ap g (point_eq h))^ (whiskerL (p pt)^ (point_htpy p)^) @
        (whiskerL (ap g (point_eq h))^
           (concat_V_pp (p pt) (ap g (point_eq h) @ point_eq g)) @
         concat_V_pp (ap g (point_eq h)) (point_eq g)))))) =
point_eq h
    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.
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]
  snapply 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.

(** 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.
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.
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
  pointed_reduce_pmap f.
A: pType
B: Type
f: A -> B
a: A
w: f a = f pt
v: a = pt
paths_ind_r pt (fun (y : A) (_ : y = pt) => f y = f pt -> f pt = f pt) idmap
  a v w =
(1 @ (ap f v)^) @ w
  destruct v; cbn.
A: pType
B: Type
f: A -> B
a: A
w: f a = f a
w = 1 @ w
  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)).
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
  (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 (fun p : point0 = point0 => 1 @ (ap f p @ 1)) 1
o* (Build_pMap inverse 1
    o* Build_pMap
         (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
  (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 (fun p : point0 = point0 => 1 @ (ap f p @ 1)) 1
o* (Build_pMap inverse 1
    o* Build_pMap
         (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
     (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 (fun p : point0 = point0 => 1 @ (ap f p @ 1)) 1
    o* (Build_pMap inverse 1
        o* Build_pMap
             (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
  (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 (fun p : point0 = point0 => 1 @ (ap f p @ 1)) 1
o* (Build_pMap inverse 1
    o* Build_pMap
         (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
   (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 (fun p0 : point0 = point0 => 1 @ (ap f p0 @ 1)) 1
 o* (Build_pMap inverse 1
     o* Build_pMap
          (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 proj1 : pfiber (pfib {| pointed_fun := f; dpoint_eq := 1 |}) =>
   (fun proj0 : 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
              (ispointed_fiber {| pointed_fun := f; dpoint_eq := 1 |})
              (fun (y0 : hfiber f (f point0))
                 (_ : y0 =
                      ispointed_fiber {| pointed_fun := f; dpoint_eq := 1 |}) =>
               y0.1 = point0 -> point0 = point0)
              idmap (y; p1) 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 : f point0 = f point0 => p0 = p1)
             (internal_paths_rew_r
                (fun p1 : (pt; p0).1 = point0 -> point0 = point0 =>
                 p0 = ap f (p1 1)^)
                (internal_paths_rew_r
                   (fun p1 : point0 = point0 => p0 = ap f p1^)
                   (internal_paths_rew_r
                      (fun
                         p1 : (ispointed_fiber
                                 {| pointed_fun := f; dpoint_eq := 1 |}).1 =
                              point0 =>
                       p0 = ap f p1^)
                      (internal_paths_rew_r
                         (fun
                            p1 : (ispointed_fiber
                                    {| pointed_fun := f; dpoint_eq := 1 |}).1 =
                                 (pt; p0).1 =>
                          p0 = ap f p1^)
                         (internal_paths_rew_r
                            (fun p1 : point0 = point0 => p0 = ap f p1)
                            (internal_paths_rew_r
                               (fun
                                  p1 : (pt; p0).1 =
                                       (ispointed_fiber
                                          {|
                                            pointed_fun := f; dpoint_eq := 1
                                          |}).1 =>
                                p0 = ap f p1)
                               (((r0^) ..2)^ @
                                internal_paths_rew_r
                                  (fun p1 : f (pt; p0).1 = pt =>
                                   p1 =
                                   ap f
                                     (ap
                                        (fun x1 : hfiber f (f point0) => x1.1)
                                        r0^)^)
                                  (internal_paths_rew_r
                                     (fun p1 : pt.1 = (pt; p0).1 =>
                                      (ap f p1)^ @ 1 =
                                      ap f
                                        (ap
                                           (fun x1 : hfiber f (f point0) =>
                                            x1.1)
                                           r0^)^)
                                     (internal_paths_rew_r
                                        (fun p1 : f pt.1 = f (pt; p0).1 =>
                                         p1^ @ 1 =
                                         ap f
                                           (ap
                                              (fun x1 : hfiber f (f point0) =>
                                               x1.1)
                                              r0^)^)
                                        (internal_paths_rew_r
                                           (fun p1 : f pt = f point0 =>
                                            ((ap f r0 ..1)^)^ @ 1 = p1)
                                           (internal_paths_rew_r
                                              (fun
                                                 p1 : 
                                                 (ispointed_fiber
                                                 {|
                                                 pointed_fun := f;
                                                 dpoint_eq := 1
                                                 |}).1 = 
                                                 (pt; p0).1 =>
                                               ((ap f r0 ..1)^)^ @ 1 =
                                               (ap f p1)^)
                                              (internal_paths_rew_r
                                                 (fun
                                                 p1 : 
                                                 f
                                                 (ispointed_fiber
                                                 {|
                                                 pointed_fun := f;
                                                 dpoint_eq := 1
                                                 |}).1 = 
                                                 f (pt; p0).1 =>
                                                 ((ap f r0 ..1)^)^ @ 1 = p1^)
                                                 (internal_paths_rew_r
                                                 (fun p1 : f pt = f point0 =>
                                                 p1 @ 1 =
                                                 ((ap f
                                                 (ap
                                                 (fun
                                                 x1 : hfiber f (f point0) =>
                                                 x1.1) r0))^)^)
                                                 (internal_paths_rew_r
                                                 (fun p1 : f pt = f point0 =>
                                                 ap f r0 ..1 @ 1 = p1)
                                                 (concat_p1
                                                 (ap f
                                                 (ap
                                                 (fun
                                                 x1 : hfiber f (f point0) =>
                                                 x1.1) r0)))
                                                 (inv_V
                                                 (ap f
                                                 (ap
                                                 (fun
                                                 x1 : hfiber f (f point0) =>
                                                 x1.1) r0))))
                                                 (inv_V (ap f r0 ..1)))
                                                 (ap_V f
                                                 (ap
                                                 (fun
                                                 x1 : hfiber f (f point0) =>
                                                 x1.1) r0)))
                                              (ap_V
                                                 (fun
                                                 x1 : hfiber f (f point0) =>
                                                 x1.1) r0))
                                           (ap_V f
                                              (ap
                                                 (fun
                                                 x1 : hfiber f (f point0) =>
                                                 x1.1) r0^)))
                                        (ap_V f r0 ..1))
                                     (pr1_path_V r0)
                                   :
                                   (ap f (r0^) ..1)^ @ pt.2 =
                                   ap f
                                     (ap
                                        (fun x1 : hfiber f (f point0) => x1.1)
                                        r0^)^)
                                  (transport_paths_Fl (r0^) ..1 pt.2))
                               (ap_V (fun x1 : hfiber f (f point0) => x1.1)
                                  r0^))
                            (inv_V
                               (ap (fun x1 : hfiber f (f point0) => x1.1)
                                  (r0^)^)))
                         (concat_p1
                            (ap (fun x1 : hfiber f (f point0) => x1.1) (r0^)^)^))
                      (transport_paths_Fl (r0^)^ 1))
                   (transport_arrow_toconst r0^ idmap 1))
                (paths_ind_r_transport
                   (fun b : hfiber f (f point0) =>
                    b.1 = point0 -> point0 = point0)
                   r0 idmap))
             (concat_p1
                (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; p0) r0 1)^)))
          (concat_1p
             (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; p0) r0 1)^ @
              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
              (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; p0) r0 1)^ @
         1))
       x q p r
     :
     (Build_pMap
        (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 (fun p0 : point0 = point0 => 1 @ (ap f p0 @ 1)) 1
      o* (Build_pMap inverse 1
          o* Build_pMap
               (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))
      proj0.1 proj0.2)
     proj1.1 proj1.2)
    x0.1 x0.2)
 :
 Build_pMap
   (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 (fun p : point0 = point0 => 1 @ (ap f p @ 1)) 1
 o* (Build_pMap inverse 1
     o* Build_pMap
          (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
     (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 (fun p : point0 = point0 => 1 @ (ap f p @ 1)) 1
    o* (Build_pMap inverse 1
        o* Build_pMap
             (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.

(** 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).
D: Type
x, y, z: D
p: x = y
q: y = z
(p^ @ 1) @ (((1 @ (1 @ p)^)^ @ q) @ 1) = 1 @ (q @ 1)
Proof.
D: Type
x, y, z: D
p: x = y
q: y = z
(p^ @ 1) @ (((1 @ (1 @ p)^)^ @ q) @ 1) = 1 @ (q @ 1)
  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.
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.
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
  pointed_reduce.
A: Type
point2: IsPointed A
B, C, D: Type
f: A -> B
g: C -> D
k: B -> D
h: A -> C
dpoint_eq1: g (h point2) = k (f point2)
p: forall x : A, k (f x) = g (h x)
H: p point2 = (ap k 1 @ 1) @ (ap g 1 @ dpoint_eq1)^
pfiber2_loops {| pointed_fun := g; dpoint_eq := dpoint_eq1 |}
o* functor_pfiber
     (square_functor_pfiber {| pointed_fun := p; dpoint_eq := H |}) ==*
Build_pMap (fun p0 : f point2 = f point2 => 1 @ (ap k p0 @ 1)) 1
o* Build_pMap
     (fun H0 : hfiber pr1 point2 =>
      paths_ind_r point2
        (fun (y : A) (_ : y = point2) =>
         f y = f point2 -> f point2 = f point2)
        idmap (H0.1).1 H0.2 (H0.1).2)
     1
  cbn in H.
A: Type
point2: IsPointed A
B, C, D: Type
f: A -> B
g: C -> D
k: B -> D
h: A -> C
dpoint_eq1: g (h point2) = k (f point2)
p: forall x : A, k (f x) = g (h x)
H: p point2 = 1 @ (1 @ dpoint_eq1)^
pfiber2_loops {| pointed_fun := g; dpoint_eq := dpoint_eq1 |}
o* functor_pfiber
     (square_functor_pfiber {| pointed_fun := p; dpoint_eq := H |}) ==*
Build_pMap (fun p0 : f point2 = f point2 => 1 @ (ap k p0 @ 1)) 1
o* Build_pMap
     (fun H0 : hfiber pr1 point2 =>
      paths_ind_r point2
        (fun (y : A) (_ : y = point2) =>
         f y = f point2 -> f point2 = f point2)
        idmap (H0.1).1 H0.2 (H0.1).2)
     1
  snapply Build_pHomotopy.
A: Type
point2: IsPointed A
B, C, D: Type
f: A -> B
g: C -> D
k: B -> D
h: A -> C
dpoint_eq1: g (h point2) = k (f point2)
p: forall x : A, k (f x) = g (h x)
H: p point2 = 1 @ (1 @ dpoint_eq1)^
pfiber2_loops {| pointed_fun := g; dpoint_eq := dpoint_eq1 |}
o* functor_pfiber
     (square_functor_pfiber {| pointed_fun := p; dpoint_eq := H |}) ==
Build_pMap (fun p0 : f point2 = f point2 => 1 @ (ap k p0 @ 1)) 1
o* Build_pMap
     (fun H0 : hfiber pr1 point2 =>
      paths_ind_r point2
        (fun (y : A) (_ : y = point2) =>
         f y = f point2 -> f point2 = f point2)
        idmap (H0.1).1 H0.2 (H0.1).2)
     1
A: Type
point2: IsPointed A
B, C, D: Type
f: A -> B
g: C -> D
k: B -> D
h: A -> C
dpoint_eq1: g (h point2) = k (f point2)
p: forall x : A, k (f x) = g (h x)
H: p point2 = 1 @ (1 @ dpoint_eq1)^
?p pt =
dpoint_eq
  (pfiber2_loops {| pointed_fun := g; dpoint_eq := dpoint_eq1 |}
   o* functor_pfiber
        (square_functor_pfiber {| pointed_fun := p; dpoint_eq := H |})) @
(dpoint_eq
   (Build_pMap (fun p0 : f point2 = f point2 => 1 @ (ap k p0 @ 1)) 1
    o* Build_pMap
         (fun H0 : hfiber pr1 point2 =>
          paths_ind_r point2
            (fun (y : A) (_ : y = point2) =>
             f y = f point2 -> f point2 = f point2)
            idmap (H0.1).1 H0.2 (H0.1).2)
         1))^
  -
A: Type
point2: IsPointed A
B, C, D: Type
f: A -> B
g: C -> D
k: B -> D
h: A -> C
dpoint_eq1: g (h point2) = k (f point2)
p: forall x : A, k (f x) = g (h x)
H: p point2 = 1 @ (1 @ dpoint_eq1)^
pfiber2_loops {| pointed_fun := g; dpoint_eq := dpoint_eq1 |}
o* functor_pfiber
     (square_functor_pfiber {| pointed_fun := p; dpoint_eq := H |}) ==
Build_pMap (fun p0 : f point2 = f point2 => 1 @ (ap k p0 @ 1)) 1
o* Build_pMap
     (fun H0 : hfiber pr1 point2 =>
      paths_ind_r point2
        (fun (y : A) (_ : y = point2) =>
         f y = f point2 -> f point2 = f point2)
        idmap (H0.1).1 H0.2 (H0.1).2)
     1 intros [[c w] v].
A: Type
point2: IsPointed A
B, C, D: Type
f: A -> B
g: C -> D
k: B -> D
h: A -> C
dpoint_eq1: g (h point2) = k (f point2)
p: forall x : A, k (f x) = g (h x)
H: p point2 = 1 @ (1 @ dpoint_eq1)^
c: [A, point2]
w: {| pointed_fun := f; dpoint_eq := 1 |} c = pt
v: pfib {| pointed_fun := f; dpoint_eq := 1 |} (c; w) = pt
(pfiber2_loops {| pointed_fun := g; dpoint_eq := dpoint_eq1 |}
 o* functor_pfiber
      (square_functor_pfiber {| pointed_fun := p; dpoint_eq := H |}))
  ((c; w); v) =
(Build_pMap (fun p0 : f point2 = f point2 => 1 @ (ap k p0 @ 1)) 1
 o* Build_pMap
      (fun H0 : hfiber pr1 point2 =>
       paths_ind_r point2
         (fun (y : A) (_ : y = point2) =>
          f y = f point2 -> f point2 = f point2)
         idmap (H0.1).1 H0.2 (H0.1).2)
      1)
  ((c; w); v)
    cbn in c, w, v.
A: Type
point2: IsPointed A
B, C, D: Type
f: A -> B
g: C -> D
k: B -> D
h: A -> C
dpoint_eq1: g (h point2) = k (f point2)
p: forall x : A, k (f x) = g (h x)
H: p point2 = 1 @ (1 @ dpoint_eq1)^
c: A
w: f c = f point2
v: c = point2
(pfiber2_loops {| pointed_fun := g; dpoint_eq := dpoint_eq1 |}
 o* functor_pfiber
      (square_functor_pfiber {| pointed_fun := p; dpoint_eq := H |}))
  ((c; w); v) =
(Build_pMap (fun p0 : f point2 = f point2 => 1 @ (ap k p0 @ 1)) 1
 o* Build_pMap
      (fun H0 : hfiber pr1 point2 =>
       paths_ind_r point2
         (fun (y : A) (_ : y = point2) =>
          f y = f point2 -> f point2 = f point2)
         idmap (H0.1).1 H0.2 (H0.1).2)
      1)
  ((c; w); v)
    destruct v.
A, B, C, D: Type
f: A -> B
g: C -> D
k: B -> D
h: A -> C
c: A
w: f c = f c
dpoint_eq1: g (h c) = k (f c)
p: forall x : A, k (f x) = g (h x)
H: p c = 1 @ (1 @ dpoint_eq1)^
(pfiber2_loops {| pointed_fun := g; dpoint_eq := dpoint_eq1 |}
 o* functor_pfiber
      (square_functor_pfiber {| pointed_fun := p; dpoint_eq := H |}))
  ((c; w); 1) =
(Build_pMap (fun p0 : f c = f c => 1 @ (ap k p0 @ 1)) 1
 o* Build_pMap
      (fun H0 : hfiber pr1 c =>
       paths_ind_r c (fun (y : A) (_ : y = c) => f y = f c -> f c = f c)
         idmap (H0.1).1 H0.2 (H0.1).2)
      1)
  ((c; w); 1)
    lhs napply pfiber2_loops_beta.
A, B, C, D: Type
f: A -> B
g: C -> D
k: B -> D
h: A -> C
c: A
w: f c = f c
dpoint_eq1: g (h c) = k (f c)
p: forall x : A, k (f x) = g (h x)
H: p c = 1 @ (1 @ dpoint_eq1)^
((point_eq {| pointed_fun := g; dpoint_eq := dpoint_eq1 |})^ @
 (ap {| pointed_fun := g; dpoint_eq := dpoint_eq1 |}
    (((square_functor_pfiber {| pointed_fun := p; dpoint_eq := H |}
         ((c; w); 1).1)^ @
      ap {| pointed_fun := h; dpoint_eq := 1 |} ((c; w); 1).2) @
     point_eq {| pointed_fun := h; dpoint_eq := 1 |}))^) @
((({| pointed_fun := p; dpoint_eq := H |} (((c; w); 1).1).1)^ @
  ap {| pointed_fun := k; dpoint_eq := 1 |} (((c; w); 1).1).2) @
 point_eq {| pointed_fun := k; dpoint_eq := 1 |}) =
(Build_pMap (fun p0 : f c = f c => 1 @ (ap k p0 @ 1)) 1
 o* Build_pMap
      (fun H0 : hfiber pr1 c =>
       paths_ind_r c (fun (y : A) (_ : y = c) => f y = f c -> f c = f c)
         idmap (H0.1).1 H0.2 (H0.1).2)
      1)
  ((c; w); 1)
    cbn.
A, B, C, D: Type
f: A -> B
g: C -> D
k: B -> D
h: A -> C
c: A
w: f c = f c
dpoint_eq1: g (h c) = k (f c)
p: forall x : A, k (f x) = g (h x)
H: p c = 1 @ (1 @ dpoint_eq1)^
(dpoint_eq1^ @ 1) @ (((p c)^ @ ap k w) @ 1) = 1 @ (ap k w @ 1)
    destruct H^; clear H p.
A, B, C, D: Type
f: A -> B
g: C -> D
k: B -> D
h: A -> C
c: A
w: f c = f c
dpoint_eq1: g (h c) = k (f c)
(dpoint_eq1^ @ 1) @ (((1 @ (1 @ dpoint_eq1)^)^ @ ap k w) @ 1) =
1 @ (ap k w @ 1)
    exact (pfiber2_loops_natural_functor_helper dpoint_eq1 (ap k w)).
  -
A: Type
point2: IsPointed A
B, C, D: Type
f: A -> B
g: C -> D
k: B -> D
h: A -> C
dpoint_eq1: g (h point2) = k (f point2)
p: forall x : A, k (f x) = g (h x)
H: p point2 = 1 @ (1 @ dpoint_eq1)^
((fun x : pfiber (pfib {| pointed_fun := f; dpoint_eq := 1 |}) =>
  (fun proj1 : pfiber {| pointed_fun := f; dpoint_eq := 1 |} =>
   (fun (c : [A, point2]) (w : {| pointed_fun := f; dpoint_eq := 1 |} c = pt)
      (v : pfib {| pointed_fun := f; dpoint_eq := 1 |} (c; w) = pt) =>
    match
      v as p0 in (_ = a)
      return
        (forall (dpoint_eq0 : g (h a) = k (f a))
         (H0 : p a = 1 @ (1 @ dpoint_eq0)^) (w0 : f c = f a),
         (pfiber2_loops {| pointed_fun := g; dpoint_eq := dpoint_eq0 |}
          o* functor_pfiber
               (square_functor_pfiber {| pointed_fun := p; dpoint_eq := H0 |}))
           ((c; w0); p0) =
         (Build_pMap (fun p1 : f a = f a => 1 @ (ap k p1 @ 1)) 1
          o* Build_pMap
               (fun H1 : hfiber pr1 a =>
                paths_ind_r a
                  (fun (y : A) (_ : y = a) => f y = f a -> f a = f a) idmap
                  (H1.1).1 H1.2 (H1.1).2)
               1)
           ((c; w0); p0))
    with
    | 1 =>
        fun (dpoint_eq0 : g (h c) = k (f c))
          (H0 : p c = 1 @ (1 @ dpoint_eq0)^) (w0 : f c = f c) =>
        pfiber2_loops_beta {| pointed_fun := g; dpoint_eq := dpoint_eq0 |}
          ({| pointed_fun := h; dpoint_eq := 1 |} (((c; w0); 1).1).1)
          ((({| pointed_fun := p; dpoint_eq := H0 |} (((c; w0); 1).1).1)^ @
            ap {| pointed_fun := k; dpoint_eq := 1 |} (((c; w0); 1).1).2) @
           point_eq {| pointed_fun := k; dpoint_eq := 1 |})
          (((square_functor_pfiber {| pointed_fun := p; dpoint_eq := H0 |}
               ((c; w0); 1).1)^ @
            ap {| pointed_fun := h; dpoint_eq := 1 |} ((c; w0); 1).2) @
           point_eq {| pointed_fun := h; dpoint_eq := 1 |}) @
        ((let p0 := H0^ in
          let p1 := p c in
          match
            p0 in (_ = p2)
            return
              (p2 = 1 @ (1 @ dpoint_eq0)^ ->
               (dpoint_eq0^ @ 1) @ ((p2^ @ ap k w0) @ 1) = 1 @ (ap k w0 @ 1))
          with
          | 1 =>
              fun _ : 1 @ (1 @ dpoint_eq0)^ = 1 @ (1 @ dpoint_eq0)^ =>
              pfiber2_loops_natural_functor_helper dpoint_eq0 (ap k w0)
          end H0)
         :
         ((point_eq {| pointed_fun := g; dpoint_eq := dpoint_eq0 |})^ @
          (ap {| pointed_fun := g; dpoint_eq := dpoint_eq0 |}
             (((square_functor_pfiber {| pointed_fun := p; dpoint_eq := H0 |}
                  ((c; w0); 1).1)^ @
               ap {| pointed_fun := h; dpoint_eq := 1 |} ((c; w0); 1).2) @
              point_eq {| pointed_fun := h; dpoint_eq := 1 |}))^) @
         ((({| pointed_fun := p; dpoint_eq := H0 |} (((c; w0); 1).1).1)^ @
           ap {| pointed_fun := k; dpoint_eq := 1 |} (((c; w0); 1).1).2) @
          point_eq {| pointed_fun := k; dpoint_eq := 1 |}) =
         (Build_pMap (fun p0 : f c = f c => 1 @ (ap k p0 @ 1)) 1
          o* Build_pMap
               (fun H1 : hfiber pr1 c =>
                paths_ind_r c
                  (fun (y : A) (_ : y = c) => f y = f c -> f c = f c) idmap
                  (H1.1).1 H1.2 (H1.1).2)
               1)
           ((c; w0); 1))
    end dpoint_eq1 H w) proj1.1 proj1.2) x.1 x.2)
 :
 pfiber2_loops {| pointed_fun := g; dpoint_eq := dpoint_eq1 |}
 o* functor_pfiber
      (square_functor_pfiber {| pointed_fun := p; dpoint_eq := H |}) ==
 Build_pMap (fun p0 : f point2 = f point2 => 1 @ (ap k p0 @ 1)) 1
 o* Build_pMap
      (fun H0 : hfiber pr1 point2 =>
       paths_ind_r point2
         (fun (y : A) (_ : y = point2) =>
          f y = f point2 -> f point2 = f point2)
         idmap (H0.1).1 H0.2 (H0.1).2)
      1)
  pt =
dpoint_eq
  (pfiber2_loops {| pointed_fun := g; dpoint_eq := dpoint_eq1 |}
   o* functor_pfiber
        (square_functor_pfiber {| pointed_fun := p; dpoint_eq := H |})) @
(dpoint_eq
   (Build_pMap (fun p0 : f point2 = f point2 => 1 @ (ap k p0 @ 1)) 1
    o* Build_pMap
         (fun H0 : hfiber pr1 point2 =>
          paths_ind_r point2
            (fun (y : A) (_ : y = point2) =>
             f y = f point2 -> f point2 = f point2)
            idmap (H0.1).1 H0.2 (H0.1).2)
         1))^ cbn; cbv delta
      [point_htpy square_functor_pfiber
       functor_hfiber2 functor_sigma
       functor_pfiber];
    cbn.
A: Type
point2: IsPointed A
B, C, D: Type
f: A -> B
g: C -> D
k: B -> D
h: A -> C
dpoint_eq1: g (h point2) = k (f point2)
p: forall x : A, k (f x) = g (h x)
H: p point2 = 1 @ (1 @ dpoint_eq1)^
pfiber2_loops_beta {| pointed_fun := g; dpoint_eq := dpoint_eq1 |} 
  (h point2) (((p point2)^ @ 1) @ 1) 1 @
match
  H^ in (_ = p0)
  return
    (p0 = 1 @ (1 @ dpoint_eq1)^ -> (dpoint_eq1^ @ 1) @ ((p0^ @ 1) @ 1) = 1)
with
| 1 =>
    fun _ : 1 @ (1 @ dpoint_eq1)^ = 1 @ (1 @ dpoint_eq1)^ =>
    pfiber2_loops_natural_functor_helper dpoint_eq1 1
end H =
(ap (pfiber2_loops {| pointed_fun := g; dpoint_eq := dpoint_eq1 |})
   (path_sigma' (fun x : hfiber g (k (f point2)) => x.1 = h point2)
      (path_sigma' (fun x : C => g x = k (f point2)) 1
         (match
            ((p point2)^ @ 1) @ 1 as p0 in (_ = b) return (p0 = 1 @ p0)
          with
          | 1 => 1
          end @
          (whiskerL 1
             match
               (p point2)^ as p0 in (_ = a) return ((p0 @ 1) @ 1 = p0 @ 1)
             with
             | 1 => 1
             end @
           (whiskerL 1
              (whiskerL (p point2)^
                 (moveR_pM (1 @ dpoint_eq1) 1 (p point2) H)^) @
            (whiskerL 1 (concat_V_pp (p point2) (1 @ dpoint_eq1)) @
             concat_V_pp 1 dpoint_eq1)))))
      (transport_paths_Fl
         (path_sigma' (fun x : C => g x = k (f point2)) 1
            (match
               ((p point2)^ @ 1) @ 1 as p0 in (_ = b) return (p0 = 1 @ p0)
             with
             | 1 => 1
             end @
             (whiskerL 1
                match
                  (p point2)^ as p0 in (_ = a) return ((p0 @ 1) @ 1 = p0 @ 1)
                with
                | 1 => 1
                end @
              (whiskerL 1
                 (whiskerL (p point2)^
                    (moveR_pM (1 @ dpoint_eq1) 1 (p point2) H)^) @
               (whiskerL 1 (concat_V_pp (p point2) (1 @ dpoint_eq1)) @
                concat_V_pp 1 dpoint_eq1)))))
         1 @
       (1 @
        (whiskerL
           (ap pr1
              (path_sigma' (fun x : C => g x = k (f point2)) 1
                 (match
                    ((p point2)^ @ 1) @ 1 as p0 in (_ = b)
                    return (p0 = 1 @ p0)
                  with
                  | 1 => 1
                  end @
                  (whiskerL 1
                     match
                       (p point2)^ as p0 in (_ = a)
                       return ((p0 @ 1) @ 1 = p0 @ 1)
                     with
                     | 1 => 1
                     end @
                   (whiskerL 1
                      (whiskerL (p point2)^
                         (moveR_pM (1 @ dpoint_eq1) 1 (p point2) H)^) @
                    (whiskerL 1 (concat_V_pp (p point2) (1 @ dpoint_eq1)) @
                     concat_V_pp 1 dpoint_eq1))))))^
           (whiskerL 1
              (moveR_pM
                 (ap pr1
                    (path_sigma' (fun x : C => g x = k (f point2)) 1
                       (match
                          ((p point2)^ @ 1) @ 1 as p0 in (_ = b)
                          return (p0 = 1 @ p0)
                        with
                        | 1 => 1
                        end @
                        (whiskerL 1
                           match
                             (p point2)^ as p0 in (_ = a)
                             return ((p0 @ 1) @ 1 = p0 @ 1)
                           with
                           | 1 => 1
                           end @
                         (whiskerL 1
                            (whiskerL (p point2)^
                               (moveR_pM (1 @ dpoint_eq1) 1 (p point2) H)^) @
                          (whiskerL 1
                             (concat_V_pp (p point2) (1 @ dpoint_eq1)) @
                           concat_V_pp 1 dpoint_eq1))))) @
                  1)
                 1 1
                 (moveL_pV
                    (ap pr1
                       (path_sigma' (fun x : C => g x = k (f point2)) 1
                          (match
                             ((p point2)^ @ 1) @ 1 as p0 in (_ = b)
                             return (p0 = 1 @ p0)
                           with
                           | 1 => 1
                           end @
                           (whiskerL 1
                              match
                                (p point2)^ as p0 in (_ = a)
                                return ((p0 @ 1) @ 1 = p0 @ 1)
                              with
                              | 1 => 1
                              end @
                            (whiskerL 1
                               (whiskerL (p point2)^
                                  (moveR_pM (1 @ dpoint_eq1) 1 (p point2) H)^) @
                             (whiskerL 1
                                (concat_V_pp (p point2) (1 @ dpoint_eq1)) @
                              concat_V_pp 1 dpoint_eq1))))) @
                     1)
                    1 1
                    (1 @@
                     (concat_p1
                        (ap pr1
                           (path_sigma' (fun x : C => g x = k (f point2)) 1
                              (match
                                 ((p point2)^ @ 1) @ 1 as p0 in (_ = b)
                                 return (p0 = 1 @ p0)
                               with
                               | 1 => 1
                               end @
                               (whiskerL 1
                                  match
                                    (p point2)^ as p0 in (_ = a)
                                    return ((p0 @ 1) @ 1 = p0 @ 1)
                                  with
                                  | 1 => 1
                                  end @
                                (whiskerL 1
                                   (whiskerL (p point2)^
                                      (moveR_pM (1 @ dpoint_eq1) 1 
                                         (p point2) H)^) @
                                 (whiskerL 1
                                    (concat_V_pp (p point2) (1 @ dpoint_eq1)) @
                                  concat_V_pp 1 dpoint_eq1)))))) @
                      match
                        match
                          ((p point2)^ @ 1) @ 1 as p0 in (_ = b)
                          return (p0 = 1 @ p0)
                        with
                        | 1 => 1
                        end @
                        (whiskerL 1
                           match
                             (p point2)^ as p0 in (_ = a)
                             return ((p0 @ 1) @ 1 = p0 @ 1)
                           with
                           | 1 => 1
                           end @
                         (whiskerL 1
                            (whiskerL (p point2)^
                               (moveR_pM (1 @ dpoint_eq1) 1 (p point2) H)^) @
                          (whiskerL 1
                             (concat_V_pp (p point2) (1 @ dpoint_eq1)) @
                           concat_V_pp 1 dpoint_eq1)))
                        as p1 in (_ = p0)
                        return
                          ((path_sigma_uncurried
                              (fun x : C => g x = k (f point2))
                              (h point2; ((p point2)^ @ 1) @ 1)
                              (h point2; p0) (1; p1))
                           ..1 = 1)
                      with
                      | 1 => 1
                      end))))^) @
         (whiskerL
            (ap pr1
               (path_sigma' (fun x : C => g x = k (f point2)) 1
                  (match
                     ((p point2)^ @ 1) @ 1 as p0 in (_ = b)
                     return (p0 = 1 @ p0)
                   with
                   | 1 => 1
                   end @
                   (whiskerL 1
                      match
                        (p point2)^ as p0 in (_ = a)
                        return ((p0 @ 1) @ 1 = p0 @ 1)
                      with
                      | 1 => 1
                      end @
                    (whiskerL 1
                       (whiskerL (p point2)^
                          (moveR_pM (1 @ dpoint_eq1) 1 (p point2) H)^) @
                     (whiskerL 1 (concat_V_pp (p point2) (1 @ dpoint_eq1)) @
                      concat_V_pp 1 dpoint_eq1))))))^
            (concat_V_pp 1
               (ap pr1
                  (path_sigma' (fun x : C => g x = k (f point2)) 1
                     (match
                        ((p point2)^ @ 1) @ 1 as p0 in (_ = b)
                        return (p0 = 1 @ p0)
                      with
                      | 1 => 1
                      end @
                      (whiskerL 1
                         match
                           (p point2)^ as p0 in (_ = a)
                           return ((p0 @ 1) @ 1 = p0 @ 1)
                         with
                         | 1 => 1
                         end @
                       (whiskerL 1
                          (whiskerL (p point2)^
                             (moveR_pM (1 @ dpoint_eq1) 1 (p point2) H)^) @
                        (whiskerL 1 (concat_V_pp (p point2) (1 @ dpoint_eq1)) @
                         concat_V_pp 1 dpoint_eq1))))) @
                1)) @
          match
            ap pr1
              (path_sigma' (fun x : C => g x = k (f point2)) 1
                 (match
                    ((p point2)^ @ 1) @ 1 as p0 in (_ = b)
                    return (p0 = 1 @ p0)
                  with
                  | 1 => 1
                  end @
                  (whiskerL 1
                     match
                       (p point2)^ as p0 in (_ = a)
                       return ((p0 @ 1) @ 1 = p0 @ 1)
                     with
                     | 1 => 1
                     end @
                   (whiskerL 1
                      (whiskerL (p point2)^
                         (moveR_pM (1 @ dpoint_eq1) 1 (p point2) H)^) @
                    (whiskerL 1 (concat_V_pp (p point2) (1 @ dpoint_eq1)) @
                     concat_V_pp 1 dpoint_eq1)))))
            as p0 in (_ = a) return (p0^ @ (p0 @ 1) = 1)
          with
          | 1 => 1
          end))))) @
 point_eq (pfiber2_loops {| pointed_fun := g; dpoint_eq := dpoint_eq1 |})) @
1
    (* The next two lines are essentially [destruct H^], with [H] also replaced by [idpath]. *)
    generalize dependent (p point2).
A: Type
point2: IsPointed A
B, C, D: Type
f: A -> B
g: C -> D
k: B -> D
h: A -> C
dpoint_eq1: g (h point2) = k (f point2)
p: forall x : A, k (f x) = g (h x)
forall (p0 : k (f point2) = g (h point2)) (H : p0 = 1 @ (1 @ dpoint_eq1)^),
pfiber2_loops_beta {| pointed_fun := g; dpoint_eq := dpoint_eq1 |} 
  (h point2) ((p0^ @ 1) @ 1) 1 @
match
  H^ in (_ = p1)
  return
    (p1 = 1 @ (1 @ dpoint_eq1)^ -> (dpoint_eq1^ @ 1) @ ((p1^ @ 1) @ 1) = 1)
with
| 1 =>
    fun _ : 1 @ (1 @ dpoint_eq1)^ = 1 @ (1 @ dpoint_eq1)^ =>
    pfiber2_loops_natural_functor_helper dpoint_eq1 1
end H =
(ap (pfiber2_loops {| pointed_fun := g; dpoint_eq := dpoint_eq1 |})
   (path_sigma' (fun x : hfiber g (k (f point2)) => x.1 = h point2)
      (path_sigma' (fun x : C => g x = k (f point2)) 1
         (match (p0^ @ 1) @ 1 as p1 in (_ = b) return (p1 = 1 @ p1) with
          | 1 => 1
          end @
          (whiskerL 1
             match p0^ as p1 in (_ = a) return ((p1 @ 1) @ 1 = p1 @ 1) with
             | 1 => 1
             end @
           (whiskerL 1 (whiskerL p0^ (moveR_pM (1 @ dpoint_eq1) 1 p0 H)^) @
            (whiskerL 1 (concat_V_pp p0 (1 @ dpoint_eq1)) @
             concat_V_pp 1 dpoint_eq1)))))
      (transport_paths_Fl
         (path_sigma' (fun x : C => g x = k (f point2)) 1
            (match (p0^ @ 1) @ 1 as p1 in (_ = b) return (p1 = 1 @ p1) with
             | 1 => 1
             end @
             (whiskerL 1
                match
                  p0^ as p1 in (_ = a) return ((p1 @ 1) @ 1 = p1 @ 1)
                with
                | 1 => 1
                end @
              (whiskerL 1 (whiskerL p0^ (moveR_pM (1 @ dpoint_eq1) 1 p0 H)^) @
               (whiskerL 1 (concat_V_pp p0 (1 @ dpoint_eq1)) @
                concat_V_pp 1 dpoint_eq1)))))
         1 @
       (1 @
        (whiskerL
           (ap pr1
              (path_sigma' (fun x : C => g x = k (f point2)) 1
                 (match
                    (p0^ @ 1) @ 1 as p1 in (_ = b) return (p1 = 1 @ p1)
                  with
                  | 1 => 1
                  end @
                  (whiskerL 1
                     match
                       p0^ as p1 in (_ = a) return ((p1 @ 1) @ 1 = p1 @ 1)
                     with
                     | 1 => 1
                     end @
                   (whiskerL 1
                      (whiskerL p0^ (moveR_pM (1 @ dpoint_eq1) 1 p0 H)^) @
                    (whiskerL 1 (concat_V_pp p0 (1 @ dpoint_eq1)) @
                     concat_V_pp 1 dpoint_eq1))))))^
           (whiskerL 1
              (moveR_pM
                 (ap pr1
                    (path_sigma' (fun x : C => g x = k (f point2)) 1
                       (match
                          (p0^ @ 1) @ 1 as p1 in (_ = b) return (p1 = 1 @ p1)
                        with
                        | 1 => 1
                        end @
                        (whiskerL 1
                           match
                             p0^ as p1 in (_ = a)
                             return ((p1 @ 1) @ 1 = p1 @ 1)
                           with
                           | 1 => 1
                           end @
                         (whiskerL 1
                            (whiskerL p0^ (moveR_pM (1 @ dpoint_eq1) 1 p0 H)^) @
                          (whiskerL 1 (concat_V_pp p0 (1 @ dpoint_eq1)) @
                           concat_V_pp 1 dpoint_eq1))))) @
                  1)
                 1 1
                 (moveL_pV
                    (ap pr1
                       (path_sigma' (fun x : C => g x = k (f point2)) 1
                          (match
                             (p0^ @ 1) @ 1 as p1 in (_ = b)
                             return (p1 = 1 @ p1)
                           with
                           | 1 => 1
                           end @
                           (whiskerL 1
                              match
                                p0^ as p1 in (_ = a)
                                return ((p1 @ 1) @ 1 = p1 @ 1)
                              with
                              | 1 => 1
                              end @
                            (whiskerL 1
                               (whiskerL p0^
                                  (moveR_pM (1 @ dpoint_eq1) 1 p0 H)^) @
                             (whiskerL 1 (concat_V_pp p0 (1 @ dpoint_eq1)) @
                              concat_V_pp 1 dpoint_eq1))))) @
                     1)
                    1 1
                    (1 @@
                     (concat_p1
                        (ap pr1
                           (path_sigma' (fun x : C => g x = k (f point2)) 1
                              (match
                                 (p0^ @ 1) @ 1 as p1 in (_ = b)
                                 return (p1 = 1 @ p1)
                               with
                               | 1 => 1
                               end @
                               (whiskerL 1
                                  match
                                    p0^ as p1 in (_ = a)
                                    return ((p1 @ 1) @ 1 = p1 @ 1)
                                  with
                                  | 1 => 1
                                  end @
                                (whiskerL 1
                                   (whiskerL p0^
                                      (moveR_pM (1 @ dpoint_eq1) 1 p0 H)^) @
                                 (whiskerL 1
                                    (concat_V_pp p0 (1 @ dpoint_eq1)) @
                                  concat_V_pp 1 dpoint_eq1)))))) @
                      match
                        match
                          (p0^ @ 1) @ 1 as p1 in (_ = b) return (p1 = 1 @ p1)
                        with
                        | 1 => 1
                        end @
                        (whiskerL 1
                           match
                             p0^ as p1 in (_ = a)
                             return ((p1 @ 1) @ 1 = p1 @ 1)
                           with
                           | 1 => 1
                           end @
                         (whiskerL 1
                            (whiskerL p0^ (moveR_pM (1 @ dpoint_eq1) 1 p0 H)^) @
                          (whiskerL 1 (concat_V_pp p0 (1 @ dpoint_eq1)) @
                           concat_V_pp 1 dpoint_eq1)))
                        as p2 in (_ = p1)
                        return
                          ((path_sigma_uncurried
                              (fun x : C => g x = k (f point2))
                              (h point2; (p0^ @ 1) @ 1) 
                              (h point2; p1) (1; p2))
                           ..1 = 1)
                      with
                      | 1 => 1
                      end))))^) @
         (whiskerL
            (ap pr1
               (path_sigma' (fun x : C => g x = k (f point2)) 1
                  (match
                     (p0^ @ 1) @ 1 as p1 in (_ = b) return (p1 = 1 @ p1)
                   with
                   | 1 => 1
                   end @
                   (whiskerL 1
                      match
                        p0^ as p1 in (_ = a) return ((p1 @ 1) @ 1 = p1 @ 1)
                      with
                      | 1 => 1
                      end @
                    (whiskerL 1
                       (whiskerL p0^ (moveR_pM (1 @ dpoint_eq1) 1 p0 H)^) @
                     (whiskerL 1 (concat_V_pp p0 (1 @ dpoint_eq1)) @
                      concat_V_pp 1 dpoint_eq1))))))^
            (concat_V_pp 1
               (ap pr1
                  (path_sigma' (fun x : C => g x = k (f point2)) 1
                     (match
                        (p0^ @ 1) @ 1 as p1 in (_ = b) return (p1 = 1 @ p1)
                      with
                      | 1 => 1
                      end @
                      (whiskerL 1
                         match
                           p0^ as p1 in (_ = a)
                           return ((p1 @ 1) @ 1 = p1 @ 1)
                         with
                         | 1 => 1
                         end @
                       (whiskerL 1
                          (whiskerL p0^ (moveR_pM (1 @ dpoint_eq1) 1 p0 H)^) @
                        (whiskerL 1 (concat_V_pp p0 (1 @ dpoint_eq1)) @
                         concat_V_pp 1 dpoint_eq1))))) @
                1)) @
          match
            ap pr1
              (path_sigma' (fun x : C => g x = k (f point2)) 1
                 (match
                    (p0^ @ 1) @ 1 as p1 in (_ = b) return (p1 = 1 @ p1)
                  with
                  | 1 => 1
                  end @
                  (whiskerL 1
                     match
                       p0^ as p1 in (_ = a) return ((p1 @ 1) @ 1 = p1 @ 1)
                     with
                     | 1 => 1
                     end @
                   (whiskerL 1
                      (whiskerL p0^ (moveR_pM (1 @ dpoint_eq1) 1 p0 H)^) @
                    (whiskerL 1 (concat_V_pp p0 (1 @ dpoint_eq1)) @
                     concat_V_pp 1 dpoint_eq1)))))
            as p1 in (_ = a) return (p1^ @ (p1 @ 1) = 1)
          with
          | 1 => 1
          end))))) @
 point_eq (pfiber2_loops {| pointed_fun := g; dpoint_eq := dpoint_eq1 |})) @
1
    napply paths_ind_r.
A: Type
point2: IsPointed A
B, C, D: Type
f: A -> B
g: C -> D
k: B -> D
h: A -> C
dpoint_eq1: g (h point2) = k (f point2)
p: forall x : A, k (f x) = g (h x)
pfiber2_loops_beta {| pointed_fun := g; dpoint_eq := dpoint_eq1 |} 
  (h point2) (((1 @ (1 @ dpoint_eq1)^)^ @ 1) @ 1) 1 @
match
  1^ in (_ = p0)
  return
    (p0 = 1 @ (1 @ dpoint_eq1)^ -> (dpoint_eq1^ @ 1) @ ((p0^ @ 1) @ 1) = 1)
with
| 1 =>
    fun _ : 1 @ (1 @ dpoint_eq1)^ = 1 @ (1 @ dpoint_eq1)^ =>
    pfiber2_loops_natural_functor_helper dpoint_eq1 1
end 1 =
(ap (pfiber2_loops {| pointed_fun := g; dpoint_eq := dpoint_eq1 |})
   (path_sigma' (fun x : hfiber g (k (f point2)) => x.1 = h point2)
      (path_sigma' (fun x : C => g x = k (f point2)) 1
         (match
            ((1 @ (1 @ dpoint_eq1)^)^ @ 1) @ 1 as p0 in (_ = b)
            return (p0 = 1 @ p0)
          with
          | 1 => 1
          end @
          (whiskerL 1
             match
               (1 @ (1 @ dpoint_eq1)^)^ as p0 in (_ = a)
               return ((p0 @ 1) @ 1 = p0 @ 1)
             with
             | 1 => 1
             end @
           (whiskerL 1
              (whiskerL (1 @ (1 @ dpoint_eq1)^)^
                 (moveR_pM (1 @ dpoint_eq1) 1 (1 @ (1 @ dpoint_eq1)^) 1)^) @
            (whiskerL 1
               (concat_V_pp (1 @ (1 @ dpoint_eq1)^) (1 @ dpoint_eq1)) @
             concat_V_pp 1 dpoint_eq1)))))
      (transport_paths_Fl
         (path_sigma' (fun x : C => g x = k (f point2)) 1
            (match
               ((1 @ (1 @ dpoint_eq1)^)^ @ 1) @ 1 as p0 in (_ = b)
               return (p0 = 1 @ p0)
             with
             | 1 => 1
             end @
             (whiskerL 1
                match
                  (1 @ (1 @ dpoint_eq1)^)^ as p0 in (_ = a)
                  return ((p0 @ 1) @ 1 = p0 @ 1)
                with
                | 1 => 1
                end @
              (whiskerL 1
                 (whiskerL (1 @ (1 @ dpoint_eq1)^)^
                    (moveR_pM (1 @ dpoint_eq1) 1 (1 @ (1 @ dpoint_eq1)^) 1)^) @
               (whiskerL 1
                  (concat_V_pp (1 @ (1 @ dpoint_eq1)^) (1 @ dpoint_eq1)) @
                concat_V_pp 1 dpoint_eq1)))))
         1 @
       (1 @
        (whiskerL
           (ap pr1
              (path_sigma' (fun x : C => g x = k (f point2)) 1
                 (match
                    ((1 @ (1 @ dpoint_eq1)^)^ @ 1) @ 1 as p0 in (_ = b)
                    return (p0 = 1 @ p0)
                  with
                  | 1 => 1
                  end @
                  (whiskerL 1
                     match
                       (1 @ (1 @ dpoint_eq1)^)^ as p0 in (_ = a)
                       return ((p0 @ 1) @ 1 = p0 @ 1)
                     with
                     | 1 => 1
                     end @
                   (whiskerL 1
                      (whiskerL (1 @ (1 @ dpoint_eq1)^)^
                         (moveR_pM (1 @ dpoint_eq1) 1 
                            (1 @ (1 @ dpoint_eq1)^) 1)^) @
                    (whiskerL 1
                       (concat_V_pp (1 @ (1 @ dpoint_eq1)^) (1 @ dpoint_eq1)) @
                     concat_V_pp 1 dpoint_eq1))))))^
           (whiskerL 1
              (moveR_pM
                 (ap pr1
                    (path_sigma' (fun x : C => g x = k (f point2)) 1
                       (match
                          ((1 @ (1 @ dpoint_eq1)^)^ @ 1) @ 1 as p0 in (_ = b)
                          return (p0 = 1 @ p0)
                        with
                        | 1 => 1
                        end @
                        (whiskerL 1
                           match
                             (1 @ (1 @ dpoint_eq1)^)^ as p0 in (_ = a)
                             return ((p0 @ 1) @ 1 = p0 @ 1)
                           with
                           | 1 => 1
                           end @
                         (whiskerL 1
                            (whiskerL (1 @ (1 @ dpoint_eq1)^)^
                               (moveR_pM (1 @ dpoint_eq1) 1
                                  (1 @ (1 @ dpoint_eq1)^) 1)^) @
                          (whiskerL 1
                             (concat_V_pp (1 @ (1 @ dpoint_eq1)^)
                                (1 @ dpoint_eq1)) @
                           concat_V_pp 1 dpoint_eq1))))) @
                  1)
                 1 1
                 (moveL_pV
                    (ap pr1
                       (path_sigma' (fun x : C => g x = k (f point2)) 1
                          (match
                             ((1 @ (1 @ dpoint_eq1)^)^ @ 1) @ 1 as p0 in
                             (_ = b) return (p0 = 1 @ p0)
                           with
                           | 1 => 1
                           end @
                           (whiskerL 1
                              match
                                (1 @ (1 @ dpoint_eq1)^)^ as p0 in (_ = a)
                                return ((p0 @ 1) @ 1 = p0 @ 1)
                              with
                              | 1 => 1
                              end @
                            (whiskerL 1
                               (whiskerL (1 @ (1 @ dpoint_eq1)^)^
                                  (moveR_pM (1 @ dpoint_eq1) 1
                                     (1 @ (1 @ dpoint_eq1)^) 1)^) @
                             (whiskerL 1
                                (concat_V_pp (1 @ (1 @ dpoint_eq1)^)
                                   (1 @ dpoint_eq1)) @
                              concat_V_pp 1 dpoint_eq1))))) @
                     1)
                    1 1
                    (1 @@
                     (concat_p1
                        (ap pr1
                           (path_sigma' (fun x : C => g x = k (f point2)) 1
                              (match
                                 ((1 @ (1 @ dpoint_eq1)^)^ @ 1) @ 1 as p0 in
                                 (_ = b) return (p0 = 1 @ p0)
                               with
                               | 1 => 1
                               end @
                               (whiskerL 1
                                  match
                                    (1 @ (1 @ dpoint_eq1)^)^ as p0 in (_ = a)
                                    return ((p0 @ 1) @ 1 = p0 @ 1)
                                  with
                                  | 1 => 1
                                  end @
                                (whiskerL 1
                                   (whiskerL (1 @ (1 @ dpoint_eq1)^)^
                                      (moveR_pM (1 @ dpoint_eq1) 1
                                         (1 @ (1 @ dpoint_eq1)^) 1)^) @
                                 (whiskerL 1
                                    (concat_V_pp (1 @ (1 @ dpoint_eq1)^)
                                       (1 @ dpoint_eq1)) @
                                  concat_V_pp 1 dpoint_eq1)))))) @
                      match
                        match
                          ((1 @ (1 @ dpoint_eq1)^)^ @ 1) @ 1 as p0 in (_ = b)
                          return (p0 = 1 @ p0)
                        with
                        | 1 => 1
                        end @
                        (whiskerL 1
                           match
                             (1 @ (1 @ dpoint_eq1)^)^ as p0 in (_ = a)
                             return ((p0 @ 1) @ 1 = p0 @ 1)
                           with
                           | 1 => 1
                           end @
                         (whiskerL 1
                            (whiskerL (1 @ (1 @ dpoint_eq1)^)^
                               (moveR_pM (1 @ dpoint_eq1) 1
                                  (1 @ (1 @ dpoint_eq1)^) 1)^) @
                          (whiskerL 1
                             (concat_V_pp (1 @ (1 @ dpoint_eq1)^)
                                (1 @ dpoint_eq1)) @
                           concat_V_pp 1 dpoint_eq1)))
                        as p1 in (_ = p0)
                        return
                          ((path_sigma_uncurried
                              (fun x : C => g x = k (f point2))
                              (h point2; ((1 @ (1 @ dpoint_eq1)^)^ @ 1) @ 1)
                              (h point2; p0) (1; p1))
                           ..1 = 1)
                      with
                      | 1 => 1
                      end))))^) @
         (whiskerL
            (ap pr1
               (path_sigma' (fun x : C => g x = k (f point2)) 1
                  (match
                     ((1 @ (1 @ dpoint_eq1)^)^ @ 1) @ 1 as p0 in (_ = b)
                     return (p0 = 1 @ p0)
                   with
                   | 1 => 1
                   end @
                   (whiskerL 1
                      match
                        (1 @ (1 @ dpoint_eq1)^)^ as p0 in (_ = a)
                        return ((p0 @ 1) @ 1 = p0 @ 1)
                      with
                      | 1 => 1
                      end @
                    (whiskerL 1
                       (whiskerL (1 @ (1 @ dpoint_eq1)^)^
                          (moveR_pM (1 @ dpoint_eq1) 1
                             (1 @ (1 @ dpoint_eq1)^) 1)^) @
                     (whiskerL 1
                        (concat_V_pp (1 @ (1 @ dpoint_eq1)^) (1 @ dpoint_eq1)) @
                      concat_V_pp 1 dpoint_eq1))))))^
            (concat_V_pp 1
               (ap pr1
                  (path_sigma' (fun x : C => g x = k (f point2)) 1
                     (match
                        ((1 @ (1 @ dpoint_eq1)^)^ @ 1) @ 1 as p0 in (_ = b)
                        return (p0 = 1 @ p0)
                      with
                      | 1 => 1
                      end @
                      (whiskerL 1
                         match
                           (1 @ (1 @ dpoint_eq1)^)^ as p0 in (_ = a)
                           return ((p0 @ 1) @ 1 = p0 @ 1)
                         with
                         | 1 => 1
                         end @
                       (whiskerL 1
                          (whiskerL (1 @ (1 @ dpoint_eq1)^)^
                             (moveR_pM (1 @ dpoint_eq1) 1
                                (1 @ (1 @ dpoint_eq1)^) 1)^) @
                        (whiskerL 1
                           (concat_V_pp (1 @ (1 @ dpoint_eq1)^)
                              (1 @ dpoint_eq1)) @
                         concat_V_pp 1 dpoint_eq1))))) @
                1)) @
          match
            ap pr1
              (path_sigma' (fun x : C => g x = k (f point2)) 1
                 (match
                    ((1 @ (1 @ dpoint_eq1)^)^ @ 1) @ 1 as p0 in (_ = b)
                    return (p0 = 1 @ p0)
                  with
                  | 1 => 1
                  end @
                  (whiskerL 1
                     match
                       (1 @ (1 @ dpoint_eq1)^)^ as p0 in (_ = a)
                       return ((p0 @ 1) @ 1 = p0 @ 1)
                     with
                     | 1 => 1
                     end @
                   (whiskerL 1
                      (whiskerL (1 @ (1 @ dpoint_eq1)^)^
                         (moveR_pM (1 @ dpoint_eq1) 1 
                            (1 @ (1 @ dpoint_eq1)^) 1)^) @
                    (whiskerL 1
                       (concat_V_pp (1 @ (1 @ dpoint_eq1)^) (1 @ dpoint_eq1)) @
                     concat_V_pp 1 dpoint_eq1)))))
            as p0 in (_ = a) return (p0^ @ (p0 @ 1) = 1)
          with
          | 1 => 1
          end))))) @
 point_eq (pfiber2_loops {| pointed_fun := g; dpoint_eq := dpoint_eq1 |})) @
1
    destruct dpoint_eq1.
A: Type
point2: IsPointed A
B, C, D: Type
f: A -> B
g: C -> D
k: B -> D
h: A -> C
p: forall x : A, k (f x) = g (h x)
pfiber2_loops_beta {| pointed_fun := g; dpoint_eq := 1 |} 
  (h point2) (((1 @ (1 @ 1)^)^ @ 1) @ 1) 1 @
match
  1^ in (_ = p0) return (p0 = 1 @ (1 @ 1)^ -> (1^ @ 1) @ ((p0^ @ 1) @ 1) = 1)
with
| 1 =>
    fun _ : 1 @ (1 @ 1)^ = 1 @ (1 @ 1)^ =>
    pfiber2_loops_natural_functor_helper 1 1
end 1 =
(ap (pfiber2_loops {| pointed_fun := g; dpoint_eq := 1 |})
   (path_sigma' (fun x : hfiber g (g (h point2)) => x.1 = h point2)
      (path_sigma' (fun x : C => g x = g (h point2)) 1
         (match
            ((1 @ (1 @ 1)^)^ @ 1) @ 1 as p0 in (_ = b) return (p0 = 1 @ p0)
          with
          | 1 => 1
          end @
          (whiskerL 1
             match
               (1 @ (1 @ 1)^)^ as p0 in (_ = a)
               return ((p0 @ 1) @ 1 = p0 @ 1)
             with
             | 1 => 1
             end @
           (whiskerL 1
              (whiskerL (1 @ (1 @ 1)^)^
                 (moveR_pM (1 @ 1) 1 (1 @ (1 @ 1)^) 1)^) @
            (whiskerL 1 (concat_V_pp (1 @ (1 @ 1)^) (1 @ 1)) @
             concat_V_pp 1 1)))))
      (transport_paths_Fl
         (path_sigma' (fun x : C => g x = g (h point2)) 1
            (match
               ((1 @ (1 @ 1)^)^ @ 1) @ 1 as p0 in (_ = b)
               return (p0 = 1 @ p0)
             with
             | 1 => 1
             end @
             (whiskerL 1
                match
                  (1 @ (1 @ 1)^)^ as p0 in (_ = a)
                  return ((p0 @ 1) @ 1 = p0 @ 1)
                with
                | 1 => 1
                end @
              (whiskerL 1
                 (whiskerL (1 @ (1 @ 1)^)^
                    (moveR_pM (1 @ 1) 1 (1 @ (1 @ 1)^) 1)^) @
               (whiskerL 1 (concat_V_pp (1 @ (1 @ 1)^) (1 @ 1)) @
                concat_V_pp 1 1)))))
         1 @
       (1 @
        (whiskerL
           (ap pr1
              (path_sigma' (fun x : C => g x = g (h point2)) 1
                 (match
                    ((1 @ (1 @ 1)^)^ @ 1) @ 1 as p0 in (_ = b)
                    return (p0 = 1 @ p0)
                  with
                  | 1 => 1
                  end @
                  (whiskerL 1
                     match
                       (1 @ (1 @ 1)^)^ as p0 in (_ = a)
                       return ((p0 @ 1) @ 1 = p0 @ 1)
                     with
                     | 1 => 1
                     end @
                   (whiskerL 1
                      (whiskerL (1 @ (1 @ 1)^)^
                         (moveR_pM (1 @ 1) 1 (1 @ (1 @ 1)^) 1)^) @
                    (whiskerL 1 (concat_V_pp (1 @ (1 @ 1)^) (1 @ 1)) @
                     concat_V_pp 1 1))))))^
           (whiskerL 1
              (moveR_pM
                 (ap pr1
                    (path_sigma' (fun x : C => g x = g (h point2)) 1
                       (match
                          ((1 @ (1 @ 1)^)^ @ 1) @ 1 as p0 in (_ = b)
                          return (p0 = 1 @ p0)
                        with
                        | 1 => 1
                        end @
                        (whiskerL 1
                           match
                             (1 @ (1 @ 1)^)^ as p0 in (_ = a)
                             return ((p0 @ 1) @ 1 = p0 @ 1)
                           with
                           | 1 => 1
                           end @
                         (whiskerL 1
                            (whiskerL (1 @ (1 @ 1)^)^
                               (moveR_pM (1 @ 1) 1 (1 @ (1 @ 1)^) 1)^) @
                          (whiskerL 1 (concat_V_pp (1 @ (1 @ 1)^) (1 @ 1)) @
                           concat_V_pp 1 1))))) @
                  1)
                 1 1
                 (moveL_pV
                    (ap pr1
                       (path_sigma' (fun x : C => g x = g (h point2)) 1
                          (match
                             ((1 @ (1 @ 1)^)^ @ 1) @ 1 as p0 in (_ = b)
                             return (p0 = 1 @ p0)
                           with
                           | 1 => 1
                           end @
                           (whiskerL 1
                              match
                                (1 @ (1 @ 1)^)^ as p0 in (_ = a)
                                return ((p0 @ 1) @ 1 = p0 @ 1)
                              with
                              | 1 => 1
                              end @
                            (whiskerL 1
                               (whiskerL (1 @ (1 @ 1)^)^
                                  (moveR_pM (1 @ 1) 1 (1 @ (1 @ 1)^) 1)^) @
                             (whiskerL 1 (concat_V_pp (1 @ (1 @ 1)^) (1 @ 1)) @
                              concat_V_pp 1 1))))) @
                     1)
                    1 1
                    (1 @@
                     (concat_p1
                        (ap pr1
                           (path_sigma' (fun x : C => g x = g (h point2)) 1
                              (match
                                 ((1 @ (1 @ 1)^)^ @ 1) @ 1 as p0 in (_ = b)
                                 return (p0 = 1 @ p0)
                               with
                               | 1 => 1
                               end @
                               (whiskerL 1
                                  match
                                    (1 @ (1 @ 1)^)^ as p0 in (_ = a)
                                    return ((p0 @ 1) @ 1 = p0 @ 1)
                                  with
                                  | 1 => 1
                                  end @
                                (whiskerL 1
                                   (whiskerL (1 @ (1 @ 1)^)^
                                      (moveR_pM (1 @ 1) 1 (1 @ (1 @ 1)^) 1)^) @
                                 (whiskerL 1
                                    (concat_V_pp (1 @ (1 @ 1)^) (1 @ 1)) @
                                  concat_V_pp 1 1)))))) @
                      match
                        match
                          ((1 @ (1 @ 1)^)^ @ 1) @ 1 as p0 in (_ = b)
                          return (p0 = 1 @ p0)
                        with
                        | 1 => 1
                        end @
                        (whiskerL 1
                           match
                             (1 @ (1 @ 1)^)^ as p0 in (_ = a)
                             return ((p0 @ 1) @ 1 = p0 @ 1)
                           with
                           | 1 => 1
                           end @
                         (whiskerL 1
                            (whiskerL (1 @ (1 @ 1)^)^
                               (moveR_pM (1 @ 1) 1 (1 @ (1 @ 1)^) 1)^) @
                          (whiskerL 1 (concat_V_pp (1 @ (1 @ 1)^) (1 @ 1)) @
                           concat_V_pp 1 1)))
                        as p1 in (_ = p0)
                        return
                          ((path_sigma_uncurried
                              (fun x : C => g x = g (h point2))
                              (h point2; ((1 @ (1 @ 1)^)^ @ 1) @ 1)
                              (h point2; p0) (1; p1))
                           ..1 = 1)
                      with
                      | 1 => 1
                      end))))^) @
         (whiskerL
            (ap pr1
               (path_sigma' (fun x : C => g x = g (h point2)) 1
                  (match
                     ((1 @ (1 @ 1)^)^ @ 1) @ 1 as p0 in (_ = b)
                     return (p0 = 1 @ p0)
                   with
                   | 1 => 1
                   end @
                   (whiskerL 1
                      match
                        (1 @ (1 @ 1)^)^ as p0 in (_ = a)
                        return ((p0 @ 1) @ 1 = p0 @ 1)
                      with
                      | 1 => 1
                      end @
                    (whiskerL 1
                       (whiskerL (1 @ (1 @ 1)^)^
                          (moveR_pM (1 @ 1) 1 (1 @ (1 @ 1)^) 1)^) @
                     (whiskerL 1 (concat_V_pp (1 @ (1 @ 1)^) (1 @ 1)) @
                      concat_V_pp 1 1))))))^
            (concat_V_pp 1
               (ap pr1
                  (path_sigma' (fun x : C => g x = g (h point2)) 1
                     (match
                        ((1 @ (1 @ 1)^)^ @ 1) @ 1 as p0 in (_ = b)
                        return (p0 = 1 @ p0)
                      with
                      | 1 => 1
                      end @
                      (whiskerL 1
                         match
                           (1 @ (1 @ 1)^)^ as p0 in (_ = a)
                           return ((p0 @ 1) @ 1 = p0 @ 1)
                         with
                         | 1 => 1
                         end @
                       (whiskerL 1
                          (whiskerL (1 @ (1 @ 1)^)^
                             (moveR_pM (1 @ 1) 1 (1 @ (1 @ 1)^) 1)^) @
                        (whiskerL 1 (concat_V_pp (1 @ (1 @ 1)^) (1 @ 1)) @
                         concat_V_pp 1 1))))) @
                1)) @
          match
            ap pr1
              (path_sigma' (fun x : C => g x = g (h point2)) 1
                 (match
                    ((1 @ (1 @ 1)^)^ @ 1) @ 1 as p0 in (_ = b)
                    return (p0 = 1 @ p0)
                  with
                  | 1 => 1
                  end @
                  (whiskerL 1
                     match
                       (1 @ (1 @ 1)^)^ as p0 in (_ = a)
                       return ((p0 @ 1) @ 1 = p0 @ 1)
                     with
                     | 1 => 1
                     end @
                   (whiskerL 1
                      (whiskerL (1 @ (1 @ 1)^)^
                         (moveR_pM (1 @ 1) 1 (1 @ (1 @ 1)^) 1)^) @
                    (whiskerL 1 (concat_V_pp (1 @ (1 @ 1)^) (1 @ 1)) @
                     concat_V_pp 1 1)))))
            as p0 in (_ = a) return (p0^ @ (p0 @ 1) = 1)
          with
          | 1 => 1
          end))))) @
 point_eq (pfiber2_loops {| pointed_fun := g; dpoint_eq := 1 |})) @
1
    reflexivity.
Defined.

(** The same for an equivalence square; the underlying double-fiber map is [functor_pfiber] of the same square. *)
Definition pfiber2_loops_natural {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* pequiv_pfiber (pequiv_pfiber h k p) h (square_pequiv_pfiber h k p)
    ==* fmap loops k o* pfiber2_loops f
  := pfiber2_loops_natural_functor p.