\import Equiv
\import Equiv.Sigma
\import Function.Iterate
\import Homotopy.HLevel
\import Logic
\import Logic.Unique
\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
\func Loop-Func {X Y : Pointed} (f : X ->* Y) : Loop X ->* Loop Y
=> (\lam z => inv f.2 *> pmap f.1 z *> f.2, pmap (_ *>) (idp_*> _) *> inv_*> _)
\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.{u} {X : \Type u}
(n : Nat)
(c : \Pi (x0 : X) -> Contr (iterl {Pointed.{u}} (Loop __) n (\new Pointed X x0)))
: X ofHLevel_-1+ n \elim n
| 0 => toProp (isContr'=>isProp c)
| suc n => \lam x x' => loop-level-iter n (\lam x=x' => Jl (\lam x'' x=x'' => Contr (iterl {Pointed.{u}} (Loop __) n (\new Pointed (x = x'') x=x''))) (c x) x=x')
\lemma loop-level-iter-inv.{u} {X : \Type u} (n : Nat) (h : X ofHLevel_-1+ n) (x0 : X)
: Contr (iterl {Pointed.{u}} (Loop __) n (\new Pointed X x0)) \elim n
| 0 => isProp=>isContr (ToProp.fromProp h) x0
| suc n => loop-level-iter-inv n (h x0 x0) idp
\func SuspLoopEquiv.{u} (A B : Pointed.{u}) : (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 (QEquiv_= (IsEquiv.toQEquiv (Susp.pushout A).pushout-univ)) >==
(\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))) ==< QEquiv_= (contr-left (rsigma base)) >==
(\Sigma (b2 : B) (A -> base = b2)) ==< inv (QEquiv_= (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))) ==< QEquiv_= (contr-left (lsigma base)) >==
(\Sigma (g : A -> Loop B) (g base = base)) `qed
\func SphereLoopEquiv.{u} (n : Nat) (B : Pointed.{u}) : (Sphere.pointed n ->* B) = iterl {Pointed.{u}} (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)
\func Omega^.{u} (n : Nat) (X : Pointed.{u}) : Pointed.{u}
=> iterr {Pointed.{u}} (Loop __) n X
\func Omega^-Func.{u} (n : Nat) {X Y : Pointed.{u}} (f : X ->* Y) : Omega^ n X ->* Omega^ n Y \elim n
| 0 => f
| suc n => Loop-Func (Omega^-Func n f)