\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)
`