\import Equiv
\import Equiv.HalfAdjoint
\import Equiv.Univalence
\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)) : Equiv (x *) \elim c
      | inP base=x => rewriteI (path (\lam i y => (inv (base-left y) *> pmap (`* y) base=x) @ i)) 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)) : Equiv (__ * x) \elim c
      | inP base=x => rewriteI (path (\lam i y => (inv (base-right y) *> pmap (y *) base=x) @ i)) 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 (QEquiv-to-= Sphere1-equiv) Circle_HSpace

\func hopf {A : HSpaceConn} (x : Susp A) : \Type \elim x
  | north => A
  | south => A
  | pglue a => Equiv-to-= (HSpaceConn-left a)
  \where
    \func total-equiv {A : HSpaceConn} : (\Sigma (x : Susp A) (hopf x)) = Join A A
      => inv (PushoutData.flattening hopf) *> QEquiv-to-= 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) => 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) => 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') => 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