Require Import Basics.
[Loading ML file number_string_notation_plugin.cmxs (using legacy method) ... done]
Require Import Types.
Require Import WildCat.
Require Import Pointed.Core.
Require Import Pointed.Loops.
Require Import Pointed.pTrunc.
Require Import Pointed.pEquiv.
Require Import Homotopy.Suspension.
Require Import Homotopy.BlakersMassey.
Require Import Truncations.

Generalizable Variables X A B f g n.

Local Open Scope path_scope.
Local Open Scope pointed_scope.

(** ** Pointedness of [Susp] and path spaces thereof *)
(** We arbitrarily choose [North] to be the point. *)
Instance ispointed_susp {X : Type} : IsPointed (Susp X) | 0
  := North.

Instance ispointed_path_susp `{IsPointed X}
  : IsPointed (North = South :> Susp X) | 0 := merid (point X).

Instance ispointed_path_susp' `{IsPointed X}
  : IsPointed (South = North :> Susp X) | 0 := (merid (point X))^.

Definition psusp (X : Type) : pType
  := [Susp X, _].

(** ** Suspension Functor *)

(** [psusp] has a functorial action. *)
(** TODO: make this a displayed functor *)
Instance is0functor_psusp : Is0Functor psusp
  := Build_Is0Functor _ _ _ _ psusp (fun X Y f
      => Build_pMap (functor_susp f) 1).

(** [psusp] is a 1-functor. *)
Instance is1functor_psusp : Is1Functor psusp.
Is1Functor psusp
Proof.
Is1Functor psusp
  snapply Build_Is1Functor.
forall (a b : Type) (f g : a $-> b),
f $== g -> fmap psusp f $== fmap psusp g
forall a : Type, fmap psusp (Id a) $== Id (psusp a)
forall (a b c : Type) (f : a $-> b) (g : b $-> c),
fmap psusp (g $o f) $== fmap psusp g $o fmap psusp f
  (** Action on 2-cells *)
  -
forall (a b : Type) (f g : a $-> b),
f $== g -> fmap psusp f $== fmap psusp g intros X Y f g p.
X, Y: Type
f, g: X $-> Y
p: f $== g
fmap psusp f $== fmap psusp g
    pointed_reduce.
X, Y: Type
f, g: X -> Y
p: f == g
Build_pMap (functor_susp f) 1 ==*
Build_pMap (functor_susp g) 1
    srapply Build_pHomotopy.
X, Y: Type
f, g: X -> Y
p: f == g
Build_pMap (functor_susp f) 1 ==
Build_pMap (functor_susp g) 1
X, Y: Type
f, g: X -> Y
p: f == g
?p pt =
dpoint_eq (Build_pMap (functor_susp f) 1) @
(dpoint_eq (Build_pMap (functor_susp g) 1))^
    {
X, Y: Type
f, g: X -> Y
p: f == g
Build_pMap (functor_susp f) 1 ==
Build_pMap (functor_susp g) 1 simpl.
X, Y: Type
f, g: X -> Y
p: f == g
functor_susp f == functor_susp g
      srapply Susp_ind.
X, Y: Type
f, g: X -> Y
p: f == g
(fun y : Susp X => functor_susp f y = functor_susp g y)
  North
X, Y: Type
f, g: X -> Y
p: f == g
(fun y : Susp X => functor_susp f y = functor_susp g y)
  South
X, Y: Type
f, g: X -> Y
p: f == g
forall x : X,
transport
  (fun y : Susp X =>
   functor_susp f y = functor_susp g y) (merid x) 
  ?H_N = ?H_S
      1,2: reflexivity.
X, Y: Type
f, g: X -> Y
p: f == g
forall x : X,
transport
  (fun y : Susp X =>
   functor_susp f y = functor_susp g y) (merid x) 1 =
1
      intro x; cbn.
X, Y: Type
f, g: X -> Y
p: f == g
x: X
transport
  (fun y : Susp X =>
   functor_susp f y = functor_susp g y) (merid x) 1 =
1
      rewrite transport_paths_FlFr.
X, Y: Type
f, g: X -> Y
p: f == g
x: X
((ap (functor_susp f) (merid x))^ @ 1) @
ap (functor_susp g) (merid x) = 1
      rewrite concat_p1.
X, Y: Type
f, g: X -> Y
p: f == g
x: X
(ap (functor_susp f) (merid x))^ @
ap (functor_susp g) (merid x) = 1
      rewrite 2 Susp_rec_beta_merid.
X, Y: Type
f, g: X -> Y
p: f == g
x: X
(merid (f x))^ @ merid (g x) = 1
      destruct (p x).
X, Y: Type
f, g: X -> Y
p: f == g
x: X
(merid (f x))^ @ merid (f x) = 1
      apply concat_Vp. }
X, Y: Type
f, g: X -> Y
p: f == g
(Susp_ind
   (fun y : Susp X =>
    functor_susp f y = functor_susp g y) 1 1
   (fun x : X =>
    internal_paths_rew_r
      (fun
         p : functor_susp f South =
             functor_susp g South => p = 1)
      (internal_paths_rew_r
         (fun
            p : functor_susp f South =
                functor_susp f North =>
          p @ ap (functor_susp g) (merid x) = 1)
         (internal_paths_rew_r
            (fun
               p : Susp_rec North South
                     (fun x0 : X => merid (f x0))
                     North =
                   Susp_rec North South
                     (fun x0 : X => merid (f x0))
                     South =>
             p^ @ ap (functor_susp g) (merid x) = 1)
            (internal_paths_rew_r
               (fun
                  p : Susp_rec North South
                        (fun x0 : X => merid (g x0))
                        North =
                      Susp_rec North South
                        (fun x0 : X => merid (g x0))
                        South =>
                (merid (f x))^ @ p = 1)
               (let p0 := p x in
                let y := g x in
                match
                  p0 in (_ = y0)
                  return ((merid ...)^ @ merid y0 = 1)
                with
                | 1 => concat_Vp (merid (f x))
                end) (Susp_rec_beta_merid x))
            (Susp_rec_beta_merid x))
         (concat_p1 (ap (functor_susp f) (merid x))^))
      (transport_paths_FlFr (merid x) 1)
    :
    transport
      (fun y : Susp X =>
       functor_susp f y = functor_susp g y) (merid x)
      1 = 1)
 :
 Build_pMap (functor_susp f) 1 ==
 Build_pMap (functor_susp g) 1) pt =
dpoint_eq (Build_pMap (functor_susp f) 1) @
(dpoint_eq (Build_pMap (functor_susp g) 1))^
    reflexivity.
  (** Preservation of identity. *)
  -
forall a : Type, fmap psusp (Id a) $== Id (psusp a) intros X.
X: Type
fmap psusp (Id X) $== Id (psusp X)
    srapply Build_pHomotopy.
X: Type
fmap psusp (Id X) == Id (psusp X)
X: Type
?p pt =
dpoint_eq (fmap psusp (Id X)) @
(dpoint_eq (Id (psusp X)))^
    {
X: Type
fmap psusp (Id X) == Id (psusp X) srapply Susp_ind; try reflexivity.
X: Type
forall x : X,
transport
  (fun y : Susp X =>
   fmap psusp (Id X) y = Id (psusp X) y) (merid x) 1 =
1
      intro x.
X: Type
x: X
transport
  (fun y : Susp X =>
   fmap psusp (Id X) y = Id (psusp X) y) (merid x) 1 =
1
      refine (transport_paths_FFlr _ _ @ _).
X: Type
x: X
((ap (fmap psusp (Id X)) (ap idmap (merid x)))^ @ 1) @
merid x = 1
      by rewrite ap_idmap, Susp_rec_beta_merid,
        concat_p1, concat_Vp. }
X: Type
Susp_ind
  (fun y : Susp X =>
   fmap psusp (Id X) y = Id (psusp X) y) 1 1
  (fun x : X =>
   transport_paths_FFlr (merid x) 1 @
   internal_paths_rew_r
     (fun p : North = Id (psusp X) South =>
      ((ap (fmap psusp (Id X)) p)^ @ 1) @ merid x = 1)
     (internal_paths_rew_r
        (fun
           p : Susp_rec North South
                 (fun x0 : X => merid (Id X x0)) North =
               Susp_rec North South
                 (fun x0 : X => merid (Id X x0)) South
         => (p^ @ 1) @ merid x = 1)
        (internal_paths_rew_r
           (fun
              p : fmap psusp (Id X)
                    (Id (psusp X) South) =
                  fmap psusp (Id X) North =>
            p @ merid x = 1)
           (internal_paths_rew_r
              (fun
                 p : fmap psusp (Id X)
                       (Id (psusp X) South) =
                     fmap psusp (Id X)
                       (Id (psusp X) South) => p = 1)
              1 (concat_Vp (merid x)))
           (concat_p1 (merid (Id X x))^))
        (Susp_rec_beta_merid x)) (ap_idmap (merid x)))
  pt =
