\import Algebra.Group
\import Algebra.Meta
\import Algebra.Monoid
\import Algebra.Pointed (ide)
\import Function.Meta
\import Homotopy.Cube
\import Logic
\import Meta
\import Paths
\import Equiv (QEquiv, Retraction, Section)
\import Equiv
\import Equiv.Univalence.Set
\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 {
    \lemma loop-comp {G : Group} (g g' : G) : path (loop g) *> path (loop g') = path (loop (g * g'))
      => movePath2 $ coe2 (Cube2.equality (path (loop g)) (path (loop (g * g'))) idp (path (loop g'))) right (path (\lam j => path (\lam i => relation g g' i j))) left

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

\lemma 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

\lemma movePath2 {A : \1-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 rMul-functorial {G : Group} (g g' : G) : (\lam x => rightMulEquiv g' (rightMulEquiv g x)) = rightMulEquiv (g * g')
  => ext (\lam x => *-assoc)

\lemma equivPathComposition.{u} {G : Group.{u}} (g g' : G) : QEquiv-to-= (rightMulEquiv g) *> QEquiv-to-= (rightMulEquiv g') = QEquiv-to-= (rightMulEquiv (g * g'))
  => QEquiv-to-=-functorial (rightMulEquiv g) (rightMulEquiv g') *> pmap QEquiv-to-= (QEquiv.equals {G} {G} {_} {rightMulEquiv (g * g')} \lam a => *-assoc)

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

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

\func decode.{u} {G : Group.{u}} (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.{u} {G : Group.{u}} (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.{u} {G : Group.{u}} {x : K1 G} (p : base = x) : decode x (encode x p) = p
  | idp => K1.loop-ide

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

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