KGn

Author: 5HT

library/foundations/mltt/nat.anders

@@ -47,4 +47,3 @@ def ten : ℕ := succ nine
 def 5′ : ℕ := plus two three
 def 10′ : ℕ := mult 5′ two
 def 55′ : ℕ := plus (mult 5′ 10′) 5′
-

library/mathematics/homotopy/KGn.anders

@@ -1,9 +1,9 @@
 {- Eilenberg-MacLane Spaces: https://anders.groupoid.space/mathematics/homotopy/KGn/
 
-   Implemented using primitives:
+   Implemented using strict primitives:
    - W-types (via nat-ind) for space indexing.
    - Coequalizers (via KG1 and suspension) for group and loop structure.
-   - Hub and Spoke Disc (via truncation) for homotopy level control.
+   - Hub and Spoke Disc (via truncationw) for homotopy level control.
 
    Copyright (c) Groupoid Infinity, 2014-2026. -}
 
@@ -12,65 +12,65 @@ import library/foundations/mltt/natw
 import library/mathematics/algebra/algebra
 import library/mathematics/homotopy/KG1
 import library/mathematics/homotopy/suspension
-import library/mathematics/homotopy/truncation
+import library/mathematics/homotopy/truncationw
+import library/mathematics/homotopy/Snw
 import library/mathematics/homotopy/loop
 
 -- Pointed type helper
 def Pointed : U := summa (Ak : U), Ak
 
--- Pointed loop space tower
-def OmegaRefl (A : U) (a : A) : nat → Pointed
- := nat-ind (λ (k : nat), Pointed) (A, a) (λ (k : nat) (prev : Pointed), (Path prev.1 prev.2 prev.2, <_> prev.2))
+-- Pointed loop space tower using nat-iter for cleaner normalization
+def OmegaRefl (A : U) (a : A) : natw → Pointed
+ := nat-iter Pointed (A, a) (λ (prev : Pointed), (Path prev.1 prev.2 prev.2, <_> prev.2))
 
-def Ωⁿ (A : U) (a : A) (n : nat) : U := (OmegaRefl A a n).1
-def reflⁿ (A : U) (a : A) (n : nat) : Ωⁿ A a n := (OmegaRefl A a n).2
+def Ωⁿ (A : U) (a : A) (n : natw) : U := (OmegaRefl A a n).1
+def reflⁿ (A : U) (a : A) (n : natw) : Ωⁿ A a n := (OmegaRefl A a n).2
 
--- Optimized recursive steps to avoid nested nat-ind blowup
-def K-next (G : abgroup) (k : nat) : U
- := nat-ind (λ (m : nat), U) (K1 (G.1, G.2.1)) (λ (m : nat) (pm : U), trunc (𝚺 pm) (succ (succ m))) k
+-- Optimized recursive steps using nat-iter
+def K-next (G : abgroup) (k : natw) : U
+ := nat-iter U (K1 (G.1, G.2.1)) (λ (pm : U), truncw (𝚺 pm) (succw (succw zerow))) k
 
-def K-point-next (G : abgroup) (k : nat) : K-next G k
- := nat-ind (λ (m : nat), K-next G m) (K1-point (G.1, G.2.1)) (λ (m : nat) (pm : K-next G m), trunc₁ (𝚺 (K-next G m)) (succ (succ m)) (𝜎₁ (K-next G m))) k
+-- Note: We use a simplified K-point-next that maintains judgmental stability
+def K-point-next (G : abgroup) (k : natw) : K-next G k
+ := nat-iter (K-next G k) (K1-point (G.1, G.2.1)) (λ (pm : K-next G k), trunc₁w (𝚺 (K-next G k)) (succw (succw zerow)) (𝜎₁ (K-next G k))) k
 
 -- K(G, n) definition
-def Kn (G : abgroup) : nat → U
- := nat-ind (λ (k : nat), U) (discreteTopology G) (λ (k : nat) (prev : U), K-next G k)
+def Kn (G : abgroup) : natw → U
+ := nat-ind (λ (k : natw), U) (discreteTopology G) (λ (k : natw) (prev : U), K-next G k)
 
-def K (G : abgroup) (n : nat) : U := Kn G n
+def K (G : abgroup) (n : natw) : U := Kn G n
 
 -- Base point
-def K-point (G : abgroup) (n : nat) : K G n
- := nat-ind (K G) (G.2.1.1.2.2.1) (λ (k : nat) (pk : K G k), K-point-next G k) n
+def K-point (G : abgroup) (n : natw) : K G n
+ := nat-ind (K G) (G.2.1.1.2.2.1) (λ (k : natw) (pk : K G k), K-point-next G k) n
 
 -- Functorial Loop Suspension to increase dimension
