\import Equiv
\import Equiv.HalfAdjoint
\import Homotopy.Connected
\import Homotopy.Cube
\import Homotopy.Join
\import Homotopy.Pointed
\import Homotopy.Pushout
\import Homotopy.Sphere
\import Homotopy.Sphere.Circle
\import Homotopy.Suspension
\import Logic
\import Paths
\import Paths.Meta

\class HSpace \extends Pointed
  | \infixl  * : E -> E -> E
  | base-left (x : E) : base * x = x
  | base-right (x : E) : x * base = x

\class HSpaceConn \extends HSpace, Connected0

-- | For every point {x} in a connected H-space, ``(x *)`` is an equivalence.
\lemma HSpaceConn-left {A : HSpaceConn} (x : A) => lem (isConn0 base x)
  \where {
    -- | If a point {x} in an H-space belongs to the same connected component as {base}, then ``(x *)`` is an equivalence.
    \lemma lem {A : HSpace} {x : A} (c : TruncP (base = x)) : IsEquiv (x *) \elim c
      | inP base=x => rewriteI (path (\lam i y => (inv (base-left y) *> pmap (* y) base=x) @ i)) (inP idEquiv)
  }

-- | For every point {x} in a connected H-space, ``(* x)`` is an equivalence.
\lemma HSpaceConn-right {A : HSpaceConn} (x : A) => lem (isConn0 base x)
  \where {
    -- | If a point {x} in an H-space belongs to the same connected component as {base}, then ``(* x)`` is an equivalence.
    \lemma lem {A : HSpace} {x : A} (c : TruncP (base = x)) : IsEquiv (__ * x) \elim c
      | inP base=x => rewriteI (path (\lam i y => (inv (base-right y) *> pmap (y *) base=x) @ i)) (inP idEquiv)
  }

\instance Circle_HSpace : HSpaceConn Sphere1
  | base => base1
  | * => mult
  | base-left _ => idp
  | base-right => mult-right
  | isConn0 (base1) (base1) => inP idp
  \where {
    \open Sphere1(ploop)

    \func circle-loop (y : Sphere1) : y = y
      | base1 => path loop
      | loop => Cube2.map ploop ploop ploop ploop (inv (<*_idp ploop) *> pmap (ploop <*) (inv (*>_inv ploop)))

    \func mult (x y : Sphere1) : Sphere1 \elim x
      | base1 => y
      | loop => circle-loop y

    \func mult-right (x : Sphere1) : mult x base1 = x
      | base1 => idp
      | loop i => idp
  }

\instance Sphere1_HSpace : HSpaceConn (Sphere ) => rewriteI (path (QEquiv_= Sphere1-equiv)) Circle_HSpace

\func hopf.{u} {A : HSpaceConn.{u}} (x : Susp A) : \Type u \elim x
  | north => A
  | south => A
  | pglue a => QEquiv_= (IsEquiv.toQEquiv (HSpaceConn-left a))
  \where
    \func total-equiv.{u} {A : HSpaceConn.{u}} : (\Sigma (x : Susp A) (hopf x)) = Join A A
      => inv (PushoutData.flattening hopf) *> QEquiv_= {total A} total_join-equiv
      \where {
        \open PushoutData(ppglue)

        \func total (A : HSpace) => PushoutData {\Sigma A A} {\Sigma (\Sigma) A} {\Sigma (\Sigma) A} (\lam p => ((),p.)) (\lam p => ((), p. * p.))

        \func total_join-equiv {A : HSpaceConn} : QEquiv {total A} {Join A A} \cowith
          | f => totalJoin
          | ret => joinTotal
          | ret_f => totalJoinTotal
          | f_sec => joinTotalJoin

        \func totalJoin {A : HSpace} (x : total A) : Join A A
          | pinl (_,a) => jinl a
          | pinr (_,a) => jinr a
          | pglue (a,a') i => pglue (a', a * a') i

        \func joinTotal {A : HSpaceConn} (x : Join A A) : total A
          | jinl a => pinl ((),a)
          | jinr a => pinr ((),a)
          | pglue (a,a') =>
            \let e : HAEquiv (* a) => IsEquiv.toQEquiv (HSpaceConn-right a)
            \in ppglue (e.sec a', a) *> pmap (\lam x => pinr ((),x)) (e.f_sec a')

        \func joinTotalJoin {A : HSpaceConn} (x : Join A A) : totalJoin (joinTotal x) = x
          | jinl a => idp
          | jinr a => idp
          | pglue (a,a') i =>
            \have | e : HAEquiv (* a) => IsEquiv.toQEquiv (HSpaceConn-right a)
                  | p =>
                    pmap totalJoin (ppglue (e.sec a', a) *> pmap (\lam y => pinr ((),y)) (e.f_sec a')) ==< pmap_*>-comm totalJoin (ppglue (e.sec a', a)) (pmap (\lam y => pinr ((),y)) (e.f_sec a')) >==
                    jglue a (e.sec a' * a) *> pmap jinr (e.f_sec a')                                   ==< Jl (\lam x p => jglue a (e.sec a' * a) *> pmap jinr p = jglue a x) idp (e.f_sec a') >==
                    jglue a a'                                                                         `qed
            \in path (p @ __ @ i)

        \func totalJoinTotal {A : HSpaceConn} (x : total A) : joinTotal (totalJoin x) = x \elim x
          | pinl (_,a) => idp
          | pinr (_,a) => idp
          | pglue (a,a') i =>
            \let | e : HAEquiv (* a') => IsEquiv.toQEquiv (HSpaceConn-right a')
                 | s => ppglue (e.ret (a * a'), a')
                 | p =>
                   s *> pmap (\lam y => pinr ((),y)) (e.f_sec (a * a')) ==< pmap (\lam p => s *> pmap (\lam y => pinr ((),y)) p) (inv (e.f_ret_f=f_sec_f a)) >==
                   s *> pmap (\lam y => pinr ((), y * a')) (e.ret_f a)  ==< Jl (\lam x p => s *> pmap (\lam y => pinr ((), y * a')) p = ppglue (x,a')) idp (e.ret_f a) >==
                   ppglue (a,a')                                        `qed
            \in path (p @ __ @ i)
      }

\func hopfS2 (x : Sphere ) => hopf x
  \where
    \func total-equiv =>
      (\Sigma (x : Sphere ) (hopfS2 x)) ==< hopf.total-equiv >==
      Join (Sphere ) (Sphere )         ==< Join_Sphere (Sphere )  >==
      Sphere                            `qed