forrmattings

Author: 5HT

library/foundations/mltt/inductive.anders

@@ -14,7 +14,6 @@ module inductive where
 import library/foundations/univalent/path
 import library/foundations/mltt/either
 
-
 -- Steve Awodey, Nicola Gambino, Kristina Sojakova
 -- Inductive Types in Homotopy Type Theory
 -- https://arxiv.org/pdf/1201.3898.pdf
@@ -48,8 +47,7 @@ def 2-β₂ (C : 𝟐 → U) (f : Π (x : 𝟐), C 0₂) (g : Π (y : 𝟐), C 1
  := <_> g 1₂
 
 def 2-η (c : 𝟐) : + (PathP (<_> 𝟐) c 0₂) (PathP (<_> 𝟐) c 1₂)
- := ind₂ (λ (c : 𝟐), + (PathP (<_> 𝟐) c 0₂) (PathP (<_> 𝟐) c 1₂))
-         (0₂, <_> 0₂) (1₂, <_> 1₂) c
+ := ind₂ (λ (c : 𝟐), + (PathP (<_> 𝟐) c 0₂) (PathP (<_> 𝟐) c 1₂)) (0₂, <_> 0₂) (1₂, <_> 1₂) c
 
 def W′ (A : U) (B : A → U) : U := W (x: A), B x
 def sup′ (A : U) (B : A → U) (x : A) (f : B x → W′ A B) : W′ A B := sup A B x f
@@ -83,13 +81,11 @@ def W-proj₁ (A : U) (B : A → U) : (W (x : A), B x) → A
  := W-case A B A (λ (x : A) (f : B x → (W (x : A), B x)), x)
 
 def W-proj₂ (A : U) (B : A → U) : Π (w : W (x : A), B x), B (W-proj₁ A B w) → (W (x : A), B x)
- := W-ind′ A B (λ (w : W (x : A), B x), B (W-proj₁ A B w) → (W (x : A), B x))
-               (λ (x : A) (f : B x → (W (x : A), B x)), f)
+ := W-ind′ A B (λ (w : W (x : A), B x), B (W-proj₁ A B w) → (W (x : A), B x)) (λ (x : A) (f : B x → (W (x : A), B x)), f)
 
 def W-η (A : U) (B : A → U)
   : Π (w : W (x : A), B x), Path (W (x : A), B x) (sup A B (W-proj₁ A B w) (W-proj₂ A B w)) w
- := W-ind′ A B (λ (w : W (x : A), B x), Path (W (x : A), B x) (sup A B (W-proj₁ A B w) (W-proj₂ A B w)) w)
-               (λ (x : A) (f : B x → (W (x : A), B x)), <_> sup A B x f)
+ := W-ind′ A B (λ (w : W (x : A), B x), Path (W (x : A), B x) (sup A B (W-proj₁ A B w) (W-proj₂ A B w)) w) (λ (x : A) (f : B x → (W (x : A), B x)), <_> sup A B x f)
 
 def trans-W (A : I → U) (B : Π (i : I), A i → U) (a : A 0) (f : B 0 a → (W (x : A 0), B 0 x)) : W (x : A 1), B 1 x
  := sup (A 1) (B 1) (transp (<i> A i) 0 a) (transp (<i> B i (transFill (A 0) (A 1) (<j> A j) a @ i) → (W (x : A i), B i x)) 0 f)
@@ -117,5 +113,5 @@ def hcomp-W′ (A : U) (B : A → U) (r : I) (a : I → Partial A r)
 def hcomp-W-is-correct (A : U) (B : A → U) (r : I) (a : I → Partial A r)
     (f : Π (i : I), PartialP [(r = 1) → B (a i 1=1) → (W (x : A), B x)] r)
     (a₀ : A[r ↦ a 0]) (f₀ : (B (ouc a₀) → (W (x : A), B x))[r ↦ f 0]) :
-    Path (W (x : A), B x) (hcomp-W A B r a f a₀ f₀) (hcomp-W′ A B r a f a₀ f₀) :=
-<_> hcomp-W A B r a f a₀ f₀
+    Path (W (x : A), B x) (hcomp-W A B r a f a₀ f₀) (hcomp-W′ A B r a f a₀ f₀)
+ := <_> hcomp-W A B r a f a₀ f₀

library/foundations/mltt/nat.anders

@@ -1,9 +1,6 @@
 {- Natural Numbers: https://anders.groupoid.space/foundations/mltt/nat/
    - Nat.
-
    Implemented using kernel primitives for judgmental beta-reduction.
-   Provides standard MLTT rules: Formation, Introduction, Elimination, and Computation.
-
    Copyright (c) Groupoid Infinity, 2014-2026. -}
 
 module nat where

library/foundations/mltt/natw.anders

@@ -1,3 +1,8 @@
+{- Homotopy Natural Numbers: https://anders.groupoid.space/foundations/mltt/natw/
+   - Homotopy Nat.
+   Implemented using W primitives using transp enforcing Homotopy Canonicity and Losing Strong Canonicity.
+   Copyright (c) Groupoid Infinity, 2014-2026. -}
+
 module natw where
 import library/foundations/mltt/inductive
 
@@ -18,8 +23,7 @@ def nat-ind (P : natw → U) (p0 : P zerow) (ps : Π (n : natw), P n → P (succ
            (λ (f' : 𝟏 → natw) (g' : Π (x : 𝟏), P (f' x)),
               transp (<i> P (sup nat-B nat-C 1₂ (λ (u : 𝟏),
                 ind₁ (λ (v : 𝟏), Path natw (f' ★) (f' v)) (<_> f' ★) u @ i))) 0 (ps (f' ★) (g' ★)))
-           b f g)
-    n
+           b f g) n
 
 def nat-rec (A : U) (a : A) (f : natw → A → A) : natw → A := nat-ind (λ (x : natw), A) a f
 def nat-iter (A : U) (a : A) (f : A → A) : natw → A := nat-rec A a (λ (n : natw) (x : A), f x)

library/mathematics/homotopy/KGn.anders

@@ -14,24 +14,18 @@ import library/mathematics/homotopy/Sn
 import library/mathematics/homotopy/loop
 import library/mathematics/homotopy/KG1
 
-
 -- K-step: K(G, n+1) = || Σ K(G, n) ||_{n+1}
 -- For k=0 (n=1), we use the K(G,1) construction from KG1.
 def K-step (G : abgroup) (k : nat) (prev : Pointed) : Pointed
  := ind-nat (λ (_ : nat), Pointed)
-    (K1 (G.1, G.2.1), K1-point (G.1, G.2.1))
+    (K1 (G.1, G.2.1), K1-point (G.1, G.2.1)) -- place unit here istead to understand how fast raw type checking is
     (λ (m : nat) (_ : Pointed),
        (trunc (𝚺 prev.1) (plus (succ (succ zero)) (succ m)),
-        trunc₁ (𝚺 prev.1) (plus (succ (succ zero)) (succ m)) (𝜎₁ prev.1)))
-    k
-
+        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
+ := 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
@@ -66,6 +60,4 @@ def K-η (G : abgroup) (n : nat) (P : Π (k : nat), K G k → U) (h : Π (k : na
  := 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
-
+     <_> (h (succ k))) n