Loop

\import Equiv.Sigma
\import Function
\import HLevel
\import Homotopy.Pointed
\import Homotopy.Pushout
\import Homotopy.Sphere
\import Homotopy.Square
\import Homotopy.Suspension
\import Meta
\import Paths
\import Paths.Meta

\instance Loop (X : Pointed) : Pointed
  | E => base = {X} base
  | base => idp

\lemma loop-level {X : \Type}
                  (n : Nat)
                  (p : \Pi (x0 : X) -> (x0 = x0) ofHLevel_-1+ n)
  : X ofHLevel_-1+ suc n
  => \lam x x' => hLevel-inh n (later rewriteI __ (p x))

\lemma loop-level-iter {X : \Type}
                       (n : Nat)
                       (c : \Pi (x0 : X) -> Contr (iterl Loop n (\new Pointed X x0)))
  : X ofHLevel_-1+ n \elim n
  | 0 => isContr'=>isProp c
  | suc n => \lam x x' => loop-level-iter n (\lam x=x' => Jl (\lam x'' x=x'' => Contr (iterl Loop n (\new Pointed (x = x'') x=x''))) (c x) x=x')

\lemma loop-level-iter-inv {X : \Type} (n : Nat) (h : X ofHLevel_-1+ n) (x0 : X)
  : Contr (iterl Loop n (\new Pointed X x0)) \elim n
  | 0 => isProp=>isContr h x0
  | suc n => loop-level-iter-inv n (h x0 x0) idp

\func SuspLoopEquiv (A B : Pointed) : (Susp.pointed A ->* B) = (A ->* Loop B) =>
  \let S => Square { | Y => B | U => A | V => \Sigma | X => \Sigma | uv _ => () | ux _ => () } \in
  (\Sigma (f : Susp A -> B) (f north = base))                                              ==< sigma-left.path-func (equiv= (pushout-univ {Susp.pushout A} {B})) >==
  (\Sigma (s : S) (Square.vy {s} () = base))                                               ==< path (iso {\Sigma (s : S) (Square.vy {s} () = base)}
                                                                                                         {\Sigma (p : \Sigma (b1 : B) (b1 = base)) (\Sigma (b2 : B) (A -> p.1 = b2))}
                                                                                                         (\lam p => \let s : Square => p.1 \in ((s.vy (), p.2), (s.xy (), s.sqcomm)))
                                                                                                         (\lam q => (\new Square { | vy _ => q.1.1 | xy _ => q.2.1 | sqcomm => q.2.2 }, q.1.2))
                                                                                                         idpe idpe) >==
  (\Sigma (p : \Sigma (b1 : B) (b1 = base)) (\Sigma (b2 : B) (A -> p.1 = b2)))             ==< equiv= (contr-left (rsigma base)) >==
  (\Sigma (b2 : B) (A -> base = b2))                                                       ==< inv (equiv= (contr-right (\lam (p : \Sigma (b2 : B) (A -> base = b2)) => lsigma (p.2 base)))) >==
  (\Sigma (p : \Sigma (b2 : B) (A -> base = b2)) (\Sigma (q : base = p.1) (p.2 base = q))) ==< path (iso {\Sigma (p : \Sigma (b2 : B) (A -> base = b2)) (\Sigma (q : base = p.1) (p.2 base = q))}
                                                                                                         {\Sigma (p : \Sigma (b2 : B) (base = b2)) (\Sigma (g : A -> base = p.1) (g base = p.2))}
                                                                                                         (\lam p => ((p.1.1,p.2.1),(p.1.2,p.2.2)))
                                                                                                         (\lam q => ((q.1.1,q.2.1),(q.1.2,q.2.2)))
                                                                                                         idpe idpe) >==
  (\Sigma (p : \Sigma (b2 : B) (base = b2)) (\Sigma (g : A -> base = p.1) (g base = p.2))) ==< equiv= (contr-left (lsigma base)) >==
  (\Sigma (g : A -> Loop B) (g base = base))                                               `qed

\func SphereLoopEquiv (n : Nat) (B : Pointed) : (Sphere.pointed n ->* B) = iterl Loop n B \elim n
  | 0 => \let smap (b : B) (s : Sphere 0) : B => \case s \with { | pinl _ => base | pinr _ => b | pglue () _ }
         \in path (iso {Sphere.pointed 0 ->* B} {B}
                       (__.1 south)
                       (\lam b => (smap b, idp))
                       (\lam p => ->*.ext {Sphere.pointed 0} (\lam s =>
                           \case \elim s \return smap (p.1 south) s = p.1 s \with {
                             | pinl _ => inv p.2
                             | pinr _ => idp
                             | pglue () _
                           }) (inv_*> p.2))
                       (\lam b => idp))
  | suc n => SuspLoopEquiv (Sphere.pointed n) B *> SphereLoopEquiv n (Loop B)