K-ind

Author: 5HT

library/mathematics/homotopy/KGn.anders

@@ -16,6 +16,9 @@ def Q-K1 (G : group) (x y : 𝟏) (r1 r2 : R¯ 𝟏 (R-K1 G) x y) : U
       (prod (Path (R¯ 𝟏 (R-K1 G) x y) r1 (loop-K1 G G.2.1.2.2.1))
       (Path (R¯ 𝟏 (R-K1 G) x y) r2 (idp (quot 𝟏 (R-K1 G)) (quot₁ 𝟏 (R-K1 G) ★))))
 def K1 (G : group) : U := ‖_‖₁ (2-quot 𝟏 (R-K1 G) (Q-K1 G))
+def K1-point' (G : group) : K1 G := trunc₁ (2-quot 𝟏 (R-K1 G) (Q-K1 G)) two (2-quot₁ 𝟏 (R-K1 G) (Q-K1 G) ★)
+def K1-loop'  (G : group) (g : G.1.1) : Path (K1 G) (K1-point' G) (K1-point' G)
+ := <i> trunc₁ (2-quot 𝟏 (R-K1 G) (Q-K1 G)) two (2-quot₂ 𝟏 (R-K1 G) (Q-K1 G) ★ ★ g @ i)
 
 def K (G : abgroup) (n: ℕ) : U
  := ℕ-iter U (discreteTopology G) (λ (_: U), ‖_‖ (𝚺ₓ (K1 (G.X, G.2.g)) n) n) n
@@ -25,9 +28,6 @@ def K-point (G : abgroup) : Π (n : ℕ), K G n
           G.2.g.1.2.2.1
           (λ (k : ℕ) (_ : K G k), trunc₁ (𝚺ₓ (K1 (G.X, G.2.g)) (succ k)) (succ k) (𝜎₁ (𝚺ₓ (K1 (G.X, G.2.g)) k)))
 
-def K1-point' (G : group) : K1 G := trunc₁ (2-quot 𝟏 (R-K1 G) (Q-K1 G)) two (2-quot₁ 𝟏 (R-K1 G) (Q-K1 G) ★)
-def K1-loop'  (G : group) (g : G.1.1) : Path (K1 G) (K1-point' G) (K1-point' G)
- := <i> trunc₁ (2-quot 𝟏 (R-K1 G) (Q-K1 G)) two (2-quot₂ 𝟏 (R-K1 G) (Q-K1 G) ★ ★ g @ i)
 
 {-