From 3cf424ef276a15fcc78637c9609d72c8555794a1 Mon Sep 17 00:00:00 2001
From: Ulrik Buchholtz <ulrikbuchholtz@gmail.com>
Date: Sat, 1 Jul 2017 13:02:23 +0100
Subject: [PATCH] add is_strunc_spi

---
 homotopy/strunc.hlean |  97 ++++++++++++++++++++++++++++++------
 move_to_lib.hlean     | 111 +++++++++++++++++++++++++++++++++++++++---
 2 files changed, 185 insertions(+), 23 deletions(-)

diff --git a/homotopy/strunc.hlean b/homotopy/strunc.hlean
index 4de0e9d..5cc8142 100644
--- a/homotopy/strunc.hlean
+++ b/homotopy/strunc.hlean
@@ -5,26 +5,32 @@ open trunc_index nat
 
 namespace int
 
-  /-
-    The function from integers to truncation indices which sends positive numbers to themselves, and negative
-    numbers to negative 2. In particular -1 is sent to -2, but since we only work with pointed types, that
-    doesn't matter for us -/
-  definition maxm2 [unfold 1] : ℤ → ℕ₋₂ :=
-  λ n, int.cases_on n trunc_index.of_nat (λk, -2)
+  section
+  private definition maxm2_le.lemma₁ {n k : ℕ} : n+(1:int) + -[1+ k] ≤ n :=
+  le.intro (
+    calc n + 1 + -[1+ k] + k = n + 1 - (k + 1) + k : by reflexivity
+                         ... = n                   : sorry)
 
-  definition maxm2_le_maxm0 (n : ℤ) : maxm2 n ≤ max0 n :=
+  private definition maxm2_le.lemma₂ {n : ℕ} {k : ℤ} : -[1+ n] + 1 + k ≤ k :=
+  le.intro (
+    calc -[1+ n] + 1 + k + n = - (n + 1) + 1 + k + n : by reflexivity
+                         ... = k                     : sorry)
+
+  definition maxm2_le (n k : ℤ) : maxm2 (n+1+k) ≤ (maxm1m1 n).+1+2+(maxm1m1 k) :=
   begin
+    rewrite [-(maxm1_eq_succ n)],
     induction n with n n,
-    { exact le.tr_refl n },
-    { exact minus_two_le 0 }
+    { induction k with k k,
+      { induction k with k IH,
+        { apply le.tr_refl },
+        { exact succ_le_succ IH } },
+      { exact trunc_index.le_trans (maxm2_monotone maxm2_le.lemma₁)
+                                   (maxm2_le_maxm1 n) } },
+    { krewrite (add_plus_two_comm -1 (maxm1m1 k)),
+      rewrite [-(maxm1_eq_succ k)],
+      exact trunc_index.le_trans (maxm2_monotone maxm2_le.lemma₂)
+                                 (maxm2_le_maxm1 k) }
   end
-
-  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
@@ -130,4 +136,63 @@ definition str [constructor] (k : ℤ) (E : spectrum) : E →ₛ strunc k E :=
 smap.mk (λ n, ptr (maxm2 (k + n)) (E n))
   (λ n, sorry)
 
+
+structure truncspectrum (n : ℤ) :=
+  (carrier : spectrum)
+  (struct : is_strunc n carrier)
+
+notation n `-spectrum` := truncspectrum n
+
+attribute truncspectrum.carrier [coercion]
+
+definition genspectrum_of_truncspectrum (n : ℤ)
+  : n-spectrum → gen_spectrum +ℤ :=
+λ E, truncspectrum.carrier E
+
+attribute genspectrum_of_truncspectrum [coercion]
+
+section
+
+  open is_conn
+
+  definition is_conn_maxm1_of_maxm2 (A : Type*) (n : ℤ)
+    : is_conn (maxm2 n) A → is_conn (maxm1m1 n).+1 A :=
+  begin
+    intro H, induction n with n n,
+    { exact H },
+    { exact is_conn_minus_one A (tr pt) }
+  end
+
+  definition is_trunc_maxm2_of_maxm1 (A : Type*) (n : ℤ)
+    : is_trunc (maxm1m1 n).+1 A → is_trunc (maxm2 n) A :=
+  begin
+    intro H, induction n with n n,
+    { exact H},
+    { apply is_contr_of_merely_prop,
+      { exact H },
+      { exact tr pt } }
+  end
+
+  variables (A : Type*) (n : ℤ) [H : is_conn (maxm2 n) A]
+  include H
+
+  definition is_trunc_maxm2_ppi (k : ℤ) (P : A → (maxm2 (n+1+k))-Type*)
+    : is_trunc (maxm2 k) (Π*(a : A), P a) :=
+  is_trunc_maxm2_of_maxm1 (Π*(a : A), P a) k
+    (@is_trunc_ppi A (maxm1m1 n)
+      (is_conn_maxm1_of_maxm2 A n H) (maxm1m1 k)
+      (λ a, ptrunctype.mk (P a) (is_trunc_of_le (P a) (maxm2_le n k)) pt))
+
+  definition is_strunc_spi (k : ℤ) (P : A → (n+1+k)-spectrum)
+    : is_strunc k (spi A P) :=
+  begin
+    intro m, unfold spi,
+    exact is_trunc_maxm2_ppi A n (k+m)
+      (λ a, ptrunctype.mk (P a m)
+       (is_trunc_maxm2_change_int (P a m) (add.assoc (n+1) k m)
+         (truncspectrum.struct (P a) m)) pt)
+  end
+
+end
+
 end spectrum
