From 52dda63e4dcd0fcbe2beb1b8cc3e090a4989629c Mon Sep 17 00:00:00 2001
From: Ulrik Buchholtz <ulrikbuchholtz@gmail.com>
Date: Thu, 29 Jun 2017 20:06:47 +0100
Subject: [PATCH] refactor strunc

---
 homotopy/strunc.hlean | 155 +++++++++++++++---------------------------
 1 file changed, 53 insertions(+), 102 deletions(-)

diff --git a/homotopy/strunc.hlean b/homotopy/strunc.hlean
index 7fdd134..684933f 100644
--- a/homotopy/strunc.hlean
+++ b/homotopy/strunc.hlean
@@ -1,8 +1,25 @@
 import .spectrum .EM
 
 -- TODO move this
+open trunc_index nat
+
 namespace int
 
+  definition maxm2 : ℤ → ℕ₋₂ :=
+  λ n, int.cases_on n trunc_index.of_nat
+    (λ m, nat.cases_on m -1 (λ a, -2))
+
+  attribute maxm2 [unfold 1]
+
+  definition maxm2_le_maxm0 (n : ℤ) : maxm2 n ≤ max0 n :=
+  begin
+    induction n with n n,
+    { exact le.tr_refl n },
+    { cases n with n,
+      { exact le.step (le.tr_refl -1) },
+      { exact minus_two_le 0 } }
+  end
+
   definition max0_le_of_le {n : ℤ} {m : ℕ} (H : n ≤ of_nat m)
     : nat.le (max0 n) m :=
   begin
@@ -17,78 +34,44 @@ open int trunc eq is_trunc lift unit pointed equiv is_equiv algebra EM
 
 namespace spectrum
 
-definition trunc_int.{u} (k : ℤ) (X : Type.{u}) : Type.{u} :=
-begin
-  induction k with k k, exact trunc k X,
-  cases k with k, exact trunc -1 X,
-  exact lift unit
-end
+definition ptrunc_maxm2_change_int {k l : ℤ} (X : Type*) (p : k = l)
+  : ptrunc (maxm2 k) X ≃* ptrunc (maxm2 l) X :=
+pequiv_ap (λ n, ptrunc (maxm2 n) X) p
 
-definition ptrunc_int.{u} (k : ℤ) (X : pType.{u}) : pType.{u} :=
-begin
-  induction k with k k, exact ptrunc k X,
-  exact plift punit
-end
--- NB the carrier of ptrunc_int k X is not definitionally 
--- equal to trunc_int k (carrier X)
-
-definition ptr_int (k : ℤ) (X : pType) : X →* ptrunc_int k X :=
-pmap.mk (λ x, int.cases_on k (λ k', tr x) (λ k', up star))
-  (int.cases_on k (λ k', idp) (λ k', idp))
-
-definition ptrunc_int_pequiv_ptrunc_int (k : ℤ) {X Y : Type*} (e : X ≃* Y) :
-  ptrunc_int k X ≃* ptrunc_int k Y :=
+definition loop_ptrunc_maxm2_pequiv (k : ℤ) (X : Type*) :
+  Ω (ptrunc (maxm2 (k+1)) X) ≃* ptrunc (maxm2 k) (Ω X) :=
 begin
   induction k with k k,
-    exact ptrunc_pequiv_ptrunc k e,
-  exact !pequiv_plift⁻¹ᵉ* ⬝e* !pequiv_plift
+  { exact loop_ptrunc_pequiv k X },
+  { cases k with k,
+    { exact loop_ptrunc_pequiv -1 X },
+    { cases k with k,
+      { exact loop_ptrunc_pequiv -2 X },
+      { exact loop_pequiv_punit_of_is_set (pType.mk (trunc -2 X) (tr pt))
+          ⬝e* (pequiv_punit_of_is_contr
+                (pType.mk (trunc -2 (Point X = Point X)) (tr idp))
+                (is_trunc_trunc -2 (Point X = Point X)))⁻¹ᵉ* } } }
 end
 
-definition ptrunc_int_change_int {k l : ℤ} (X : Type*) (p : k = l) :
-  ptrunc_int k X ≃* ptrunc_int l X :=
-pequiv_ap (λn, ptrunc_int n X) p
-
-definition loop_ptrunc_int_pequiv (k : ℤ) (X : Type*) :
-  Ω (ptrunc_int (k+1) X) ≃* ptrunc_int k (Ω X) :=
-begin
-  induction k with k k,
-    exact loop_ptrunc_pequiv k X,
-  cases k with k,
-    change Ω (ptrunc 0 X) ≃* plift punit,
-    exact !loop_pequiv_punit_of_is_set ⬝e* !pequiv_plift,
-  exact loop_pequiv_loop !pequiv_plift⁻¹ᵉ* ⬝e* !loop_punit ⬝e* !pequiv_plift
-end
+definition is_trunc_of_is_trunc_maxm2 (k : ℤ) (X : Type)
+  : is_trunc (maxm2 k) X → is_trunc (max0 k) X :=
+λ H, @is_trunc_of_le X _ _ (maxm2_le_maxm0 k) H
 
 definition strunc [constructor] (k : ℤ) (E : spectrum) : spectrum :=