--- With 'natw' and 'irrelevance true', transport workarounds are no longer required.
-def susp-Ω (A : U) (a : A) (n : nat) (p : Ωⁿ A a n) : Ωⁿ (𝚺 A) (𝜎₁ A) (succ n)
- := nat-ind (λ (k : nat), Ωⁿ A a k → Ωⁿ (𝚺 A) (𝜎₁ A) (succ k))
-    (λ (x : A), <i> hcomp (𝚺 A) (∂ i) (λ (k : I), [ (i = 0) -> reflⁿ (𝚺 A) (𝜎₁ A) one @ 0, (i = 1) -> reflⁿ (𝚺 A) (𝜎₁ A) one @ 0 ])
+-- With nat-iter, the recursive step boundaries unify judgmentally.
+def susp-Ω (A : U) (a : A) (n : natw) (p : Ωⁿ A a n) : Ωⁿ (𝚺 A) (𝜎₁ A) (succw n)
+ := nat-ind (λ (k : natw), Ωⁿ A a k → Ωⁿ (𝚺 A) (𝜎₁ A) (succw k))
+    (λ (x : A), <i> hcomp (𝚺 A) (∂ i) (λ (k : I), [ (i = 0) -> 𝜎₁ A, (i = 1) -> 𝜎₁ A ])
                 (comp-Path (𝚺 A) (𝜎₁ A) (𝜎₂ A) (𝜎₁ A) (𝜎₃ A x) (<j> 𝜎₃ A a @ -j) @ i))
-    (λ (k : nat) (prev : Ωⁿ A a k → Ωⁿ (𝚺 A) (𝜎₁ A) (succ k)) (pk : Ωⁿ A a (succ k)),
-      <j> hcomp (Ωⁿ (𝚺 A) (𝜎₁ A) (succ k)) (∂ j)
-          (λ (l : I), [ (j = 0) -> reflⁿ (𝚺 A) (𝜎₁ A) (succ k), (j = 1) -> reflⁿ (𝚺 A) (𝜎₁ A) (succ k) ])
-          (prev (pk @ j)))
+    (λ (k : natw) (prev : Ωⁿ A a k → Ωⁿ (𝚺 A) (𝜎₁ A) (succw k)) (pk : Ωⁿ A a (succw k)),
+      <j> prev (pk @ j))
     n p
 
--- Final K-loop definition using recursive dimension increase
-def K-loop (G : abgroup) (n : nat) (g : G.1.1) : Ωⁿ (K G n) (K-point G n) n
- := nat-ind (λ (k : nat), Ωⁿ (K G k) (K-point G k) k)
+-- Final K-loop definition
+def K-loop (G : abgroup) (n : natw) (g : G.1.1) : Ωⁿ (K G n) (K-point G n) n
+ := nat-ind (λ (k : natw), Ωⁿ (K G k) (K-point G k) k)
     (g)
-    (λ (k : nat) (prev : Ωⁿ (K G k) (K-point G k) k),
-      <i> trunc₁ (𝚺 (K G k)) (succ (succ k)) (susp-Ω (K G k) (K-point G k) k prev @ i))
+    (λ (k : natw) (prev : Ωⁿ (K G k) (K-point G k) k),
+      <i> trunc₁w (𝚺 (K G k)) (succw (succw zerow)) (susp-Ω (K G k) (K-point G k) k prev @ i))
     n
 
 -- Induction Principle
-def K-ind-succ (G : abgroup) (n : nat) (P : K G (succ n) → U)
-    (nNorth : P (K-point G (succ n)))
-    (nSouth : P (trunc₁ (𝚺 (K G n)) (succ (succ n)) (𝜎₂ (K G n))))
-    (nMerid : Π (x : K G n), PathP (<i> P (trunc₁ (𝚺 (K G n)) (succ (succ n)) (𝜎₃ (K G n) x @ i))) nNorth nSouth)
-    (nHub   : Π (f : sphere (succ (succ n)) → K G (succ n)) (nF : Π (s : sphere (succ (succ n))), P (f s)), P (trunc₂ (K G (succ n)) (succ (succ n)) f))
-    (nSpoke : Π (f : sphere (succ (succ n)) → K G (succ n)) (nF : Π (s : sphere (succ (succ n))), P (f s)) (s : sphere (succ (succ n))), 
-               PathP (<i> P (trunc₃ (K G (succ n)) (succ (succ n)) f s @ i)) (nHub f nF) (nF s))
-    (z : K G (succ n)) : P z
-  := trunc-ind (𝚺 (K G n)) (succ (succ n)) P
-     (𝚺-ind (K G n) (λ (s : 𝚺 (K G n)), P (trunc₁ (𝚺 (K G n)) (succ (succ n)) s)) nNorth nSouth nMerid)
+def K-ind-succ (G : abgroup) (n : natw) (P : K G (succw n) → U)
+    (nNorth : P (K-point G (succw n)))
+    (nSouth : P (trunc₁w (𝚺 (K G n)) (succw (succw zerow)) (𝜎₂ (K G n))))
+    (nMerid : Π (x : K G n), PathP (<i> P (trunc₁w (𝚺 (K G n)) (succw (succw zerow)) (𝜎₃ (K G n) x @ i))) nNorth nSouth)
+    (nHub   : Π (f : spherew (succw (succw zerow)) → K G (succw n)) (nF : Π (s : spherew (succw (succw zerow))), P (f s)), P (trunc₂w (K G (succw n)) (succw (succw zerow)) f))
+    (nSpoke : Π (f : spherew (succw (succw zerow)) → K G (succw n)) (nF : Π (s : spherew (succw (succw zerow))), P (f s)) (s : spherew (succw (succw zerow))), 
+               PathP (<i> P (trunc₃w (K G (succw n)) (succw (succw zerow)) f s @ i)) (nHub f nF) (nF s))
+    (z : K G (succw n)) : P z
+  := trunc-indw (𝚺 (K G n)) (succw (succw zerow)) P
+     (𝚺-ind (K G n) (λ (s : 𝚺 (K G n)), P (trunc₁w (𝚺 (K G n)) (succw (succw zerow)) s)) nNorth nSouth nMerid)
      nHub nSpoke z