diff --git a/move_to_lib.hlean b/move_to_lib.hlean
index 0be4007..217faf4 100644
--- a/move_to_lib.hlean
+++ b/move_to_lib.hlean
@@ -139,6 +139,110 @@ namespace nat
 
 end nat
 
+
+namespace trunc_index
+  open is_conn nat trunc is_trunc
+  lemma minus_two_add_plus_two (n : ℕ₋₂) : -2+2+n = n :=
+  by induction n with n p; reflexivity; exact ap succ p
+
+  protected definition of_nat_monotone {n k : ℕ} : n ≤ k → of_nat n ≤ of_nat k :=
+  begin
+    intro H, induction H with k H K,
+    { apply le.tr_refl },
+    { apply le.step K }
+  end
+
+  lemma add_plus_two_comm (n k : ℕ₋₂) : n +2+ k = k +2+ n :=
+  begin
+    induction n with n IH,
+    { exact minus_two_add_plus_two k },
+    { exact !succ_add_plus_two ⬝ ap succ IH}
+  end
+
+end trunc_index
+
+namespace int
+
+  open trunc_index
+  /-
+    The function from integers to truncation indices which sends
+    positive numbers to themselves, and negative numbers to negative
+    2. In particular -1 is sent to -2, but since we only work with
+    pointed types, that doesn't matter for us -/
+  definition maxm2 [unfold 1] : ℤ → ℕ₋₂ :=
+  λ n, int.cases_on n trunc_index.of_nat (λk, -2)
+
+  -- we also need the max -1 - function
+  definition maxm1 [unfold 1] : ℤ → ℕ₋₂ :=
+  λ n, int.cases_on n trunc_index.of_nat (λk, -1)
+
+  definition maxm2_le_maxm1 (n : ℤ) : maxm2 n ≤ maxm1 n :=
+  begin
+    induction n with n n,
+    { exact le.tr_refl n },
+    { exact minus_two_le -1 }
+  end
+
+  -- the is maxm1 minus 1
+  definition maxm1m1 [unfold 1] : ℤ → ℕ₋₂ :=
+  λ n, int.cases_on n (λ k, k.-1) (λ k, -2)
+
+  definition maxm1_eq_succ (n : ℤ) : maxm1 n = (maxm1m1 n).+1 :=
+  begin
+    induction n with n n,
+    { reflexivity },
+    { reflexivity }
+  end
+
+  definition maxm2_le_maxm0 (n : ℤ) : maxm2 n ≤ max0 n :=
+  begin
+    induction n with n n,
+    { exact le.tr_refl n },
+    { exact minus_two_le 0 }
+  end
+
+  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
+
+  section
+  -- is there a way to get this from int.add_assoc?
+  private definition maxm2_monotone.lemma₁ {n k : ℕ}
+    : k + n + (1:int) = k + (1:int) + n :=
+  begin
+    induction n with n IH,
+    { reflexivity },
+    { exact ap (λ z, z + 1) IH }
+  end
+
+  private definition maxm2_monotone.lemma₂ {n k : ℕ} : ¬ n ≤ -[1+ k] :=
+  int.not_le_of_gt (lt.intro
+    (calc -[1+ k] + (succ (k + n))
+         = -(k+1) + (k + n + 1) : by reflexivity
+     ... = -(k+1) + (k + 1 + n) : maxm2_monotone.lemma₁
+     ... = (-(k+1) + (k+1)) + n : int.add_assoc
+     ... = (0:int) + n          : by rewrite int.add_left_inv
+     ... = n                    : int.zero_add))
+
+  definition maxm2_monotone {n k : ℤ} : n ≤ k → maxm2 n ≤ maxm2 k :=
+  begin
+    intro H,
+    induction n with n n,
+    { induction k with k k,
+      { exact trunc_index.of_nat_monotone (le_of_of_nat_le_of_nat H) },
+      { exact empty.elim (maxm2_monotone.lemma₂ H) } },
+    { induction k with k k,
+      { apply minus_two_le },
+      { apply le.tr_refl } }
+  end
+  end
+
+end int
+
 namespace pmap
 
   definition eta {A B : Type*} (f : A →* B) : pmap.mk f (respect_pt f) = f :=
@@ -184,13 +288,6 @@ namespace trunc
 
 end trunc
 
-namespace trunc_index
-  open is_conn nat trunc is_trunc
-  lemma minus_two_add_plus_two (n : ℕ₋₂) : -2+2+n = n :=
-  by induction n with n p; reflexivity; exact ap succ p
-
-end trunc_index
-
 namespace sigma
 
   -- definition sigma_pathover_equiv_of_is_prop {A : Type} {B : A → Type} {C : Πa, B a → Type}