\import Algebra.Group
\import Algebra.Monoid
\import Algebra.Pointed (ide)
\import Homotopy.Cube
\import Logic
\import Paths
\import Equiv (QEquiv, Retraction, Section)
\import Equiv
\import Equiv.Univalence
\import Paths.Meta

\truncated \data K1 (G : Group) : \1-Type
  | base
  | loop G : base = base
  | relation (g g' : G) (i : I) (j : I) \elim i, j {
    | left, j => base
    | right, j => loop g' j
    | i, left => loop g i
    | i, right => loop (g * g') i
  }
  \where {
    \func loop-comp {G : Group} (g g' : G) : path (loop g) *> path (loop g') = path (loop (g * g'))
      => movePath2 (ret {=-to-Equiv (Cube2.equality (path (loop g)) (path (loop (g * g'))) idp (path (loop g')))}
                             (path (\lam j => path (\lam i => relation g g' i j))))

    \func loop-ide {G : Group} : path (loop (ide {G})) = idp
      => idp-lemma (path (loop ide)) (path (loop ide)) (loop-comp ide ide *> simplify)
      \where {
        \func idp-lemma {A : \Type} {a a' : A} (p : a = a') (q : a = a) (h : q *> p = p) : q = idp \elim p
          | idp => h
      }

  }

\func movePath1 {A : \1-Type} {a a' a'' : A} {p : a = a'} {q : a' = a''} {r : a = a''} (h : p *> q = r) : p = r *> inv q
  => (inv (pmap (p *>) (*>_inv q)) *> inv (*>-assoc p q (inv q))) *> pmap (`*> inv q) h

\func movePath2 {A : \Type} {a a' a'' : A} {p : a = a'} {q : a' = a''} {r : a = a''} (h : p = r *> inv q) : p *> q = r
  => pmap (`*> q) h *> *>-assoc r (inv q) q *> pmap (r *>) (inv_*> q)

\func leftMulEquiv {G : Group} (g : G) : QEquiv (g *) \cowith
  | ret => inverse g *
  | ret_f h => simplify
  | f_sec h => simplify

\func rightMulEquiv {G : Group} (g : G) : QEquiv (`* g) \cowith
  | ret => `* (inverse g)
  | ret_f h => simplify
  | f_sec h => simplify

\func =-to-Equiv-functorial {A B C : \Type} (p : A = B) (q : B = C)
  : =-to-Equiv (p *> q) = (=-to-Equiv p `transEquiv` =-to-Equiv q) \elim q
  | idp => prop-isProp {Equiv (=-to-Equiv p)} (=-to-Equiv p) (=-to-Equiv p `transEquiv` =-to-Equiv idp)

\func Equiv-to-=-functorial {A B C : \Type} (e1 : Equiv {A} {B}) (e2 : Equiv {B} {C})
  : Equiv-to-= e1 *> Equiv-to-= e2 = Equiv-to-= (e1 `transEquiv` e2)
  => Equiv-to-= e1 *> Equiv-to-= e2                                             ==< inv (ret_f {univalence {A} {C}} (Equiv-to-= e1 *> Equiv-to-= e2)) >==
     Equiv-to-= (=-to-Equiv (Equiv-to-= e1 *> Equiv-to-= e2))                   ==< pmap Equiv-to-= (=-to-Equiv-functorial (Equiv-to-= e1) (Equiv-to-= e2)) >==
     Equiv-to-= (=-to-Equiv (Equiv-to-= e1) `transEquiv` =-to-Equiv (Equiv-to-= e2)) ==< pmap (\lam x => Equiv-to-= (x `transEquiv` =-to-Equiv (Equiv-to-= e2))) (f_sec {univalence {A} {B}} e1) >==
     Equiv-to-= (e1 `transEquiv` =-to-Equiv (Equiv-to-= e2))                         ==< pmap (\lam x => Equiv-to-= (e1 `transEquiv` x)) (f_sec {univalence {B} {C}} e2) >==
     Equiv-to-= (e1 `transEquiv` e2) `qed

\func rMul-functorial {G : Group} (g g' : G) : (\lam x => rightMulEquiv g' (rightMulEquiv g x)) = rightMulEquiv (g * g')
  => ext (\lam x => *-assoc)

\func equivFibr {G : Group} (g g' : G) (i : I) => Equiv {G} {G} (rMul-functorial g g' @ i)

\lemma compToMult {G : Group} (g g' : G) : Path (equivFibr g g') (rightMulEquiv g `transEquiv` rightMulEquiv g') (rightMulEquiv (g * g'))
  => prop-dpi _ _ _

\lemma equivPathComposition {G : Group} (g g' : G) : Equiv-to-= (rightMulEquiv g) *> Equiv-to-= (rightMulEquiv g') = Equiv-to-= (rightMulEquiv (g * g'))
  => Equiv-to-= (rightMulEquiv g) *> Equiv-to-= (rightMulEquiv g')  ==< Equiv-to-=-functorial (rightMulEquiv g) (rightMulEquiv g') >==
     Equiv-to-= (rightMulEquiv g `transEquiv` rightMulEquiv g')     ==< pmap Equiv-to-= (compToMult g g') >==
     Equiv-to-= (rightMulEquiv (g * g'))                            `qed

\func code {G : Group} (x : K1 G) : \Set \elim x
  | base => G
  | loop g => Equiv-to-= (rightMulEquiv g)
  | relation g g' i j => Cube2.map (Equiv-to-= (rightMulEquiv g)) (Equiv-to-= (rightMulEquiv (g * g'))) idp (Equiv-to-= (rightMulEquiv g'))
                                   (movePath1 (equivPathComposition g g')) @ j @ i

\func encode {G : Group} (x : K1 G) (p : base = x) : code x
   => transport code p ide

\func decode {G : Group} (x : K1 G) : code x -> base = x \elim x
  | base => \lam c => path (loop c)
  | loop g => pathOver (decode_loop_homo g)
  \where {
    \func wind {G : Group} (g : G) : base {G} = base => path (loop g)

    \func decode_loop_homo {G : Group} (g : G) : transport (\lam x => code {G} x -> base = x) (wind g) wind = wind
      => simp_coe (\lam c => simp_coe (K1.loop-comp c g))
  }

\func encode_decode {G : Group} {x : K1 G} (p : base = x) : decode x (encode x p) = p
  | idp => K1.loop-ide

\func decode_encode {G : Group} (x : K1 G) (c : code x) : encode x (decode x c) = c \elim x
  | base => ide-left

\func Loop_K1 {G : Group} : (base {G} = base) = G
  => path (iso (encode base) (decode base) (encode_decode {G} {base}) (decode_encode base))