From 9934c9c73d401bfa60e8332d37ed22264c1679db Mon Sep 17 00:00:00 2001
From: Ulrik Buchholtz <ulrikbuchholtz@gmail.com>
Date: Wed, 28 Jun 2017 17:19:23 +0100
Subject: [PATCH] trivial homotopy groups of truncated spectra

---
 homotopy/strunc.hlean | 56 ++++++++++++++++++++++++++++++++++++++-----
 1 file changed, 50 insertions(+), 6 deletions(-)

diff --git a/homotopy/strunc.hlean b/homotopy/strunc.hlean
index c509b2c..89221f0 100644
--- a/homotopy/strunc.hlean
+++ b/homotopy/strunc.hlean
@@ -1,6 +1,20 @@
 import .spectrum .EM
 
+-- TODO move this
+namespace int
+
+  definition max0_le_of_le {n : ℤ} {m : ℕ} (H : n ≤ of_nat m)
+    : nat.le (max0 n) m :=
+  begin
+    induction n with n n,
+    { exact le_of_of_nat_le_of_nat H },
+    { exact nat.zero_le m }
+  end
+
+end int
+
 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} :=
@@ -60,13 +74,35 @@ begin
     { -- case = -1
       exact is_trunc -1 X },
     { -- case < -1
-      exact lift unit } }
+      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, 
+  { apply is_trunc_loop, exact H },
+  { cases k with k,
+    { apply is_trunc_loop, exact H},
+    { apply is_trunc_loop, cases k with k,
+      { exact H },
+      { 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)
 
@@ -84,7 +120,7 @@ begin
     { -- case = -1
       exact is_trunc_trunc -1 X },
     { -- case < -1
-      exact up unit.star } }
+      apply is_trunc_lift } }
 end
 
 definition is_trunc_ptrunc_int (k : ℤ) (X : pType)
@@ -97,7 +133,7 @@ begin
     { -- case = -1
       apply is_trunc_lift, apply is_trunc_unit },
     { -- case < -1
-      exact up unit.star } }
+      apply is_trunc_lift, apply is_trunc_unit } }
 end
 
 definition is_strunc_strunc (k : ℤ) (E : spectrum)
@@ -111,16 +147,24 @@ begin
   { -- case ≥ 0
     apply is_trunc_int_change_int (EM G n) (zero_add n)⁻¹,
     apply is_trunc_EM },
-  { cases n,
+  { induction n with n IH,
     { -- case = -1
       apply is_trunc_loop, exact ab_group.is_set_carrier G },
     { -- case < -1
-      exact up unit.star }}
+      apply is_trunc_int_loop, exact IH }}
 end
 
 definition trivial_shomotopy_group_of_is_strunc (E : spectrum)
   {n k : ℤ} (K : is_strunc n E) (H : n < k)
   : is_contr (πₛ[k] E) :=
-sorry
+let m := n + (2 - k) in
+have I : m < 2, from
+  calc
+    m = (2 - k) + n : int.add_comm n (2 - k)
+  ... < (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)))
+  (nat.succ_le_succ (max0_le_of_le (le_sub_one_of_lt I)))
 
 end spectrum