-spectrum.MK (λ(n : ℤ), ptrunc_int (k + n) (E n))
-            (λ(n : ℤ), ptrunc_int_pequiv_ptrunc_int (k + n) (equiv_glue E n) ⬝e*
-                       (loop_ptrunc_int_pequiv (k + n) (E (n+1)))⁻¹ᵉ* ⬝e*
-                       loop_pequiv_loop (ptrunc_int_change_int _ (add.assoc k n 1)))
+spectrum.MK (λ(n : ℤ), ptrunc (maxm2 (k + n)) (E n))
+            (λ(n : ℤ), ptrunc_pequiv_ptrunc (maxm2 (k + n)) (equiv_glue E n)
+              ⬝e* (loop_ptrunc_maxm2_pequiv (k + n) (E (n+1)))⁻¹ᵉ*
+              ⬝e* (loop_pequiv_loop
+                   (ptrunc_maxm2_change_int _ (add.assoc k n 1))))
 
 definition strunc_change_int [constructor] {k l : ℤ} (E : spectrum) (p : k = l) :
   strunc k E →ₛ strunc l E :=
 begin induction p, reflexivity end
 
-definition is_trunc_int.{u} (k : ℤ) (X : Type.{u}) : Type.{u} :=
+definition is_trunc_maxm2_loop (A : pType) (k : ℤ)
+  : is_trunc (maxm2 (k + 1)) A → is_trunc (maxm2 k) (Ω A) :=
 begin
-  induction k with k k,
-  { -- case ≥ 0
-    exact is_trunc k X },
-  { cases k with k,
-    { -- case = -1
-      exact is_trunc -1 X },
-    { -- case < -1
-      exact is_contr X } }
-end
-
-definition is_trunc_int_change_int {k l : ℤ} (X : Type) (p : k = l)
-  : is_trunc_int k X → is_trunc_int l X :=
-begin induction p, exact id end
-
-definition is_trunc_int_loop (A : pType) (k : ℤ)
-  : is_trunc_int (k + 1) A → is_trunc_int k (Ω A) :=
-begin
-  intro H, induction k with k k, 
+  intro H, induction k with k k,
   { apply is_trunc_loop, exact H },
   { cases k with k,
     { apply is_trunc_loop, exact H},
@@ -97,65 +80,33 @@ begin
       { apply is_trunc_succ, exact H } } }
 end
 
-definition is_trunc_of_is_trunc_int (k : ℤ) (X : Type)
-  : is_trunc_int k X → is_trunc (max0 k) X :=
-begin
-  intro H, induction k with k k,
-  { exact H },
-  { cases k with k,
-    { apply is_trunc_succ, exact H },
-    { apply is_trunc_of_is_contr, exact H } }
-end
-
 definition is_strunc (k : ℤ) (E : spectrum) : Type :=
-Π (n : ℤ), is_trunc_int (k + n) (E n)
+Π (n : ℤ), is_trunc (maxm2 (k + n)) (E n)
 
 definition is_strunc_change_int {k l : ℤ} (E : spectrum) (p : k = l)
   : is_strunc k E → is_strunc l E :=
 begin induction p, exact id end
 
-definition is_trunc_trunc_int (k : ℤ) (X : Type)
-  : is_trunc_int k (trunc_int k X) :=
-begin
-  induction k with k k,
-  { -- case ≥ 0
-    exact is_trunc_trunc k X },
-  { cases k with k,
-    { -- case = -1
-      exact is_trunc_trunc -1 X },
-    { -- case < -1
-      apply is_trunc_lift } }
-end
-
-definition is_trunc_ptrunc_int (k : ℤ) (X : pType)
-  : is_trunc_int k (ptrunc_int k X) :=
-begin
-  induction k with k k,
-  { -- case ≥ 0
-    exact is_trunc_trunc k X },
-  { cases k with k,
-    { -- case = -1
-      apply is_trunc_lift, apply is_trunc_unit },
-    { -- case < -1
-      apply is_trunc_lift, apply is_trunc_unit } }
-end
-
 definition is_strunc_strunc (k : ℤ) (E : spectrum)
   : is_strunc k (strunc k E) :=
-λ n, is_trunc_ptrunc_int (k + n) (E n)
+λ n, is_trunc_trunc (maxm2 (k + n)) (E n)
+
+definition is_trunc_maxm2_change_int {k l : ℤ} (X : pType) (p : k = l)
+  : is_trunc (maxm2 k) X → is_trunc (maxm2 l) X :=
+by induction p; exact id
 
 definition is_strunc_EM_spectrum (G : AbGroup)
   : is_strunc 0 (EM_spectrum G) :=
 begin
   intro n, induction n with n n,
   { -- case ≥ 0
-    apply is_trunc_int_change_int (EM G n) (zero_add n)⁻¹,
+    apply is_trunc_maxm2_change_int (EM G n) (zero_add n)⁻¹,
     apply is_trunc_EM },
   { induction n with n IH,
     { -- case = -1
       apply is_trunc_loop, exact ab_group.is_set_carrier G },
     { -- case < -1
-      apply is_trunc_int_loop, exact IH }}
+      apply is_trunc_maxm2_loop, exact IH }}
 end
 
 definition trivial_shomotopy_group_of_is_strunc (E : spectrum)
@@ -168,11 +119,11 @@ have I : m < 2, from
   ... < (2 - k) + k : add_lt_add_left H (2 - k)
   ... = 2           : sub_add_cancel 2 k,
 @trivial_homotopy_group_of_is_trunc (E (2 - k)) (max0 m) 2
-  (is_trunc_of_is_trunc_int m (E (2 - k)) (K (2 - k)))
+  (is_trunc_of_is_trunc_maxm2 m (E (2 - k)) (K (2 - k)))
   (nat.succ_le_succ (max0_le_of_le (le_sub_one_of_lt I)))
 
 definition str [constructor] (k : ℤ) (E : spectrum) : E →ₛ strunc k E :=
-smap.mk (λ n, ptr_int (k + n) (E n))
-  sorry
+smap.mk (λ n, ptr (maxm2 (k + n)) (E n))
+  (λ n, sorry)
 
 end spectrum