```\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))```