dpoint_eq (fmap psusp (Id X)) @
(dpoint_eq (Id (psusp X)))^
    reflexivity.
  (** Preservation of composition. *)
  -
forall (a b c : Type) (f : a $-> b) (g : b $-> c),
fmap psusp (g $o f) $== fmap psusp g $o fmap psusp f pointed_reduce_rewrite; srefine (Build_pHomotopy _ _); cbn.
a, b, c: Type
f: a -> b
g: b -> c
functor_susp (fun x : a => g (f x)) ==
(fun x : Susp a => functor_susp g (functor_susp f x))
a, b, c: Type
f: a -> b
g: b -> c
?Goal ispointed_susp = 1
    {
a, b, c: Type
f: a -> b
g: b -> c
functor_susp (fun x : a => g (f x)) ==
(fun x : Susp a => functor_susp g (functor_susp f x)) srapply Susp_ind; try reflexivity; cbn.
a, b, c: Type
f: a -> b
g: b -> c
forall x : a,
transport
  (fun y : Susp a =>
   functor_susp (fun x0 : a => g (f x0)) y =
   functor_susp g (functor_susp f y)) (merid x) 1 = 1
      intros x.
a, b, c: Type
f: a -> b
g: b -> c
x: a
transport
  (fun y : Susp a =>
   functor_susp (fun x : a => g (f x)) y =
   functor_susp g (functor_susp f y)) (merid x) 1 = 1
      refine (transport_paths_FlFr _ _ @ _).
a, b, c: Type
f: a -> b
g: b -> c
x: a
((ap (functor_susp (fun x : a => g (f x))) (merid x))^ @
 1) @
ap
  (fun x : Susp a => functor_susp g (functor_susp f x))
  (merid x) = 1
      rewrite concat_p1; apply moveR_Vp.
a, b, c: Type
f: a -> b
g: b -> c
x: a
ap
  (fun x : Susp a => functor_susp g (functor_susp f x))
  (merid x) =
ap (functor_susp (fun x : a => g (f x))) (merid x) @ 1
      by rewrite concat_p1, ap_compose, !Susp_rec_beta_merid. }
a, b, c: Type
f: a -> b
g: b -> c
Susp_ind
  (fun y : Susp a =>
   functor_susp (fun x : a => g (f x)) y =
   (fun x : Susp a =>
    functor_susp g (functor_susp f x)) y) 1 1
  ((fun x : a =>
    transport_paths_FlFr (merid x) 1 @
    internal_paths_rew_r
      (fun
         p : functor_susp (fun x0 : a => g (f x0))
               South =
             functor_susp (fun x0 : a => g (f x0))
               North =>
       p @
       ap
         (fun x0 : Susp a =>
          functor_susp g (functor_susp f x0))
         (merid x) = 1)
      (moveR_Vp
         (ap
            (fun x0 : Susp a =>
             functor_susp g (functor_susp f x0))
            (merid x)) 1
         (ap (functor_susp (fun x0 : a => g (f x0)))
            (merid x))
         (internal_paths_rew_r
            (fun
               p : functor_susp g
                     (functor_susp f North) =
                   functor_susp
                     (fun x0 : a => g (f x0)) South =>
             ap
               (fun x0 : Susp a =>
                functor_susp g (functor_susp f x0))
               (merid x) = p)
            (internal_paths_rew_r
               (fun
                  p : functor_susp g
                        (functor_susp f North) =
                      functor_susp g
                        (functor_susp f South) =>
                p =
                ap
                  (functor_susp
                     (fun x0 : a => g (f x0)))
                  (merid x))
               (internal_paths_rew_r
                  (fun
                     p : Susp_rec North South
                           (fun x0 : a => merid (f x0))
                           North =
                         Susp_rec North South
                           (fun x0 : a => merid (f x0))
                           South =>
                   ap (functor_susp g) p =
                   ap
                     (functor_susp
                        (fun x0 : a => g (f x0)))
                     (merid x))
                  (internal_paths_rew_r
                     (fun
                        p : Susp_rec North South
                              (fun ... => merid ...)
                              North =
                            Susp_rec North South
                              (fun ... => merid ...)
                              South =>
                      p =
                      ap
                        (functor_susp
                           (fun ... => g ...))
                        (merid x))
                     (internal_paths_rew_r
                        (fun
                           p : Susp_rec North South
                                 (...) North =
                               Susp_rec North South
                                 (...) South =>
                         merid (g (...)) = p) 1
                        (Susp_rec_beta_merid x))
                     (Susp_rec_beta_merid (f x)))
                  (Susp_rec_beta_merid x))
               (ap_compose (functor_susp f)
                  (functor_susp g) (merid x)))
            (concat_p1
               (ap
                  (functor_susp
                     (fun x0 : a => g (f x0)))
                  (merid x)))))
      (concat_p1
         (ap (functor_susp (fun x0 : a => g (f x0)))
            (merid x))^))
   :
   forall x : a,
   transport
     (fun y : Susp a =>
      functor_susp (fun x0 : a => g (f x0)) y =
      (fun x0 : Susp a =>
       functor_susp g (functor_susp f x0)) y)
     (merid x) 1 = 1) ispointed_susp = 1
    reflexivity.
Defined.

(** ** Loop-Suspension Adjunction *)

