format

Author: 5HT

library/mathematics/homotopy/KGn.anders

@@ -1,9 +1,5 @@
 {- Eilenberg-MacLane Spaces: https://anders.groupoid.space/mathematics/homotopy/KGn/
-
-    Implemented using primitive nat and ind-nat to ensure judgmental
-    reduction across the loop space tower.
-
-    Copyright (c) Groupoid Infinity, 2016-2026. -}
+   Copyright (c) Groupoid Infinity, 2016-2026. -}
 
 module KGn where
 import library/foundations/mltt/nat
@@ -24,40 +20,26 @@ def K-step (G : abgroup) (k : nat) (prev : Pointed) : Pointed
         trunc₁ (𝚺 prev.1) (plus (succ (succ zero)) (succ m)) (𝜎₁ prev.1))) k
 
 -- K(G, n) tower construction using primitive ind-nat
-def K-Pointed (G : abgroup) (n : nat) : Pointed
- := ind-nat (λ (x : nat), Pointed) (G.1.1, G.2.1.1.2.2.1) (λ (k : nat) (prev : Pointed), K-step G k prev) n
-
+def K-Pointed (G : abgroup) (n : nat) : Pointed := ind-nat (λ (x : nat), Pointed) (G.1.1, G.2.1.1.2.2.1) (λ (k : nat) (prev : Pointed), K-step G k prev) n
 def K (G : abgroup) (n : nat) : U := (K-Pointed G n).1
 def K-point (G : abgroup) (n : nat) : K G n := (K-Pointed G n).2
 
--- K(G, n) Rules
--- Elimination (Induction):
--- P must be a family over the whole tower to allow induction on n.
-def K-ind (G : abgroup) (n : nat) (P : Π (k : nat), K G k → U)
-    (pBase : Π (g : G.1.1), P zero g)
-    (pStep : Π (k : nat) (prev : Π (z : K G k), P k z) (z : K G (succ k)), P (succ k) z)
-    (z : K G n) : P n z
- := ind-nat (λ (k : nat), Π (pB : Π (g : G.1.1), P zero g),
-              (Π (m : nat) (pr : Π (y : K G m), P m y) (y : K G (succ m)), P (succ m) y) →
-              (Π (z : K G k), P k z))
+-- Elimination (Induction): P must be a family over the whole tower to allow induction on n.
+def K-ind (G : abgroup) (n : nat) (P : Π (k : nat), K G k → U) (pBase : Π (g : G.1.1), P zero g)
+    (pStep : Π (k : nat) (prev : Π (z : K G k), P k z) (z : K G (succ k)), P (succ k) z) (z : K G n) : P n z
+ := ind-nat (λ (k : nat), Π (pB : Π (g : G.1.1), P zero g), (Π (m : nat) (pr : Π (y : K G m), P m y) (y : K G (succ m)), P (succ m) y) → (Π (z : K G k), P k z))
     (λ (pB : Π (g : G.1.1), P zero g) (pS : Π (m : nat) (pr : Π (y : K G m), P m y) (y : K G (succ m)), P (succ m) y) (z : K G zero), pB z)
     (λ (k : nat) (prev : Π (pB : Π (g : G.1.1), P zero g) (pS : Π (m : nat) (pr : Π (y : K G m), P m y) (y : K G (succ m)), P (succ m) y) (z : K G k), P k z)
-       (pB : Π (g : G.1.1), P zero g) (pS : Π (m : nat) (pr : Π (y : K G m), P m y) (y : K G (succ m)), P (succ m) y) (z : K G (succ k)),
-       pS k (λ (y : K G k), prev pB pS y) z)
-    n pBase pStep z
+    (pB : Π (g : G.1.1), P zero g) (pS : Π (m : nat) (pr : Π (y : K G m), P m y) (y : K G (succ m)), P (succ m) y) (z : K G (succ k)), pS k (λ (y : K G k), prev pB pS y) z) n pBase pStep z
 
 -- Computation Rule (Beta):
-def K-point-β (G : abgroup) (n : nat) (P : Π (k : nat), K G k → U)
-    (pBase : Π (g : G.1.1), P zero g)
+def K-point-β (G : abgroup) (n : nat) (P : Π (k : nat), K G k → U) (pBase : Π (g : G.1.1), P zero g)
     (pStep : Π (k : nat) (prev : Π (z : K G k), P k z) (z : K G (succ k)), P (succ k) z)
   : Path (P n (K-point G n)) (K-ind G n P pBase pStep (K-point G n)) (K-ind G n P pBase pStep (K-point G n))
  := <_> (K-ind G n P pBase pStep (K-point G n))
 
--- Uniqueness (Eta):
--- This rule must be proven by induction on n because ind-nat does not reduce on a variable n.
+-- Uniqueness (Eta): This rule must be proven by induction on n because ind-nat does not reduce on a variable n.
 def K-η (G : abgroup) (n : nat) (P : Π (k : nat), K G k → U) (h : Π (k : nat) (z : K G k), P k z)
   : Path (Π (z : K G n), P n z) (h n) (λ (z : K G n), K-ind G n P (λ (g : G.1.1), h zero g) (λ (k : nat) (prev : Π (y : K G k), P k y) (y : K G (succ k)), h (succ k) y) z)
- := ind-nat (λ (k : nat), Path (Π (z : K G k), P k z) (h k) (λ (z : K G k), K-ind G k P (λ (g : G.1.1), h zero g) (λ (m : nat) (pr : Π (y : K G m), P m y) (y : K G (succ m)), h (succ m) y) z))
-    (<_> (h zero))
-    (λ (k : nat) (prev : Path (Π (z : K G k), P k z) (h k) (λ (z : K G k), K-ind G k P (λ (g : G.1.1), h zero g) (λ (m : nat) (pr : Π (y : K G m), P m y) (y : K G (succ m)), h (succ m) y) z)),
-     <_> (h (succ k))) n
+ := ind-nat (λ (k : nat), Path (Π (z : K G k), P k z) (h k) (λ (z : K G k), K-ind G k P (λ (g : G.1.1), h zero g) (λ (m : nat) (pr : Π (y : K G m), P m y) (y : K G (succ m)), h (succ m) y) z)) (<_> (h zero))
+    (λ (k : nat) (prev : Path (Π (z : K G k), P k z) (h k) (λ (z : K G k), K-ind G k P (λ (g : G.1.1), h zero g) (λ (m : nat) (pr : Π (y : K G m), P m y) (y : K G (succ m)), h (succ m) y) z)), <_> (h (succ k))) n

library/mathematics/homotopy/truncation.anders

@@ -11,7 +11,7 @@ import library/foundations/mltt/either
 import library/mathematics/homotopy/Sn
 import library/mathematics/homotopy/hs
 
-def trunc  (A : U) (n : ℕ)        : U := hs (sphere n) A
+def trunc  (A : U) (n : ℕ)                                                 : U         := hs (sphere n) A
 def trunc₁ (A : U) (n : ℕ) (x : A)                                         : trunc A n := center (sphere n) A x
 def trunc₂ (A : U) (n : ℕ) (f : sphere n → hs (sphere n) A)                : trunc A n := hub' (sphere n) A f
 def trunc₃ (A : U) (n : ℕ) (f : sphere n → hs (sphere n) A) (s : sphere n)             := spoke' (sphere n) A f s