From HoTT Require Import Basics.From HoTT Require Import Basics.
Require Import Types.
From HoTT.WildCat Require Import Core Universe PointedCat NatTrans Yoneda.
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 p0 : functor_susp f South = functor_susp g South => p0 = 1)
      (internal_paths_rew_r
         (fun p0 : functor_susp f South = functor_susp f North =>
          p0 @ ap (functor_susp g) (merid x) = 1)
         (internal_paths_rew_r
            (fun
               p0 : Susp_rec North South (fun x0 : X => merid (f x0)) North =
                    Susp_rec North South (fun x0 : X => merid (f x0)) South =>
             p0^ @ ap (functor_susp g) (merid x) = 1)
            (internal_paths_rew_r
               (fun
                  p0 : 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))^ @ p0 = 1)
               (let p0 := p x in
                let y := g x in
                match
                  p0 in (_ = y0) return ((merid (f x))^ @ 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 x0 : a => g (f x0)) 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 x0 : a => g (f x0))) (merid x))^ @ 1) @
ap (fun x0 : Susp a => functor_susp g (functor_susp f x0)) (merid x) = 1
      rewrite concat_p1; apply moveR_Vp.
a, b, c: Type
f: a -> b
g: b -> c
x: a
ap (fun x0 : Susp a => functor_susp g (functor_susp f x0)) (merid x) =
ap (functor_susp (fun x0 : a => g (f x0))) (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 x0 : b => merid (g x0))
                              North =
                            Susp_rec North South (fun x0 : b => merid (g x0))
                              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 (g (f x0))) North =
                               Susp_rec North South
                                 (fun x0 : a => merid (g (f x0))) South =>
                         merid (g (f x)) = 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 p0 : point0 = point0 => 1 @ (ap f p0 @ 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 p0 : point0 = point0 => 1 @ (ap f p0 @ 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 p0 : point0 = point0 => 1 @ (ap f p0 @ 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 @ (ap f x0 @ 1)))
                            North =
                          Susp_rec North South
                            (fun x0 : point0 = point0 =>
                             merid (1 @ (ap f x0 @ 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 x0 : X => merid x0 @ (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 x0 : X => merid x0 @ (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
      lhs' exact (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
      lhs' apply 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
      lhs' exact (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
      lhs_V' apply 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
      lhs' exact (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
      lhs' exact (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
      lhs_V' apply 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
      lhs' exact (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
      lhs' apply 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
      lhs' exact (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
      (phomotopy_transitive'
         (fmap loops (loop_susp_counit B o* fmap psusp g) o* loop_susp_unit A)
         (fmap loops (loop_susp_counit B) $o fmap loops (fmap psusp g)
          o* loop_susp_unit A)
         g
         (pmap_prewhisker (loop_susp_unit A)
            (fmap_comp loops (fmap psusp g) (loop_susp_counit B)))
         (phomotopy_transitive'
            (fmap loops (loop_susp_counit B) $o fmap loops (fmap psusp g)
             o* loop_susp_unit A)
            (fmap loops (loop_susp_counit B)
             o* (fmap loops (fmap psusp g) o* loop_susp_unit A))
            g
            (pmap_compose_assoc (fmap loops (loop_susp_counit B))
               (fmap loops (fmap psusp g)) (loop_susp_unit A))
            (phomotopy_transitive'
               (fmap loops (loop_susp_counit B)
                o* (fmap loops (fmap psusp g) o* loop_susp_unit A))
               (fmap loops (loop_susp_counit B)
                o* (loop_susp_unit (loops B) o* g))
               g
               (pmap_postwhisker (fmap loops (loop_susp_counit B))
                  (loop_susp_unit_natural g)^*)
               (phomotopy_transitive'
                  (fmap loops (loop_susp_counit B)
                   o* (loop_susp_unit (loops B) o* g))
                  (fmap loops (loop_susp_counit B)
                   o* loop_susp_unit (loops B) o* g)
                  g
                  (phomotopy_symmetric'
                     (fmap loops (loop_susp_counit B)
                      o* loop_susp_unit (loops B) o* g)
                     (fmap loops (loop_susp_counit B)
                      o* (loop_susp_unit (loops B) o* g))
                     (pmap_compose_assoc (fmap loops (loop_susp_counit B))
                        (loop_susp_unit (loops B)) g))
                  (phomotopy_transitive'
                     (fmap loops (loop_susp_counit B)
                      o* loop_susp_unit (loops B) o* g)
                     (pmap_idmap o* g) 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
      (phomotopy_transitive'
         (loop_susp_counit B o* fmap psusp (fmap loops f o* loop_susp_unit A))
         (loop_susp_counit B
          o* (fmap psusp (fmap loops f) $o fmap psusp (loop_susp_unit A)))
         f
         (pmap_postwhisker (loop_susp_counit B)
            (fmap_comp psusp (loop_susp_unit A) (fmap loops f)))
         (phomotopy_transitive'
            (loop_susp_counit B
             o* (fmap psusp (fmap loops f) $o fmap psusp (loop_susp_unit A)))
            (loop_susp_counit B o* fmap psusp (fmap loops f)
             o* fmap psusp (loop_susp_unit A))
            f
            (phomotopy_symmetric'
               (loop_susp_counit B o* fmap psusp (fmap loops f)
                o* fmap psusp (loop_susp_unit A))
               (loop_susp_counit B
                o* (fmap psusp (fmap loops f) $o
                    fmap psusp (loop_susp_unit A)))
               (pmap_compose_assoc (loop_susp_counit B)
                  (fmap psusp (fmap loops f)) (fmap psusp (loop_susp_unit A))))
            (phomotopy_transitive'
               (loop_susp_counit B o* fmap psusp (fmap loops f)
                o* fmap psusp (loop_susp_unit A))
               (f o* loop_susp_counit (psusp A)
                o* fmap psusp (loop_susp_unit A))
               f
               (pmap_prewhisker (fmap psusp (loop_susp_unit A))
                  (loop_susp_counit_natural f)^*)
               (phomotopy_transitive'
                  (f o* loop_susp_counit (psusp A)
                   o* fmap psusp (loop_susp_unit A))
                  (f
                   o* (loop_susp_counit (psusp A)
                       o* fmap psusp (loop_susp_unit A)))
                  f
                  (pmap_compose_assoc f (loop_susp_counit (psusp A))
                     (fmap psusp (loop_susp_unit A)))
                  (phomotopy_transitive'
                     (f
                      o* (loop_susp_counit (psusp A)
                          o* fmap psusp (loop_susp_unit A)))
                     (f o* pmap_idmap) f
                     (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
     (phomotopy_transitive'
        (fmap loops (loop_susp_counit B o* fmap psusp g) o* loop_susp_unit A)
        (fmap loops (loop_susp_counit B) $o fmap loops (fmap psusp g)
         o* loop_susp_unit A)
        g
        (pmap_prewhisker (loop_susp_unit A)
           (fmap_comp loops (fmap psusp g) (loop_susp_counit B)))
        (phomotopy_transitive'
           (fmap loops (loop_susp_counit B) $o fmap loops (fmap psusp g)
            o* loop_susp_unit A)
           (fmap loops (loop_susp_counit B)
            o* (fmap loops (fmap psusp g) o* loop_susp_unit A))
           g
           (pmap_compose_assoc (fmap loops (loop_susp_counit B))
              (fmap loops (fmap psusp g)) (loop_susp_unit A))
           (phomotopy_transitive'
              (fmap loops (loop_susp_counit B)
               o* (fmap loops (fmap psusp g) o* loop_susp_unit A))
              (fmap loops (loop_susp_counit B)
               o* (loop_susp_unit (loops B) o* g))
              g
              (pmap_postwhisker (fmap loops (loop_susp_counit B))
                 (loop_susp_unit_natural g)^*)
              (phomotopy_transitive'
                 (fmap loops (loop_susp_counit B)
                  o* (loop_susp_unit (loops B) o* g))
                 (fmap loops (loop_susp_counit B) o* loop_susp_unit (loops B)
                  o* g)
                 g
                 (phomotopy_symmetric'
                    (fmap loops (loop_susp_counit B)
                     o* loop_susp_unit (loops B) o* g)
                    (fmap loops (loop_susp_counit B)
                     o* (loop_susp_unit (loops B) o* g))
                    (pmap_compose_assoc (fmap loops (loop_susp_counit B))
                       (loop_susp_unit (loops B)) g))
                 (phomotopy_transitive'
                    (fmap loops (loop_susp_counit B)
                     o* loop_susp_unit (loops B) o* g)
                    (pmap_idmap o* g) g
                    (pmap_prewhisker g (loop_susp_triangle1 B))
                    (pmap_postcompose_idmap g)))))))
  (fun f : psusp A $-> B =>
   path_pforall
     (phomotopy_transitive'
        (loop_susp_counit B o* fmap psusp (fmap loops f o* loop_susp_unit A))
        (loop_susp_counit B
         o* (fmap psusp (fmap loops f) $o fmap psusp (loop_susp_unit A)))
        f
        (pmap_postwhisker (loop_susp_counit B)
           (fmap_comp psusp (loop_susp_unit A) (fmap loops f)))
        (phomotopy_transitive'
           (loop_susp_counit B
            o* (fmap psusp (fmap loops f) $o fmap psusp (loop_susp_unit A)))
           (loop_susp_counit B o* fmap psusp (fmap loops f)
            o* fmap psusp (loop_susp_unit A))
           f
           (phomotopy_symmetric'
              (loop_susp_counit B o* fmap psusp (fmap loops f)
               o* fmap psusp (loop_susp_unit A))
              (loop_susp_counit B
               o* (fmap psusp (fmap loops f) $o fmap psusp (loop_susp_unit A)))
              (pmap_compose_assoc (loop_susp_counit B)
                 (fmap psusp (fmap loops f)) (fmap psusp (loop_susp_unit A))))
           (phomotopy_transitive'
              (loop_susp_counit B o* fmap psusp (fmap loops f)
               o* fmap psusp (loop_susp_unit A))
              (f o* loop_susp_counit (psusp A)
               o* fmap psusp (loop_susp_unit A))
              f
              (pmap_prewhisker (fmap psusp (loop_susp_unit A))
                 (loop_susp_counit_natural f)^*)
              (phomotopy_transitive'
                 (f o* loop_susp_counit (psusp A)
                  o* fmap psusp (loop_susp_unit A))
                 (f
                  o* (loop_susp_counit (psusp A)
                      o* fmap psusp (loop_susp_unit A)))
                 f
                 (pmap_compose_assoc f (loop_susp_counit (psusp A))
                    (fmap psusp (loop_susp_unit A)))
                 (phomotopy_transitive'
                    (f
                     o* (loop_susp_counit (psusp A)
                         o* fmap psusp (loop_susp_unit A)))
                    (f o* pmap_idmap) f
                    (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
    lhs' exact (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)
  rhs_V' apply 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
  rhs' apply 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
  rhs_V rapply 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.