Module Book_Loop_Susp_Adjunction.

  (** Here is the proof of the adjunction isomorphism given in the book (6.5.4); we put it in a non-exported module for reasons discussed below. *)
  Definition loop_susp_adjoint `{Funext} (A B : pType)
  : (psusp A ->* B) <~> (A ->* loops B).
H: Funext
A, B: pType
(psusp A ->* B) <~> (A ->* loops B)
  Proof.
H: Funext
A, B: pType
(psusp A ->* B) <~> (A ->* loops B)
    refine (_ oE (issig_pmap (psusp A) B)^-1).
H: Funext
A, B: pType
{f : psusp A -> B & f pt = pt} <~> (A ->* loops B)
    refine (_ oE (equiv_functor_sigma_pb
                 (Q := fun NSm => fst NSm.1 = point B)
                 (equiv_Susp_rec A B))).
H: Funext
A, B: pType
{NSm : {NS : B * B & A -> fst NS = snd NS} &
fst NSm.1 = pt} <~> (A ->* loops B)
    transitivity {bp : {b:B & b = point B} & {b:B & A -> bp.1 = b} }.
H: Funext
A, B: pType
{NSm : {NS : B * B & A -> fst NS = snd NS} &
fst NSm.1 = pt} <~>
{bp : {b : B & b = pt} & {b : B & A -> bp.1 = b}}
H: Funext
A, B: pType
{bp : {b : B & b = pt} & {b : B & A -> bp.1 = b}} <~>
(A ->* loops B)
    1:make_equiv.
H: Funext
A, B: pType
{bp : {b : B & b = pt} & {b : B & A -> bp.1 = b}} <~>
(A ->* loops B)
    refine (_ oE equiv_contr_sigma _); simpl.
H: Funext
A, B: pType
{b : B & A -> pt = b} <~> (A ->* loops B)
    refine (_ oE (equiv_sigma_contr
                   (A := {p : B & A -> point B = p})
                   (fun pm => { q : point B = pm.1 & pm.2 (point A) = q }))^-1).
H: Funext
A, B: pType
{pm : {p : B & A -> pt = p} &
{q : pt = pm.1 & pm.2 pt = q}} <~> (A ->* loops B)
    make_equiv_contr_basedpaths.
  Defined.

  (** Unfortunately, with this definition it seems to be quite hard to prove that the isomorphism is natural on pointed maps.  The following proof gets partway there, but ends with a pretty intractable goal.  It's also quite slow, so we don't want to compile it all the time. *)
  (**
<<
  Definition loop_susp_adjoint_nat_r `{Funext} (A B B' : pType)
             (f : psusp A ->* B) (g : B ->* B')
  : loop_susp_adjoint A B' (g o* f)
    ==* fmap loops g o* loop_susp_adjoint A B f.
  Proof.
    pointed_reduce. (* Very slow for some reason. *)
    exact (Build_pHomotopy _ _).
    - intros a. simpl.
      exact (_ @ (concat_1p _)^).
      exact (_ @ (concat_p1 _)^).
      rewrite !transport_sigma. simpl.
      rewrite !(transport_arrow_fromconst (B := A)).
      rewrite !transport_paths_Fr.
      rewrite !ap_V, !ap_pr1_path_basedpaths.
      Fail rewrite ap_pp, !(ap_compose f g), ap_V. (* This line fails with current versions of the library. *)
      Fail reflexivity.
      admit.
    - cbn.
      Fail reflexivity.
  Abort.
>>
   *)

End Book_Loop_Susp_Adjunction.

(** Thus, instead we will construct the adjunction in terms of a unit and counit natural transformation. *)

Definition loop_susp_unit (X : pType) : X ->* loops (psusp X)
  := Build_pMap (fun x => merid x @ (merid (point X))^) (concat_pV _).

(** By Freudenthal, we have that this map is (2n+2)-connected when [X] is (n+1)-connected. *)
Instance conn_map_loop_susp_unit `{Univalence} (n : trunc_index)
  (X : pType) `{IsConnected n.+1 X}
  : IsConnMap (n +2+ n) (loop_susp_unit X).
H: Univalence
n: trunc_index
X: pType
H0: IsConnected (Tr n.+1) X
IsConnMap (Tr (n +2+ n)) (loop_susp_unit X)
Proof.
H: Univalence
n: trunc_index
X: pType
H0: IsConnected (Tr n.+1) X
IsConnMap (Tr (n +2+ n)) (loop_susp_unit X)
  exact (conn_map_compose _ merid (equiv_concat_r (merid pt)^ _)).
Defined.

(** We also have this corollary: *)
Definition pequiv_ptr_loop_psusp `{Univalence} (X : pType) n `{IsConnected n.+1 X}
  : pTr (n +2+ n) X <~>* pTr (n +2+ n) (loops (psusp X)).
H: Univalence
X: pType
n: trunc_index
H0: IsConnected (Tr n.+1) X
pTr (n +2+ n) X <~>* pTr (n +2+ n) (loops (psusp X))
Proof.
H: Univalence
X: pType
n: trunc_index
H0: IsConnected (Tr n.+1) X
pTr (n +2+ n) X <~>* pTr (n +2+ n) (loops (psusp X))
  snapply Build_pEquiv.
H: Univalence
X: pType
n: trunc_index
H0: IsConnected (Tr n.+1) X
pTr (n +2+ n) X ->* pTr (n +2+ n) (loops (psusp X))
H: Univalence
X: pType
n: trunc_index
H0: IsConnected (Tr n.+1) X
IsEquiv ?pointed_equiv_fun
  1:exact (fmap (pTr _) (loop_susp_unit _)).
H: Univalence
X: pType
n: trunc_index
H0: IsConnected (Tr n.+1) X
IsEquiv (fmap (pTr (n +2+ n)) (loop_susp_unit X))
  rapply O_inverts_conn_map.
Defined.

Definition loop_susp_unit_natural {X Y : pType} (f : X ->* Y)
  : loop_susp_unit Y o* f
  ==* fmap loops (fmap psusp f) o* loop_susp_unit X.
X, Y: pType
f: X ->* Y
loop_susp_unit Y o* f ==*
fmap loops (fmap psusp f) o* loop_susp_unit X
Proof.
X, Y: pType
f: X ->* Y
loop_susp_unit Y o* f ==*
fmap loops (fmap psusp f) o* loop_susp_unit X
  pointed_reduce.
X: Type
point0: IsPointed X
Y: Type
f: X -> Y
loop_susp_unit [Y, f point0]
o* {| pointed_fun := f; dpoint_eq := 1 |} ==*
Build_pMap
  (fun p : ispointed_susp = ispointed_susp =>
   1 @ (ap (functor_susp f) p @ 1)) 1
o* loop_susp_unit [X, point0]
  snapply Build_pHomotopy; cbn.
X: Type
point0: IsPointed X
Y: Type
f: X -> Y
(fun x : X => merid (f x) @ (merid (f point0))^) ==
(fun x : X =>
 1 @
 (ap (functor_susp f) (merid x @ (merid point0)^) @ 1))
X: Type
point0: IsPointed X
Y: Type
f: X -> Y
?Goal point0 =
(1 @ concat_pV (merid (f point0))) @
(ap
   (fun p : ispointed_susp = ispointed_susp =>
    1 @ (ap (functor_susp f) p @ 1))
   (concat_pV (merid point0)) @ 1)^
  -
X: Type
point0: IsPointed X
Y: Type
f: X -> Y
(fun x : X => merid (f x) @ (merid (f point0))^) ==
(fun x : X =>
 1 @
 (ap (functor_susp f) (merid x @ (merid point0)^) @ 1)) intros x; symmetry.
X: Type
point0: IsPointed X
Y: Type
f: X -> Y
x: X
1 @
(ap (functor_susp f) (merid x @ (merid point0)^) @ 1) =
merid (f x) @ (merid (f point0))^
    lhs napply concat_1p; lhs napply concat_p1.
X: Type
point0: IsPointed X
Y: Type
f: X -> Y
x: X
ap (functor_susp f) (merid x @ (merid point0)^) =
merid (f x) @ (merid (f point0))^
    lhs napply (ap_pV _ (merid x) (merid point0)).
X: Type
point0: IsPointed X
Y: Type
f: X -> Y
x: X
ap (functor_susp f) (merid x) @
(ap (functor_susp f) (merid point0))^ =
merid (f x) @ (merid (f point0))^
    exact (Susp_rec_beta_merid _ @@ inverse2 (Susp_rec_beta_merid _)).
  -
X: Type
point0: IsPointed X
Y: Type
f: X -> Y
((fun x : X =>
  (concat_1p
     (ap (functor_susp f) (merid x @ (merid point0)^) @
      1) @
   (concat_p1
      (ap (functor_susp f) (merid x @ (merid point0)^)) @
    (ap_pV (functor_susp f) (merid x) (merid point0) @
     (Susp_rec_beta_merid x @@
      inverse2 (Susp_rec_beta_merid point0)))))^)
 :
 (fun x : X => merid (f x) @ (merid (f point0))^) ==
 (fun x : X =>
  1 @
  (ap (functor_susp f) (merid x @ (merid point0)^) @ 1)))
  point0 =
(1 @ concat_pV (merid (f point0))) @
(ap
   (fun p : ispointed_susp = ispointed_susp =>
    1 @ (ap (functor_susp f) p @ 1))
   (concat_pV (merid point0)) @ 1)^ cbn.
X: Type
point0: IsPointed X
Y: Type
f: X -> Y
(concat_1p
   (ap (functor_susp f)
      (merid point0 @ (merid point0)^) @ 1) @
 (concat_p1
    (ap (functor_susp f)
       (merid point0 @ (merid point0)^)) @
  (ap_pV (functor_susp f) 
     (merid point0) (merid point0) @
   (Susp_rec_beta_merid point0 @@
    inverse2 (Susp_rec_beta_merid point0)))))^ =
(1 @ concat_pV (merid (f point0))) @
(ap
   (fun p : ispointed_susp = ispointed_susp =>
    1 @ (ap (functor_susp f) p @ 1))
   (concat_pV (merid point0)) @ 1)^ apply moveL_pV.
X: Type
point0: IsPointed X
Y: Type
f: X -> Y
(concat_1p
   (ap (functor_susp f)
      (merid point0 @ (merid point0)^) @ 1) @
 (concat_p1
    (ap (functor_susp f)
       (merid point0 @ (merid point0)^)) @
  (ap_pV (functor_susp f) 
     (merid point0) (merid point0) @
   (Susp_rec_beta_merid point0 @@
    inverse2 (Susp_rec_beta_merid point0)))))^ @
(ap
   (fun p : ispointed_susp = ispointed_susp =>
    1 @ (ap (functor_susp f) p @ 1))
   (concat_pV (merid point0)) @ 1) =
1 @ concat_pV (merid (f point0))
    rhs napply concat_1p.
X: Type
point0: IsPointed X
Y: Type
f: X -> Y
(concat_1p
   (ap (functor_susp f)
      (merid point0 @ (merid point0)^) @ 1) @
 (concat_p1
    (ap (functor_susp f)
       (merid point0 @ (merid point0)^)) @
  (ap_pV (functor_susp f) 
     (merid point0) (merid point0) @
   (Susp_rec_beta_merid point0 @@
    inverse2 (Susp_rec_beta_merid point0)))))^ @
(ap
   (fun p : ispointed_susp = ispointed_susp =>
    1 @ (ap (functor_susp f) p @ 1))
   (concat_pV (merid point0)) @ 1) =
concat_pV (merid (f point0))
    apply moveR_Vp.
X: Type
point0: IsPointed X
Y: Type
f: X -> Y
ap
  (fun p : ispointed_susp = ispointed_susp =>
   1 @ (ap (functor_susp f) p @ 1))
  (concat_pV (merid point0)) @ 1 =
(concat_1p
   (ap (functor_susp f)
      (merid point0 @ (merid point0)^) @ 1) @
 (concat_p1
    (ap (functor_susp f)
       (merid point0 @ (merid point0)^)) @
  (ap_pV (functor_susp f) 
     (merid point0) (merid point0) @
   (Susp_rec_beta_merid point0 @@
    inverse2 (Susp_rec_beta_merid point0))))) @
concat_pV (merid (f point0))
    lhs napply concat_p1.
X: Type
point0: IsPointed X
Y: Type
f: X -> Y
ap
  (fun p : ispointed_susp = ispointed_susp =>
   1 @ (ap (functor_susp f) p @ 1))
  (concat_pV (merid point0)) =
(concat_1p
   (ap (functor_susp f)
      (merid point0 @ (merid point0)^) @ 1) @
 (concat_p1
    (ap (functor_susp f)
       (merid point0 @ (merid point0)^)) @
  (ap_pV (functor_susp f) 
     (merid point0) (merid point0) @
   (Susp_rec_beta_merid point0 @@
    inverse2 (Susp_rec_beta_merid point0))))) @
concat_pV (merid (f point0))
    (* Handle the [ap ... (1 @ q)] part. *)
    lhs napply (ap_compose (fun p => ap _ p @ 1) _ (concat_pV _)).
X: Type
point0: IsPointed X
Y: Type
f: X -> Y
ap (concat 1)
  (ap
     (fun p : ispointed_susp = ispointed_susp =>
      ap (functor_susp f) p @ 1)
     (concat_pV (merid point0))) =
(concat_1p
   (ap (functor_susp f)
      (merid point0 @ (merid point0)^) @ 1) @
 (concat_p1
    (ap (functor_susp f)
       (merid point0 @ (merid point0)^)) @
  (ap_pV (functor_susp f) 
     (merid point0) (merid point0) @
   (Susp_rec_beta_merid point0 @@
    inverse2 (Susp_rec_beta_merid point0))))) @
concat_pV (merid (f point0))
    lhs_V napply concat_1p_1.
X: Type
point0: IsPointed X
Y: Type
f: X -> Y
concat_1p
  (ap (functor_susp f)
     (merid point0 @ (merid point0)^) @ 1) @
ap
  (fun p : ispointed_susp = ispointed_susp =>
   ap (functor_susp f) p @ 1)
  (concat_pV (merid point0)) =
(concat_1p
   (ap (functor_susp f)
      (merid point0 @ (merid point0)^) @ 1) @
 (concat_p1
    (ap (functor_susp f)
       (merid point0 @ (merid point0)^)) @
  (ap_pV (functor_susp f) 
     (merid point0) (merid point0) @
   (Susp_rec_beta_merid point0 @@
    inverse2 (Susp_rec_beta_merid point0))))) @
concat_pV (merid (f point0))
    rhs napply concat_pp_p.
X: Type
point0: IsPointed X
Y: Type
f: X -> Y
concat_1p
  (ap (functor_susp f)
     (merid point0 @ (merid point0)^) @ 1) @
ap
  (fun p : ispointed_susp = ispointed_susp =>
   ap (functor_susp f) p @ 1)
  (concat_pV (merid point0)) =
concat_1p
  (ap (functor_susp f)
     (merid point0 @ (merid point0)^) @ 1) @
((concat_p1
    (ap (functor_susp f)
       (merid point0 @ (merid point0)^)) @
  (ap_pV (functor_susp f) 
     (merid point0) (merid point0) @
   (Susp_rec_beta_merid point0 @@
    inverse2 (Susp_rec_beta_merid point0)))) @
 concat_pV (merid (f point0)))
    apply whiskerL.
X: Type
point0: IsPointed X
Y: Type
f: X -> Y
ap
  (fun p : ispointed_susp = ispointed_susp =>
   ap (functor_susp f) p @ 1)
  (concat_pV (merid point0)) =
(concat_p1
   (ap (functor_susp f)
      (merid point0 @ (merid point0)^)) @
 (ap_pV (functor_susp f) (merid point0) (merid point0) @
  (Susp_rec_beta_merid point0 @@
   inverse2 (Susp_rec_beta_merid point0)))) @
concat_pV (merid (f point0))
    (* Handle the [ap ... (q @ 1)] part. *)
    lhs napply (ap_compose _ (fun q => q @ 1) (concat_pV _)).
X: Type
point0: IsPointed X
Y: Type
f: X -> Y
ap (fun q : ispointed_susp = ispointed_susp => q @ 1)
  (ap (ap (functor_susp f)) (concat_pV (merid point0))) =
(concat_p1
   (ap (functor_susp f)
      (merid point0 @ (merid point0)^)) @
 (ap_pV (functor_susp f) (merid point0) (merid point0) @
  (Susp_rec_beta_merid point0 @@
   inverse2 (Susp_rec_beta_merid point0)))) @
concat_pV (merid (f point0))
    lhs_V napply concat_p1_1.
X: Type
point0: IsPointed X
Y: Type
f: X -> Y
concat_p1
  (ap (functor_susp f)
     (merid point0 @ (merid point0)^)) @
ap (ap (functor_susp f)) (concat_pV (merid point0)) =
(concat_p1
   (ap (functor_susp f)
      (merid point0 @ (merid point0)^)) @
 (ap_pV (functor_susp f) (merid point0) (merid point0) @
  (Susp_rec_beta_merid point0 @@
   inverse2 (Susp_rec_beta_merid point0)))) @
concat_pV (merid (f point0))
    rhs napply concat_pp_p.
X: Type
point0: IsPointed X
Y: Type
f: X -> Y
concat_p1
  (ap (functor_susp f)
     (merid point0 @ (merid point0)^)) @
ap (ap (functor_susp f)) (concat_pV (merid point0)) =
concat_p1
  (ap (functor_susp f)
     (merid point0 @ (merid point0)^)) @
((ap_pV (functor_susp f) (merid point0) (merid point0) @
  (Susp_rec_beta_merid point0 @@
   inverse2 (Susp_rec_beta_merid point0))) @
 concat_pV (merid (f point0)))
    apply whiskerL.
X: Type
point0: IsPointed X
Y: Type
f: X -> Y
ap (ap (functor_susp f)) (concat_pV (merid point0)) =
(ap_pV (functor_susp f) (merid point0) (merid point0) @
 (Susp_rec_beta_merid point0 @@
  inverse2 (Susp_rec_beta_merid point0))) @
concat_pV (merid (f point0))
    (* Finish it off. *)
    symmetry.
X: Type
point0: IsPointed X
Y: Type
f: X -> Y
(ap_pV (functor_susp f) (merid point0) (merid point0) @
 (Susp_rec_beta_merid point0 @@
  inverse2 (Susp_rec_beta_merid point0))) @
concat_pV (merid (f point0)) =
ap (ap (functor_susp f)) (concat_pV (merid point0))
    lhs napply concat_pp_p.
X: Type
point0: IsPointed X
Y: Type
f: X -> Y
ap_pV (functor_susp f) (merid point0) (merid point0) @
((Susp_rec_beta_merid point0 @@
  inverse2 (Susp_rec_beta_merid point0)) @
 concat_pV (merid (f point0))) =
ap (ap (functor_susp f)) (concat_pV (merid point0))
    exact (ap_ap_concat_pV _ _ _ (Susp_rec_beta_merid point0)).
Defined.

Definition loop_susp_counit (X : pType) : psusp (loops X) ->* X
  := Build_pMap (Susp_rec (point X) (point X) idmap) 1.

Definition loop_susp_counit_natural {X Y : pType} (f : X ->* Y)
  : f o* loop_susp_counit X
  ==* loop_susp_counit Y o* fmap psusp (fmap loops f).
X, Y: pType
f: X ->* Y
f o* loop_susp_counit X ==*
loop_susp_counit Y o* fmap psusp (fmap loops f)
Proof.
X, Y: pType
f: X ->* Y
f o* loop_susp_counit X ==*
loop_susp_counit Y o* fmap psusp (fmap loops f)
  pointed_reduce.
X: Type
point0: IsPointed X
Y: Type
f: X -> Y
{| pointed_fun := f; dpoint_eq := 1 |}
o* loop_susp_counit [X, point0] ==*
loop_susp_counit [Y, f point0]
o* Build_pMap
     (functor_susp
        (fun p : point0 = point0 => 1 @ (ap f p @ 1)))
     1
  simple refine (Build_pHomotopy _ _); simpl.
X: Type
point0: IsPointed X
Y: Type
f: X -> Y
(fun x : Susp (point0 = point0) =>
 f (Susp_rec pt pt idmap x)) ==
(fun x : Susp (point0 = point0) =>
 Susp_rec pt pt idmap
   (functor_susp
      (fun p : point0 = point0 => 1 @ (ap f p @ 1)) x))
X: Type
point0: IsPointed X
Y: Type
f: X -> Y
?Goal pt = 1
  -
X: Type
point0: IsPointed X
Y: Type
f: X -> Y
(fun x : Susp (point0 = point0) =>
 f (Susp_rec pt pt idmap x)) ==
(fun x : Susp (point0 = point0) =>
 Susp_rec pt pt idmap
   (functor_susp
      (fun p : point0 = point0 => 1 @ (ap f p @ 1)) x)) simple refine (Susp_ind _ _ _ _); cbn; try reflexivity; intros p.
X: Type
point0: IsPointed X
Y: Type
f: X -> Y
p: point0 = point0
transport
  (fun y : Susp (point0 = point0) =>
   f (Susp_rec pt pt idmap y) =
   Susp_rec pt pt idmap
     (functor_susp
        (fun p : point0 = point0 => 1 @ (ap f p @ 1))
        y)) (merid p) 1 = 1
    rewrite transport_paths_FlFr, ap_compose, concat_p1.
X: Type
point0: IsPointed X
Y: Type
f: X -> Y
p: point0 = point0
(ap f (ap (Susp_rec pt pt idmap) (merid p)))^ @
ap
  (fun x : Susp (point0 = point0) =>
   Susp_rec pt pt idmap
     (functor_susp
        (fun p : point0 = point0 => 1 @ (ap f p @ 1))
        x)) (merid p) = 1
    apply moveR_Vp.
X: Type
point0: IsPointed X
Y: Type
f: X -> Y
p: point0 = point0
ap
  (fun x : Susp (point0 = point0) =>
   Susp_rec pt pt idmap
     (functor_susp
        (fun p : point0 = point0 => 1 @ (ap f p @ 1))
        x)) (merid p) =
ap f (ap (Susp_rec pt pt idmap) (merid p)) @ 1
    refine (ap_compose
              (Susp_rec North South (fun x0 => merid (1 @ (ap f x0 @ 1))))
              (Susp_rec (point Y) (point Y) idmap) (merid p) @ _).
X: Type
point0: IsPointed X
Y: Type
f: X -> Y
p: point0 = point0
ap (Susp_rec pt pt idmap)
  (ap
     (Susp_rec North South
        (fun x0 : point0 = point0 =>
         merid (1 @ (ap f x0 @ 1)))) 
     (merid p)) =
ap f (ap (Susp_rec pt pt idmap) (merid p)) @ 1
    do 2 rewrite Susp_rec_beta_merid.
X: Type
point0: IsPointed X
Y: Type
f: X -> Y
p: point0 = point0
1 @ (ap f p @ 1) =
ap f (ap (Susp_rec pt pt idmap) (merid p)) @ 1
    refine (concat_1p _ @ _).
X: Type
point0: IsPointed X
Y: Type
f: X -> Y
p: point0 = point0
ap f p @ 1 =
ap f (ap (Susp_rec pt pt idmap) (merid p)) @ 1 f_ap.
X: Type
point0: IsPointed X
Y: Type
f: X -> Y
p: point0 = point0
ap f p = ap f (ap (Susp_rec pt pt idmap) (merid p)) f_ap.
X: Type
point0: IsPointed X
Y: Type
f: X -> Y
p: point0 = point0
p = ap (Susp_rec pt pt idmap) (merid p) symmetry.
X: Type
point0: IsPointed X
Y: Type
f: X -> Y
p: point0 = point0
ap (Susp_rec pt pt idmap) (merid p) = p
    exact (Susp_rec_beta_merid _).
  -
X: Type
point0: IsPointed X
Y: Type
f: X -> Y
Susp_ind
  (fun y : Susp (point0 = point0) =>
   (fun x : Susp (point0 = point0) =>
    f (Susp_rec pt pt idmap x)) y =
   (fun x : Susp (point0 = point0) =>
    Susp_rec pt pt idmap
      (functor_susp
         (fun p : point0 = point0 => 1 @ (ap f p @ 1))
         x)) y)
  (1
   :
   (fun y : Susp (point0 = point0) =>
    (fun x : Susp (point0 = point0) =>
     f (Susp_rec pt pt idmap x)) y =
    (fun x : Susp (point0 = point0) =>
     Susp_rec pt pt idmap
       (functor_susp
          (fun p : point0 = point0 => 1 @ (ap f p @ 1))
          x)) y) North)
  (1
   :
   (fun y : Susp (point0 = point0) =>
    (fun x : Susp (point0 = point0) =>
     f (Susp_rec pt pt idmap x)) y =
    (fun x : Susp (point0 = point0) =>
     Susp_rec pt pt idmap
       (functor_susp
          (fun p : point0 = point0 => 1 @ (ap f p @ 1))
          x)) y) South)
  ((fun p : point0 = point0 =>
    internal_paths_rew_r
      (fun
         p0 : f (Susp_rec pt pt idmap South) =
              Susp_rec pt pt idmap
                (functor_susp
                   (fun p0 : point0 = point0 =>
                    1 @ (ap f p0 @ 1)) South) =>
       p0 = 1)
      (internal_paths_rew_r
         (fun
            p0 : f (Susp_rec pt pt idmap North) =
                 f (Susp_rec pt pt idmap South) =>
          (p0^ @ 1) @
          ap
            (fun x : Susp (point0 = point0) =>
             Susp_rec pt pt idmap
               (functor_susp
                  (fun p1 : point0 = point0 =>
                   1 @ (ap f p1 @ 1)) x)) 
            (merid p) = 1)
         (internal_paths_rew_r
            (fun
               p0 : f (Susp_rec pt pt idmap South) =
                    f (Susp_rec pt pt idmap North) =>
             p0 @
             ap
               (fun x : Susp (point0 = point0) =>
                Susp_rec pt pt idmap
                  (functor_susp
                     (fun p1 : point0 = point0 =>
                      1 @ (ap f p1 @ 1)) x)) 
               (merid p) = 1)
            (moveR_Vp
               (ap
                  (fun x : Susp (point0 = point0) =>
                   Susp_rec pt pt idmap
                     (functor_susp
                       (fun p0 : point0 = point0 =>
                       1 @ (ap f p0 @ 1)) x))
                  (merid p)) 1
               (ap f
                  (ap (Susp_rec pt pt idmap) (merid p)))
               (ap_compose
                  (Susp_rec North South
                     (fun x0 : point0 = point0 =>
                      merid (1 @ (ap f x0 @ 1))))
                  (Susp_rec pt pt idmap) 
                  (merid p) @
                internal_paths_rew_r
                  (fun
                     p0 : 
                      Susp_rec North South
                       (fun x0 : point0 = point0 =>
                       merid (1 @ ...)) North =
                      Susp_rec North South
                       (fun x0 : point0 = point0 =>
                       merid (1 @ ...)) South =>
                   ap (Susp_rec pt pt idmap) p0 =
                   ap f
                     (ap 
                       (Susp_rec pt pt idmap)
                       (merid p)) @ 1)
                  (internal_paths_rew_r
                     (fun
                       p0 : 
                       Susp_rec pt pt idmap North =
                       Susp_rec pt pt idmap South =>
                      p0 =
                      ap f
                       (ap 
                       (Susp_rec pt pt idmap)
                       (merid p)) @ 1)
                     (concat_1p (ap f p @ 1) @
                      ap11
                       (ap11 1
                       (ap11 1
                       (Susp_rec_beta_merid p)^)) 1)
                     (Susp_rec_beta_merid
                       (1 @ (ap f p @ 1))))
                  (Susp_rec_beta_merid p)))
            (concat_p1
               (ap f
                  (ap (Susp_rec pt pt idmap) (merid p)))^))
         (ap_compose (Susp_rec pt pt idmap) f
            (merid p)))
      (transport_paths_FlFr (merid p) 1))
   :
   forall x : point0 = point0,
   transport
     (fun y : Susp (point0 = point0) =>
      (fun x0 : Susp (point0 = point0) =>
       f (Susp_rec pt pt idmap x0)) y =
      (fun x0 : Susp (point0 = point0) =>
       Susp_rec pt pt idmap
         (functor_susp
            (fun p : point0 = point0 =>
             1 @ (ap f p @ 1)) x0)) y) 
     (merid x)
     (1
      :
      (fun y : Susp (point0 = point0) =>
       (fun x0 : Susp (point0 = point0) =>
        f (Susp_rec pt pt idmap x0)) y =
       (fun x0 : Susp (point0 = point0) =>
        Susp_rec pt pt idmap
          (functor_susp
             (fun p : point0 = point0 =>
              1 @ (ap f p @ 1)) x0)) y) North) =
   (1
    :
    (fun y : Susp (point0 = point0) =>
     (fun x0 : Susp (point0 = point0) =>
      f (Susp_rec pt pt idmap x0)) y =
     (fun x0 : Susp (point0 = point0) =>
      Susp_rec pt pt idmap
        (functor_susp
           (fun p : point0 = point0 =>
            1 @ (ap f p @ 1)) x0)) y) South)) pt = 1 reflexivity.
Qed.

(** Now the triangle identities *)

Definition loop_susp_triangle1 (X : pType)
  : fmap loops (loop_susp_counit X) o* loop_susp_unit (loops X)
  ==* pmap_idmap.
X: pType
fmap loops (loop_susp_counit X)
o* loop_susp_unit (loops X) ==* pmap_idmap
Proof.
X: pType
fmap loops (loop_susp_counit X)
o* loop_susp_unit (loops X) ==* pmap_idmap
  (* This proof has a lot of overlap with [loop_susp_unit_natural]. Can a common lemma be factored out? *)
  snapply Build_pHomotopy.
X: pType
fmap loops (loop_susp_counit X)
o* loop_susp_unit (loops X) == pmap_idmap
X: pType
?p pt =
dpoint_eq
  (fmap loops (loop_susp_counit X)
   o* loop_susp_unit (loops X)) @
(dpoint_eq pmap_idmap)^
  -
X: pType
fmap loops (loop_susp_counit X)
o* loop_susp_unit (loops X) == pmap_idmap intros p; cbn.
X: pType
p: loops X
1 @
(ap (Susp_rec pt pt idmap) (merid p @ (merid 1)^) @ 1) =
p
    lhs napply concat_1p; lhs napply concat_p1.
X: pType
p: loops X
ap (Susp_rec pt pt idmap) (merid p @ (merid 1)^) = p
    lhs napply (ap_pV _ (merid p) _).
X: pType
p: loops X
ap (Susp_rec pt pt idmap) (merid p) @
(ap (Susp_rec pt pt idmap) (merid 1))^ = p
    lhs napply (Susp_rec_beta_merid _ @@ inverse2 (Susp_rec_beta_merid _)).
X: pType
p: loops X
p @ 1^ = p
    apply concat_p1.
  -
X: pType
((fun p : loops X =>
  concat_1p
    (ap (Susp_rec pt pt idmap) (merid p @ (merid 1)^) @
     1) @
  (concat_p1
     (ap (Susp_rec pt pt idmap) (merid p @ (merid 1)^)) @
   (ap_pV (Susp_rec pt pt idmap) (merid p) (merid 1) @
    ((Susp_rec_beta_merid p @@
      inverse2 (Susp_rec_beta_merid 1)) @ concat_p1 p)))
  :
  (fmap loops (loop_susp_counit X)
   o* loop_susp_unit (loops X)) p = pmap_idmap p)
 :
 fmap loops (loop_susp_counit X)
 o* loop_susp_unit (loops X) == pmap_idmap) pt =
dpoint_eq
  (fmap loops (loop_susp_counit X)
   o* loop_susp_unit (loops X)) @
(dpoint_eq pmap_idmap)^ simpl.
X: pType
concat_1p
  (ap (Susp_rec pt pt idmap) (merid pt @ (merid 1)^) @
   1) @
(concat_p1
   (ap (Susp_rec pt pt idmap) (merid pt @ (merid 1)^)) @
 (ap_pV (Susp_rec pt pt idmap) (merid pt) (merid 1) @
  ((Susp_rec_beta_merid pt @@
    inverse2 (Susp_rec_beta_merid 1)) @ 1))) =
(ap
   (fun p : pt = pt =>
    1 @ (ap (Susp_rec pt pt idmap) p @ 1))
   (concat_pV (merid pt)) @ 1) @ 1
    do 2 rhs napply concat_p1.
X: pType
concat_1p
  (ap (Susp_rec pt pt idmap) (merid pt @ (merid 1)^) @
   1) @
(concat_p1
   (ap (Susp_rec pt pt idmap) (merid pt @ (merid 1)^)) @
 (ap_pV (Susp_rec pt pt idmap) (merid pt) (merid 1) @
  ((Susp_rec_beta_merid pt @@
    inverse2 (Susp_rec_beta_merid 1)) @ 1))) =
ap
  (fun p : pt = pt =>
   1 @ (ap (Susp_rec pt pt idmap) p @ 1))
  (concat_pV (merid pt))
    rhs napply (ap_compose (fun p => ap _ p @ 1) _ (concat_pV _)).
X: pType
concat_1p
  (ap (Susp_rec pt pt idmap) (merid pt @ (merid 1)^) @
   1) @
(concat_p1
   (ap (Susp_rec pt pt idmap) (merid pt @ (merid 1)^)) @
 (ap_pV (Susp_rec pt pt idmap) (merid pt) (merid 1) @
  ((Susp_rec_beta_merid pt @@
    inverse2 (Susp_rec_beta_merid 1)) @ 1))) =
ap (concat 1)
  (ap
     (fun p : pt = pt =>
      ap (Susp_rec pt pt idmap) p @ 1)
     (concat_pV (merid pt)))
    rhs_V napply (concat_1p_1 _ _).
X: pType
concat_1p
  (ap (Susp_rec pt pt idmap) (merid pt @ (merid 1)^) @
   1) @
(concat_p1
   (ap (Susp_rec pt pt idmap) (merid pt @ (merid 1)^)) @
 (ap_pV (Susp_rec pt pt idmap) (merid pt) (merid 1) @
  ((Susp_rec_beta_merid pt @@
    inverse2 (Susp_rec_beta_merid 1)) @ 1))) =
concat_1p
  (ap (Susp_rec pt pt idmap) (merid pt @ (merid pt)^) @
   1) @
ap
  (fun p : pt = pt => ap (Susp_rec pt pt idmap) p @ 1)
  (concat_pV (merid pt))
    apply whiskerL.
X: pType
concat_p1
  (ap (Susp_rec pt pt idmap) (merid pt @ (merid 1)^)) @
(ap_pV (Susp_rec pt pt idmap) (merid pt) (merid 1) @
 ((Susp_rec_beta_merid pt @@
   inverse2 (Susp_rec_beta_merid 1)) @ 1)) =
ap
  (fun p : pt = pt => ap (Susp_rec pt pt idmap) p @ 1)
  (concat_pV (merid pt))
    rhs napply (ap_compose _ (fun q => q @ 1) (concat_pV _)).
X: pType
concat_p1
  (ap (Susp_rec pt pt idmap) (merid pt @ (merid 1)^)) @
(ap_pV (Susp_rec pt pt idmap) (merid pt) (merid 1) @
 ((Susp_rec_beta_merid pt @@
   inverse2 (Susp_rec_beta_merid 1)) @ 1)) =
ap (fun q : pt = pt => q @ 1)
  (ap (ap (Susp_rec pt pt idmap))
     (concat_pV (merid pt)))
    rhs_V napply concat_p1_1.
X: pType
concat_p1
  (ap (Susp_rec pt pt idmap) (merid pt @ (merid 1)^)) @
(ap_pV (Susp_rec pt pt idmap) (merid pt) (merid 1) @
 ((Susp_rec_beta_merid pt @@
   inverse2 (Susp_rec_beta_merid 1)) @ 1)) =
concat_p1
  (ap (Susp_rec pt pt idmap) (merid pt @ (merid pt)^)) @
ap (ap (Susp_rec pt pt idmap)) (concat_pV (merid pt))
    apply whiskerL.
X: pType
ap_pV (Susp_rec pt pt idmap) (merid pt) (merid 1) @
((Susp_rec_beta_merid pt @@
  inverse2 (Susp_rec_beta_merid 1)) @ 1) =
ap (ap (Susp_rec pt pt idmap)) (concat_pV (merid pt))
    exact (ap_ap_concat_pV _ _ _ (Susp_rec_beta_merid pt)).
Defined. (* A bit slow, ~0.09s. *)

Definition loop_susp_triangle2 (X : pType)
  : loop_susp_counit (psusp X) o* fmap psusp (loop_susp_unit X)
  ==* pmap_idmap.
X: pType
loop_susp_counit (psusp X)
o* fmap psusp (loop_susp_unit X) ==* pmap_idmap
Proof.
X: pType
loop_susp_counit (psusp X)
o* fmap psusp (loop_susp_unit X) ==* pmap_idmap
  simple refine (Build_pHomotopy _ _);
  [ simple refine (Susp_ind _ _ _ _) | ]; try reflexivity; cbn.
X: pType
Susp_rec ispointed_susp ispointed_susp idmap
  (functor_susp (fun x : X => merid x @ (merid pt)^)
     South) = South
X: pType
forall x : X,
transport
  (fun y : Susp X =>
   Susp_rec ispointed_susp ispointed_susp idmap
     (functor_susp
        (fun x0 : X => merid x0 @ (merid pt)^) y) = y)
  (merid x) 1 = ?Goal
  -
X: pType
Susp_rec ispointed_susp ispointed_susp idmap
  (functor_susp (fun x : X => merid x @ (merid pt)^)
     South) = South exact (merid (point X)).
  -
X: pType
forall x : X,
transport
  (fun y : Susp X =>
   Susp_rec ispointed_susp ispointed_susp idmap
     (functor_susp
        (fun x0 : X => merid x0 @ (merid pt)^) y) = y)
  (merid x) 1 = merid pt intros x.
X: pType
x: X
transport
  (fun y : Susp X =>
   Susp_rec ispointed_susp ispointed_susp idmap
     (functor_susp
        (fun x : X => merid x @ (merid pt)^) y) = y)
  (merid x) 1 = merid pt
    rewrite transport_paths_FlFr, ap_idmap, ap_compose.
X: pType
x: X
((ap (Susp_rec ispointed_susp ispointed_susp idmap)
    (ap
       (functor_susp
          (fun x : X => merid x @ (merid pt)^))
       (merid x)))^ @ 1) @ merid x = merid pt
    rewrite Susp_rec_beta_merid.
X: pType
x: X
((ap (Susp_rec ispointed_susp ispointed_susp idmap)
    (merid (merid x @ (merid pt)^)))^ @ 1) @ merid x =
merid pt
    apply moveR_pM; rewrite concat_p1.
X: pType
x: X
(ap (Susp_rec ispointed_susp ispointed_susp idmap)
   (merid (merid x @ (merid pt)^)))^ =
merid pt @ (merid x)^
    refine (inverse2 (Susp_rec_beta_merid _) @ _).
X: pType
x: X
(merid x @ (merid pt)^)^ = merid pt @ (merid x)^
    rewrite inv_pp, inv_V; reflexivity.
Qed.

(** Now we can finally construct the adjunction equivalence. *)

Definition loop_susp_adjoint `{Funext} (A B : pType)
  : (psusp A ->** B) <~>* (A ->** loops B).
H: Funext
A, B: pType
(psusp A ->** B) <~>* (A ->** loops B)
Proof.
H: Funext
A, B: pType
(psusp A ->** B) <~>* (A ->** loops B)
  snapply Build_pEquiv'.
H: Funext
A, B: pType
(psusp A ->** B) <~> (A ->** loops B)
H: Funext
A, B: pType
?f pt = pt
  -
H: Funext
A, B: pType
(psusp A ->** B) <~> (A ->** loops B) refine (equiv_adjointify
              (fun f => fmap loops f o* loop_susp_unit A)
              (fun g => loop_susp_counit B o* fmap psusp g) _ _).
H: Funext
A, B: pType
(fun x : A ->* loops B =>
 fmap loops (loop_susp_counit B o* fmap psusp x)
 o* loop_susp_unit A) == idmap
H: Funext
A, B: pType
(fun x : psusp A $-> B =>
 loop_susp_counit B
 o* fmap psusp (fmap loops x o* loop_susp_unit A)) ==
idmap
    +
H: Funext
A, B: pType
(fun x : A ->* loops B =>
 fmap loops (loop_susp_counit B o* fmap psusp x)
 o* loop_susp_unit A) == idmap intros g.
H: Funext
A, B: pType
g: A ->* loops B
fmap loops (loop_susp_counit B o* fmap psusp g)
o* loop_susp_unit A = g apply path_pforall.
H: Funext
A, B: pType
g: A ->* loops B
fmap loops (loop_susp_counit B o* fmap psusp g)
o* loop_susp_unit A ==* g
      refine (pmap_prewhisker _ (fmap_comp loops _ _) @* _).
H: Funext
A, B: pType
g: A ->* loops B
fmap loops (loop_susp_counit B) $o
fmap loops (fmap psusp g) o* loop_susp_unit A ==* g
      refine (pmap_compose_assoc _ _ _ @* _).
H: Funext
A, B: pType
g: A ->* loops B
fmap loops (loop_susp_counit B)
o* (fmap loops (fmap psusp g) o* loop_susp_unit A) ==*
g
      refine (pmap_postwhisker _ (loop_susp_unit_natural g)^* @* _).
H: Funext
A, B: pType
g: A ->* loops B
fmap loops (loop_susp_counit B)
o* (loop_susp_unit (loops B) o* g) ==* g
      refine ((pmap_compose_assoc _ _ _)^* @* _).
H: Funext
A, B: pType
g: A ->* loops B
fmap loops (loop_susp_counit B)
o* loop_susp_unit (loops B) o* g ==* g
      refine (pmap_prewhisker g (loop_susp_triangle1 B) @* _).
H: Funext
A, B: pType
g: A ->* loops B
pmap_idmap o* g ==* g
      apply pmap_postcompose_idmap.
    +
H: Funext
A, B: pType
(fun x : psusp A $-> B =>
 loop_susp_counit B
 o* fmap psusp (fmap loops x o* loop_susp_unit A)) ==
idmap intros f.
H: Funext
A, B: pType
f: psusp A $-> B
loop_susp_counit B
o* fmap psusp (fmap loops f o* loop_susp_unit A) = f apply path_pforall.
H: Funext
A, B: pType
f: psusp A $-> B
loop_susp_counit B
o* fmap psusp (fmap loops f o* loop_susp_unit A) ==* f
      refine (pmap_postwhisker _ (fmap_comp psusp _ _) @* _).
H: Funext
A, B: pType
f: psusp A $-> B
loop_susp_counit B
o* (fmap psusp (fmap loops f) $o
    fmap psusp (loop_susp_unit A)) ==* f
      refine ((pmap_compose_assoc _ _ _)^* @* _).
H: Funext
A, B: pType
f: psusp A $-> B
loop_susp_counit B o* fmap psusp (fmap loops f)
o* fmap psusp (loop_susp_unit A) ==* f
      refine (pmap_prewhisker _ (loop_susp_counit_natural f)^* @* _).
H: Funext
A, B: pType
f: psusp A $-> B
f o* loop_susp_counit (psusp A)
o* fmap psusp (loop_susp_unit A) ==* f
      refine (pmap_compose_assoc _ _ _ @* _).
H: Funext
A, B: pType
f: psusp A $-> B
f
o* (loop_susp_counit (psusp A)
    o* fmap psusp (loop_susp_unit A)) ==* f
      refine (pmap_postwhisker f (loop_susp_triangle2 A) @* _).
H: Funext
A, B: pType
f: psusp A $-> B
f o* pmap_idmap ==* f
      apply pmap_precompose_idmap.
  -
H: Funext
A, B: pType
equiv_adjointify
  (fun f : psusp A $-> B =>
   fmap loops f o* loop_susp_unit A)
  (fun g : A ->* loops B =>
   loop_susp_counit B o* fmap psusp g)
  ((fun g : A ->* loops B =>
    path_pforall
      (pmap_prewhisker (loop_susp_unit A)
         (fmap_comp loops (fmap psusp g)
            (loop_susp_counit B)) @*
       (pmap_compose_assoc
          (fmap loops (loop_susp_counit B))
          (fmap loops (fmap psusp g))
          (loop_susp_unit A) @*
        (pmap_postwhisker
           (fmap loops (loop_susp_counit B))
           (loop_susp_unit_natural g)^* @*
         ((pmap_compose_assoc
             (fmap loops (loop_susp_counit B))
             (loop_susp_unit (loops B)) g)^* @*
          (pmap_prewhisker g (loop_susp_triangle1 B) @*
           pmap_postcompose_idmap g))))))
   :
   (fun x : A ->* loops B =>
    fmap loops (loop_susp_counit B o* fmap psusp x)
    o* loop_susp_unit A) == idmap)
  ((fun f : psusp A $-> B =>
    path_pforall
      (pmap_postwhisker (loop_susp_counit B)
         (fmap_comp psusp (loop_susp_unit A)
            (fmap loops f)) @*
       ((pmap_compose_assoc (loop_susp_counit B)
           (fmap psusp (fmap loops f))
           (fmap psusp (loop_susp_unit A)))^* @*
        (pmap_prewhisker
           (fmap psusp (loop_susp_unit A))
           (loop_susp_counit_natural f)^* @*
         (pmap_compose_assoc f
            (loop_susp_counit (psusp A))
            (fmap psusp (loop_susp_unit A)) @*
          (pmap_postwhisker f (loop_susp_triangle2 A) @*
           pmap_precompose_idmap f))))))
   :
   (fun x : psusp A $-> B =>
    loop_susp_counit B
    o* fmap psusp (fmap loops x o* loop_susp_unit A)) ==
   idmap) pt = pt apply path_pforall.
H: Funext
A, B: pType
equiv_adjointify
  (fun f : psusp A $-> B =>
   fmap loops f o* loop_susp_unit A)
  (fun g : A ->* loops B =>
   loop_susp_counit B o* fmap psusp g)
  (fun g : A ->* loops B =>
   path_pforall
     (pmap_prewhisker (loop_susp_unit A)
        (fmap_comp loops (fmap psusp g)
           (loop_susp_counit B)) @*
      (pmap_compose_assoc
         (fmap loops (loop_susp_counit B))
         (fmap loops (fmap psusp g))
         (loop_susp_unit A) @*
       (pmap_postwhisker
          (fmap loops (loop_susp_counit B))
          (loop_susp_unit_natural g)^* @*
        ((pmap_compose_assoc
            (fmap loops (loop_susp_counit B))
            (loop_susp_unit (loops B)) g)^* @*
         (pmap_prewhisker g (loop_susp_triangle1 B) @*
          pmap_postcompose_idmap g))))))
  (fun f : psusp A $-> B =>
   path_pforall
     (pmap_postwhisker (loop_susp_counit B)
        (fmap_comp psusp (loop_susp_unit A)
           (fmap loops f)) @*
      ((pmap_compose_assoc (loop_susp_counit B)
          (fmap psusp (fmap loops f))
          (fmap psusp (loop_susp_unit A)))^* @*
       (pmap_prewhisker
          (fmap psusp (loop_susp_unit A))
          (loop_susp_counit_natural f)^* @*
        (pmap_compose_assoc f
           (loop_susp_counit (psusp A))
           (fmap psusp (loop_susp_unit A)) @*
         (pmap_postwhisker f (loop_susp_triangle2 A) @*
          pmap_precompose_idmap f)))))) pt ==* pt
    unfold equiv_adjointify, equiv_fun.
H: Funext
A, B: pType
fmap loops pt o* loop_susp_unit A ==* pt
    napply (pmap_prewhisker _ fmap_loops_pconst @* _).
H: Funext
A, B: pType
pconst o* loop_susp_unit A ==* pt
    tapply cat_zero_l.
Defined.

(** And its naturality is easy. *)

Definition loop_susp_adjoint_nat_r `{Funext} (A B B' : pType)
  (f : psusp A ->* B) (g : B ->* B') : loop_susp_adjoint A B' (g o* f)
  ==* fmap loops g o* loop_susp_adjoint A B f.
H: Funext
A, B, B': pType
f: psusp A ->* B
g: B ->* B'
loop_susp_adjoint A B' (g o* f) ==*
fmap loops g o* loop_susp_adjoint A B f
Proof.
H: Funext
A, B, B': pType
f: psusp A ->* B
g: B ->* B'
loop_susp_adjoint A B' (g o* f) ==*
fmap loops g o* loop_susp_adjoint A B f
  cbn.
H: Funext
A, B, B': pType
f: psusp A ->* B
g: B ->* B'
Build_pMap
  (fun p : ispointed_susp = ispointed_susp =>
   (ap g (point_eq f) @ point_eq g)^ @
   (ap (fun x : Susp A => g (f x)) p @
    (ap g (point_eq f) @ point_eq g)))
  (whiskerL (ap g (point_eq f) @ point_eq g)^
     (concat_1p (ap g (point_eq f) @ point_eq g)) @
   concat_Vp (ap g (point_eq f) @ point_eq g))
o* loop_susp_unit A ==*
Build_pMap
  (fun p : pt = pt =>
   (point_eq g)^ @ (ap g p @ point_eq g))
  (whiskerL (point_eq g)^ (concat_1p (point_eq g)) @
   concat_Vp (point_eq g))
o* (Build_pMap
      (fun p : ispointed_susp = ispointed_susp =>
       (point_eq f)^ @ (ap f p @ point_eq f))
      (whiskerL (point_eq f)^ (concat_1p (point_eq f)) @
       concat_Vp (point_eq f)) o* loop_susp_unit A)
  refine (_ @* pmap_compose_assoc _ _ _).
H: Funext
A, B, B': pType
f: psusp A ->* B
g: B ->* B'
Build_pMap
  (fun p : ispointed_susp = ispointed_susp =>
   (ap g (point_eq f) @ point_eq g)^ @
   (ap (fun x : Susp A => g (f x)) p @
    (ap g (point_eq f) @ point_eq g)))
  (whiskerL (ap g (point_eq f) @ point_eq g)^
     (concat_1p (ap g (point_eq f) @ point_eq g)) @
   concat_Vp (ap g (point_eq f) @ point_eq g))
o* loop_susp_unit A ==*
Build_pMap
  (fun p : pt = pt =>
   (point_eq g)^ @ (ap g p @ point_eq g))
  (whiskerL (point_eq g)^ (concat_1p (point_eq g)) @
   concat_Vp (point_eq g))
o* Build_pMap
     (fun p : ispointed_susp = ispointed_susp =>
      (point_eq f)^ @ (ap f p @ point_eq f))
     (whiskerL (point_eq f)^ (concat_1p (point_eq f)) @
      concat_Vp (point_eq f)) o* loop_susp_unit A
  apply pmap_prewhisker.
H: Funext
A, B, B': pType
f: psusp A ->* B
g: B ->* B'
Build_pMap
  (fun p : ispointed_susp = ispointed_susp =>
   (ap g (point_eq f) @ point_eq g)^ @
   (ap (fun x : Susp A => g (f x)) p @
    (ap g (point_eq f) @ point_eq g)))
  (whiskerL (ap g (point_eq f) @ point_eq g)^
     (concat_1p (ap g (point_eq f) @ point_eq g)) @
   concat_Vp (ap g (point_eq f) @ point_eq g)) ==*
Build_pMap
  (fun p : pt = pt =>
   (point_eq g)^ @ (ap g p @ point_eq g))
  (whiskerL (point_eq g)^ (concat_1p (point_eq g)) @
   concat_Vp (point_eq g))
o* Build_pMap
     (fun p : ispointed_susp = ispointed_susp =>
      (point_eq f)^ @ (ap f p @ point_eq f))
     (whiskerL (point_eq f)^ (concat_1p (point_eq f)) @
      concat_Vp (point_eq f))
  exact (fmap_comp loops f g).
Defined.

Definition loop_susp_adjoint_nat_l `{Funext} (A A' B : pType)
  (f : A ->* loops B) (g : A' ->* A) : (loop_susp_adjoint A' B)^-1 (f o* g)
  ==* (loop_susp_adjoint A B)^-1 f o* fmap psusp g.
H: Funext
A, A', B: pType
f: A ->* loops B
g: A' ->* A
(loop_susp_adjoint A' B)^-1 (f o* g) ==*
(loop_susp_adjoint A B)^-1 f o* fmap psusp g
Proof.
H: Funext
A, A', B: pType
f: A ->* loops B
g: A' ->* A
(loop_susp_adjoint A' B)^-1 (f o* g) ==*
(loop_susp_adjoint A B)^-1 f o* fmap psusp g
  cbn.
H: Funext
A, A', B: pType
f: A ->* loops B
g: A' ->* A
loop_susp_counit B
o* Build_pMap (functor_susp (fun x : A' => f (g x))) 1 ==*
loop_susp_counit B o* Build_pMap (functor_susp f) 1
o* Build_pMap (functor_susp g) 1
  refine (_ @* (pmap_compose_assoc _ _ _)^*).
H: Funext
A, A', B: pType
f: A ->* loops B
g: A' ->* A
loop_susp_counit B
o* Build_pMap (functor_susp (fun x : A' => f (g x))) 1 ==*
loop_susp_counit B
o* (Build_pMap (functor_susp f) 1
    o* Build_pMap (functor_susp g) 1)
  apply pmap_postwhisker.
H: Funext
A, A', B: pType
f: A ->* loops B
g: A' ->* A
Build_pMap (functor_susp (fun x : A' => f (g x))) 1 ==*
Build_pMap (functor_susp f) 1
o* Build_pMap (functor_susp g) 1
  exact (fmap_comp psusp g f).
Defined.

Instance is1natural_loop_susp_adjoint_r `{Funext} (A : pType)
  : Is1Natural (opyon (psusp A)) (opyon A o loops)
      (loop_susp_adjoint A).
H: Funext
A: pType
Is1Natural (opyon (psusp A)) (opyon A o loops)
  (fun B : pType => loop_susp_adjoint A B)
Proof.
H: Funext
A: pType
Is1Natural (opyon (psusp A)) (opyon A o loops)
  (fun B : pType => loop_susp_adjoint A B)
  snapply Build_Is1Natural.
H: Funext
A: pType
forall (a a' : pType) (f : a $-> a'),
(fun B : pType => pointed_fun (loop_susp_adjoint A B))
  a' $o fmap (opyon (psusp A)) f $==
fmap (opyon A o loops) f $o
(fun B : pType => pointed_fun (loop_susp_adjoint A B))
  a
  intros B B' g f.
H: Funext
A, B, B': pType
g: B $-> B'
f: opyon (psusp A) B
(loop_susp_adjoint A B' $o fmap (opyon (psusp A)) g) f =
(fmap (opyon A o loops) g $o loop_susp_adjoint A B) f
  refine ( _ @ cat_assoc_strong _ _ _).
H: Funext
A, B, B': pType
g: B $-> B'
f: opyon (psusp A) B
(loop_susp_adjoint A B' $o fmap (opyon (psusp A)) g) f =
fmap loops g $o fmap loops f $o loop_susp_unit A
  refine (ap (fun x => x o* loop_susp_unit A) _).
H: Funext
A, B, B': pType
g: B $-> B'
f: opyon (psusp A) B
fmap loops (fmap (opyon (psusp A)) g f) =
fmap loops g $o fmap loops f
  apply path_pforall.
H: Funext
A, B, B': pType
g: B $-> B'
f: opyon (psusp A) B
fmap loops (fmap (opyon (psusp A)) g f) ==*
fmap loops g $o fmap loops f
  tapply (fmap_comp loops).
Defined.

Lemma natequiv_loop_susp_adjoint_r `{Funext} (A : pType)
  : NatEquiv (opyon (psusp A)) (opyon A o loops).
H: Funext
A: pType
NatEquiv (opyon (psusp A)) (opyon A o loops)
Proof.
H: Funext
A: pType
NatEquiv (opyon (psusp A)) (opyon A o loops)
  rapply Build_NatEquiv.
Defined.