diff --git a/algebra/left_module.hlean b/algebra/left_module.hlean
index 0de50d3..e7eff94 100644
--- a/algebra/left_module.hlean
+++ b/algebra/left_module.hlean
@@ -421,7 +421,6 @@ end
       (λa, to_right_inv (equiv_of_isomorphism eB) _) (λb, to_right_inv (equiv_of_isomorphism eC) _)
       (short_exact_mod.h H))
 
-
   end
 
   end
diff --git a/algebra/module_exact_couple.hlean b/algebra/module_exact_couple.hlean
index 80c4762..6843cab 100644
--- a/algebra/module_exact_couple.hlean
+++ b/algebra/module_exact_couple.hlean
@@ -451,6 +451,52 @@ namespace left_module
   -- print axioms Dinfdiag0
   -- print axioms Dinfdiag_stable
 
+  open int group prod convergence_theorem prod.ops
+
+  definition Z2 [constructor] : Set := gℤ ×g gℤ
+
+  structure converges_to.{u v w} {R : Ring} (E' : gℤ → gℤ → LeftModule.{u v} R)
+                                 (Dinf : graded_module.{u 0 w} R gℤ) : Type.{max u (v+1) (w+1)} :=
+    (X : exact_couple.{u 0 v w} R Z2)
+    (HH : is_bounded X)
+    (e : Π(x : gℤ ×g gℤ), exact_couple.E X x ≃lm E' x.1 x.2)
+    (s₀ : gℤ)
+    (p : Π(n : gℤ), is_bounded.B' HH (deg (k X) (n, s₀)) = 0)
+    (f : Π(n : gℤ), exact_couple.D X (deg (k X) (n, s₀)) ≃lm Dinf n)
+
+  infix ` ⟹ `:25 := converges_to
+
+  definition converges_to_g [reducible] (E' : gℤ → gℤ → AbGroup) (Dinf : gℤ → AbGroup) : Type :=
+  (λn s, LeftModule_int_of_AbGroup (E' n s)) ⟹ (λn, LeftModule_int_of_AbGroup (Dinf n))
+
+  infix ` ⟹ᵍ `:25 := converges_to_g
+
+  section
+  open converges_to
+  parameters {R : Ring} {E' : gℤ → gℤ → LeftModule R} {Dinf : graded_module R gℤ} (c : E' ⟹ Dinf)
+  local abbreviation X := X c
+  local abbreviation HH := HH c
+  local abbreviation s₀ := s₀ c
+  local abbreviation Dinfdiag (n : gℤ) (k : ℕ) := Dinfdiag X HH (n, s₀) k
+  local abbreviation Einfdiag (n : gℤ) (k : ℕ) := Einfdiag X HH (n, s₀) k
+
+  include c
+
+  theorem is_contr_converges_to (H : Π(n s : gℤ), is_contr (E' n s)) (n : gℤ) : is_contr (Dinf n) :=
+  begin
+    assert H2 : Π(m : gℤ) (k : ℕ), is_contr (Einfdiag m k),
+    { intro m k, apply is_contr_E, exact is_trunc_equiv_closed_rev -2 (equiv_of_isomorphism (e c _)) },
+    assert H3 : Π(m : gℤ), is_contr (Dinfdiag m 0),
+    { intro m, fapply nat.rec_down (λk, is_contr (Dinfdiag m k)),
+      { exact is_bounded.B HH (deg (k X) (m, s₀)) },
+      { apply Dinfdiag_stable, reflexivity },
+      { intro k H, exact sorry /-note zz := is_contr_middle_of_is_exact (short_exact_mod_infpage k)-/ }},
+    refine @is_trunc_equiv_closed _ _ _ _ (H3 n),
+    apply equiv_of_isomorphism,
+    exact Dinfdiag0 X HH (n, s₀) (p c n) ⬝lm f c n
+  end
+  end
+
 end left_module
 open left_module
 namespace pointed
@@ -485,8 +531,7 @@ namespace pointed
   open prod prod.ops fiber
   parameters {A : ℤ → Type*[1]} (f : Π(n : ℤ), A n →* A (n - 1)) [Hf : Πn, is_conn_fun 1 (f n)]
   include Hf
-  protected definition I [constructor] : Set := trunctype.mk (gℤ ×g gℤ) !is_trunc_prod
-  local abbreviation I := @pointed.I
+  local abbreviation I [constructor] := Z2
 
   -- definition D_sequence : graded_module rℤ I :=
   -- λv, LeftModule_int_of_AbGroup (πc[v.2] (A (v.1)))
@@ -510,8 +555,8 @@ namespace spectrum
 
   parameters {A : ℤ → spectrum} (f : Π(s : ℤ), A s →ₛ A (s - 1))
 
-  protected definition I [constructor] : Set := trunctype.mk (gℤ ×g gℤ) !is_trunc_prod
-  local abbreviation I := @spectrum.I
+--  protected definition I [constructor] : Set := gℤ ×g gℤ
+  local abbreviation I [constructor] := Z2
 
   definition D_sequence : graded_module rℤ I :=
   λv, LeftModule_int_of_AbGroup (πₛ[v.1] (A (v.2)))
@@ -588,8 +633,8 @@ namespace spectrum
 
   open int
   parameters (ub : ℤ) (lb : ℤ → ℤ)
-    (Aub : Πs n, s ≥ ub + 1 → is_equiv (f s n))
-    (Alb : Πs n, s ≤ lb n → is_contr (πₛ[n] (A s)))
+    (Aub : Π(s n : ℤ), s ≥ ub + 1 → is_equiv (f s n))
+    (Alb : Π(s n : ℤ), s ≤ lb n → is_contr (πₛ[n] (A s)))
 
   definition B : I → ℕ
   | (n, s) := max0 (s - lb n)
@@ -652,6 +697,17 @@ namespace spectrum
       refine !add.assoc ⬝ ap (add s) !add.comm ⬝ !add.assoc⁻¹,
     end
 
+  definition converges_to_sequence : (λn s, πₛ[n] (sfiber (f s))) ⟹ᵍ (λn, πₛ[n] (A ub)) :=
+  begin
+    fapply converges_to.mk,
+    { exact exact_couple_sequence },
+    { exact is_bounded_sequence },
+    { intros, reflexivity },
+    { exact ub },
+    { intro n, change max0 (ub - ub) = 0, exact ap max0 (sub_self ub) },
+    { intro n, reflexivity }
+  end
+
   end
 
 -- Uncomment the next line to see that the proof uses univalence, but that there are no holes
diff --git a/algebra/product_group.hlean b/algebra/product_group.hlean
index 2bd56d1..066e18a 100644
--- a/algebra/product_group.hlean
+++ b/algebra/product_group.hlean
@@ -1,7 +1,7 @@
 /-
 Copyright (c) 2015 Floris van Doorn. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Floris van Doorn, Egbert Rijke
+Authors: Floris van Doorn, Egbert Rijke, Favonia
 
 Constructions with groups
 -/
diff --git a/algebra/seq_colim.hlean b/algebra/seq_colim.hlean
index 2de1070..ee1ddb1 100644
--- a/algebra/seq_colim.hlean
+++ b/algebra/seq_colim.hlean
@@ -1,3 +1,5 @@
+--Authors: Robert Rose, Liz Vidaurre
+
 import .direct_sum .quotient_group ..move_to_lib
 
 open eq algebra is_trunc set_quotient relation sigma prod sum list trunc function equiv sigma.ops nat
diff --git a/colim.hlean b/colim.hlean
index 1e5c279..5d398a6 100644
--- a/colim.hlean
+++ b/colim.hlean
@@ -1,4 +1,4 @@
--- authors: Floris van Doorn, Egbert Rijke
+-- authors: Floris van Doorn, Egbert Rijke, Stefano Piceghello
 
 import hit.colimit types.fin homotopy.chain_complex types.pointed2
 open seq_colim pointed algebra eq is_trunc nat is_equiv equiv sigma sigma.ops chain_complex
diff --git a/homology/homology.hlean b/homology/homology.hlean
index 51f6400..4b52be5 100644
--- a/homology/homology.hlean
+++ b/homology/homology.hlean
@@ -1,7 +1,7 @@
 /-
 Copyright (c) 2017 Yuri Sulyma, Favonia
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Yuri Sulyma, Favonia
+Authors: Yuri Sulyma, Favonia, Floris van Doorn
 
 Reduced homology theories
 -/
diff --git a/homotopy/EM.hlean b/homotopy/EM.hlean
index 28b8b3d..aa95281 100644
--- a/homotopy/EM.hlean
+++ b/homotopy/EM.hlean
@@ -570,24 +570,4 @@ namespace EM
     abstract (EMadd1_functor_gcompose φ φ⁻¹ᵍ n)⁻¹* ⬝* EMadd1_functor_phomotopy proof right_inv φ qed n ⬝*
              EMadd1_functor_gid H n end
 
-  /- Eilenberg MacLane spaces are the fibers of the Postnikov system of a type -/
-
-  definition postnikov_map [constructor] (A : Type*) (n : ℕ₋₂) : ptrunc (n.+1) A →* ptrunc n A :=
-  ptrunc.elim (n.+1) !ptr
-
-  open fiber
-
-  definition pfiber_postnikov_map (A : Type*) (n : ℕ) : pfiber (postnikov_map A n) ≃* EM_type A (n+1) :=
-  begin
-    symmetry, apply EM_type_pequiv,
-    { symmetry, refine _ ⬝g ghomotopy_group_ptrunc (n+1) A,
-      exact chain_complex.LES_isomorphism_of_trivial_cod _ _
-        (trivial_homotopy_group_of_is_trunc _ (self_lt_succ n))
-        (trivial_homotopy_group_of_is_trunc _ (le_succ _)) },
-    { apply is_conn_fun_trunc_elim,  apply is_conn_fun_tr },
-    { have is_trunc (n+1) (ptrunc n.+1 A), from !is_trunc_trunc,
-      have is_trunc ((n+1).+1) (ptrunc n A), by do 2 apply is_trunc_succ, apply is_trunc_trunc,
-      apply is_trunc_pfiber }
-  end
-
 end EM
diff --git a/homotopy/fwedge.hlean b/homotopy/fwedge.hlean
index a89bcc4..f870237 100644
--- a/homotopy/fwedge.hlean
+++ b/homotopy/fwedge.hlean
@@ -1,7 +1,7 @@
 /-
 Copyright (c) 2016 Jakob von Raumer. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Floris van Doorn
+Authors: Floris van Doorn, Favonia
 
 The Wedge Sum of a family of Pointed Types
 -/
diff --git a/homotopy/pushout.hlean b/homotopy/pushout.hlean
index 5ddffd7..38f7a8f 100644
--- a/homotopy/pushout.hlean
+++ b/homotopy/pushout.hlean
@@ -485,6 +485,11 @@ namespace pushout
       apply eq_inv_con_of_con_eq, exact (to_homotopy_pt p)⁻¹ }
   end
 
+  /-
+    The maps  Z^{C_f} --> Z^Y --> Z^X  are exact at Z^Y.
+    Here Y^X means pointed maps from X to Y and C_f is the cofiber of f.
+    The maps are given by precomposing with (pcod f) and f.
+  -/
   definition cofiber_exact {X Y Z : Type*} (f : X →* Y) :
     is_exact_t (@ppcompose_right _ _ Z (pcod f)) (ppcompose_right f) :=
   begin
diff --git a/homotopy/serre.hlean b/homotopy/serre.hlean
new file mode 100644
index 0000000..4946217
--- /dev/null
+++ b/homotopy/serre.hlean
@@ -0,0 +1,116 @@
+import ..algebra.module_exact_couple .strunc
+
+open eq spectrum trunc is_trunc pointed int EM algebra left_module fiber lift
+
+/- Eilenberg MacLane spaces are the fibers of the Postnikov system of a type -/
+
+definition postnikov_map [constructor] (A : Type*) (n : ℕ₋₂) : ptrunc (n.+1) A →* ptrunc n A :=
+ptrunc.elim (n.+1) !ptr
+
+definition ptrunc_functor_postnikov_map {A B : Type*} (n : ℕ₋₂) (f : A →* B) :
+  ptrunc_functor n f ∘* postnikov_map A n ~* ptrunc.elim (n.+1) (!ptr ∘* f) :=
+begin
+  fapply phomotopy.mk,
+  { intro x, induction x with a, reflexivity },
+  { reflexivity }
+end
+
+section
+open nat is_conn group
+definition pfiber_postnikov_map (A : Type*) (n : ℕ) :
+  pfiber (postnikov_map A n) ≃* EM_type A (n+1) :=
+begin
+  symmetry, apply EM_type_pequiv,
+  { symmetry, refine _ ⬝g ghomotopy_group_ptrunc (n+1) A,
+    exact chain_complex.LES_isomorphism_of_trivial_cod _ _
+      (trivial_homotopy_group_of_is_trunc _ (self_lt_succ n))
+      (trivial_homotopy_group_of_is_trunc _ (le_succ _)) },
+  { apply is_conn_fun_trunc_elim,  apply is_conn_fun_tr },
+  { have is_trunc (n+1) (ptrunc n.+1 A), from !is_trunc_trunc,
+    have is_trunc ((n+1).+1) (ptrunc n A), by do 2 apply is_trunc_succ, apply is_trunc_trunc,
+    apply is_trunc_pfiber }
+end
+end
+
+definition postnikov_map_natural {A B : Type*} (f : A →* B) (n : ℕ₋₂) :
+  psquare (postnikov_map A n) (postnikov_map B n)
+          (ptrunc_functor (n.+1) f) (ptrunc_functor n f) :=
+!ptrunc_functor_postnikov_map ⬝* !ptrunc_elim_ptrunc_functor⁻¹*
+
+definition encode_ap1_gen_tr (n : ℕ₋₂) {A : Type*} {a a' : A} (p : a = a') :
+  trunc.encode (ap1_gen tr idp idp p) = tr p :> trunc n (a = a') :=
+by induction p; reflexivity
+
+definition ap1_postnikov_map (A : Type*) (n : ℕ₋₂) :
+  psquare (Ω→ (postnikov_map A (n.+1))) (postnikov_map (Ω A) n)
+          (loop_ptrunc_pequiv (n.+1) A) (loop_ptrunc_pequiv n A) :=
+have psquare (postnikov_map (Ω A) n) (Ω→ (postnikov_map A (n.+1)))
+             (loop_ptrunc_pequiv (n.+1) A)⁻¹ᵉ* (loop_ptrunc_pequiv n A)⁻¹ᵉ*,
+begin
+  refine _ ⬝* !ap1_ptrunc_elim⁻¹*, apply pinv_left_phomotopy_of_phomotopy,
+  fapply phomotopy.mk,
+  { intro x, induction x with p, exact !encode_ap1_gen_tr⁻¹ },
+  { reflexivity }
+end,
+this⁻¹ᵛ*
+
+
+-- definition postnikov_map_int (X : Type*) (k : ℤ) :
+--   ptrunc (maxm2 (k + 1)) X →* ptrunc (maxm2 k) X :=
+-- begin
+--   induction k with k k,
+--     exact postnikov_map X k,
+--   exact !pconst
+-- end
+
+-- definition postnikov_map_int_natural {A B : Type*} (f : A →* B) (k : ℤ) :
+--   psquare (postnikov_map_int A k) (postnikov_map_int B k)
+--           (ptrunc_int_functor (k+1) f) (ptrunc_int_functor k f) :=
+-- begin
+--   induction k with k k,
+--     exact postnikov_map_natural f k,
+--   apply psquare_of_phomotopy, exact !pcompose_pconst ⬝* !pconst_pcompose⁻¹*
+-- end
+
+-- definition postnikov_map_int_natural_pequiv {A B : Type*} (f : A ≃* B) (k : ℤ) :
+--   psquare (postnikov_map_int A k) (postnikov_map_int B k)
+--           (ptrunc_int_pequiv_ptrunc_int (k+1) f) (ptrunc_int_pequiv_ptrunc_int k f) :=
+-- begin
+--   induction k with k k,
+--     exact postnikov_map_natural f k,
+--   apply psquare_of_phomotopy, exact !pcompose_pconst ⬝* !pconst_pcompose⁻¹*
+-- end
+
+-- definition pequiv_ap_natural2 {X A : Type} (B C : X → A → Type*) {a a' : X → A}
+--   (p : a ~ a')
+--   (s : X → X) (f : Πx a, B x a →* C (s x) a) (x : X) :
+--   psquare (pequiv_ap (B x) (p x)) (pequiv_ap (C (s x)) (p x)) (f x (a x)) (f x (a' x)) :=
+-- begin induction p using homotopy.rec_on_idp, exact phrfl end
+
+-- definition pequiv_ap_natural3 {X A : Type} (B C : X → A → Type*) {a a' : A}
+--   (p : a = a')
+--   (s : X → X) (x : X) (f : Πx a, B x a →* C (s x) a) :
+--   psquare (pequiv_ap (B x) p) (pequiv_ap (C (s x)) p) (f x a) (f x a') :=
+-- begin induction p, exact phrfl end
+
+-- definition postnikov_smap (X : spectrum) (k : ℤ) :
+--   strunc (k+1) X →ₛ strunc k X :=
+-- smap.mk (λn, postnikov_map_int (X n) (k + n) ∘* ptrunc_int_change_int _ !norm_num.add_comm_middle)
+--         (λn, begin
+--                exact sorry
+-- --             exact (_ ⬝vp* !ap1_pequiv_ap) ⬝h* (!postnikov_map_int_natural_pequiv ⬝v* _ ⬝v* _) ⬝vp* !ap1_pcompose,
+--              end)
+
+
+-- section atiyah_hirzebruch
+--   parameters {X : Type*} (Y : X → spectrum)
+
+--   definition atiyah_hirzebruch_exact_couple : exact_couple rℤ spectrum.I :=
+--   @exact_couple_sequence (λs, strunc s (spi X (λx, Y x)))
+--                          (λs, !postnikov_smap ∘ₛ strunc_change_int _ !succ_pred⁻¹)
+
+-- --  parameters (k : ℕ) (H : Π(x : X) (n : ℕ), is_trunc (k + n) (Y x n))
+
+
+
+-- end atiyah_hirzebruch
diff --git a/homotopy/smash_adjoint.hlean b/homotopy/smash_adjoint.hlean
index 5c0892a..93121bc 100644
--- a/homotopy/smash_adjoint.hlean
+++ b/homotopy/smash_adjoint.hlean
@@ -570,6 +570,9 @@ namespace smash
   smash_iterate_psusp n A pbool ⬝e*
   iterate_psusp_pequiv n (smash_pbool_pequiv A)
 
+  definition smash_pcircle (A : Type*) : A ∧ pcircle ≃* psusp A :=
+  smash_sphere A 1
+
   definition sphere_smash_sphere (n m : ℕ) : psphere n ∧ psphere m ≃* psphere (n+m) :=
   smash_sphere (psphere n) m ⬝e*
   iterate_psusp_pequiv m (psphere_pequiv_iterate_psusp n) ⬝e*
diff --git a/homotopy/spectrum.hlean b/homotopy/spectrum.hlean
index f1ca5ee..0f6a3b6 100644
--- a/homotopy/spectrum.hlean
+++ b/homotopy/spectrum.hlean
@@ -1,7 +1,7 @@
 /-
 Copyright (c) 2016 Michael Shulman. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Michael Shulman, Floris van Doorn
+Authors: Michael Shulman, Floris van Doorn, Stefano Piceghello, Yuri Sulyma
 
 -/
 
diff --git a/homotopy/strunc.hlean b/homotopy/strunc.hlean
index 684933f..5cc8142 100644
--- a/homotopy/strunc.hlean
+++ b/homotopy/strunc.hlean
@@ -5,27 +5,32 @@ 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))
+  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)
 
-  attribute maxm2 [unfold 1]
+  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_maxm0 (n : ℤ) : maxm2 n ≤ max0 n :=
+  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 },
-    { cases n with n,
-      { exact le.step (le.tr_refl -1) },
-      { 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
@@ -43,14 +48,11 @@ definition loop_ptrunc_maxm2_pequiv (k : ℤ) (X : Type*) :
 begin
   induction k with k k,
   { 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)))⁻¹ᵉ* } } }
+  { refine pequiv_of_is_contr _ _ _ !is_trunc_trunc,
+    apply is_contr_loop,
+    cases k with k,
+    { change is_set (trunc 0 X), apply _ },
+    { change is_set (trunc -2 X), apply _ }}
 end
 
 definition is_trunc_of_is_trunc_maxm2 (k : ℤ) (X : Type)
@@ -73,14 +75,12 @@ definition is_trunc_maxm2_loop (A : pType) (k : ℤ)
 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 } } }
+  { apply is_contr_loop, cases k with k,
+    { exact H },
+    { have H2 : is_contr A, from H, apply _ } }
 end
 
-definition is_strunc (k : ℤ) (E : spectrum) : Type :=
+definition is_strunc [reducible] (k : ℤ) (E : spectrum) : Type :=
 Π (n : ℤ), is_trunc (maxm2 (k + n)) (E n)
 
 definition is_strunc_change_int {k l : ℤ} (E : spectrum) (p : k = l)
@@ -95,6 +95,10 @@ 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 strunc_functor [constructor] (k : ℤ) {E F : spectrum} (f : E →ₛ F) :
+  strunc k E →ₛ strunc k F :=
+smap.mk (λn, ptrunc_functor (maxm2 (k + n)) (f n)) sorry
+
 definition is_strunc_EM_spectrum (G : AbGroup)
   : is_strunc 0 (EM_spectrum G) :=
 begin
@@ -102,13 +106,19 @@ begin
   { -- case ≥ 0
     apply is_trunc_maxm2_change_int (EM G n) (zero_add n)⁻¹,
     apply is_trunc_EM },
-  { induction n with n IH,
+  { change is_contr (EM_spectrum G (-[1+n])),
+    induction n with n IH,
     { -- case = -1
-      apply is_trunc_loop, exact ab_group.is_set_carrier G },
+      apply is_contr_loop, exact is_trunc_EM G 0 },
     { -- case < -1
-      apply is_trunc_maxm2_loop, exact IH }}
+      apply is_trunc_loop, apply is_trunc_succ, exact IH }}
 end
 
+definition strunc_elim [constructor] {k : ℤ} {E F : spectrum} (f : E →ₛ F)
+  (H : is_strunc k F) : strunc k E →ₛ F :=
+smap.mk (λn, ptrunc.elim (maxm2 (k + n)) (f n))
+        (λn, sorry)
+
 definition trivial_shomotopy_group_of_is_strunc (E : spectrum)
   {n k : ℤ} (K : is_strunc n E) (H : n < k)
   : is_contr (πₛ[k] E) :=
@@ -126,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 899739a..217faf4 100644
--- a/move_to_lib.hlean
+++ b/move_to_lib.hlean
@@ -120,6 +120,129 @@ namespace eq
 
 end eq open eq
 
+namespace nat
+
+  protected definition rec_down (P : ℕ → Type) (s : ℕ) (H0 : P s) (Hs : Πn, P (n+1) → P n) : P 0 :=
+  have Hp : Πn, P n → P (pred n),
+  begin
+    intro n p, cases n with n,
+    { exact p },
+    { exact Hs n p }
+  end,
+  have H : Πn, P (s - n),
+  begin
+    intro n, induction n with n p,
+    { exact H0 },
+    { exact Hp (s - n) p }
+  end,
+  transport P (nat.sub_self s) (H s)
+
+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 :=
@@ -165,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}
diff --git a/pointed.hlean b/pointed.hlean
index 62adf6c..f1e1e85 100644
--- a/pointed.hlean
+++ b/pointed.hlean
@@ -192,15 +192,22 @@ namespace pointed
     psquare (pequiv_ap B p) (pequiv_ap C p) (f a) (f a') :=
   begin induction p, exact phrfl end
 
-  definition pequiv_ap_natural2 {A : Type} (B C : A → Type*) {a a' : A} (p : a = a')
-    (f : Πa, B a →* C a) :
-    psquare (pequiv_ap B p) (pequiv_ap C p) (f a) (f a') :=
-  begin induction p, exact phrfl end
+  definition is_contr_loop (A : Type*) [is_set A] : is_contr (Ω A) :=
+  is_contr.mk idp (λa, !is_prop.elim)
+
+  definition pequiv_of_is_contr (A B : Type*) (HA : is_contr A) (HB : is_contr B) : A ≃* B :=
+  pequiv_punit_of_is_contr A _ ⬝e* (pequiv_punit_of_is_contr B _)⁻¹ᵉ*
 
   definition loop_pequiv_punit_of_is_set (X : Type*) [is_set X] : Ω X ≃* punit :=
-  pequiv_punit_of_is_contr _ (is_contr_of_inhabited_prop pt)
+  pequiv_punit_of_is_contr _ (is_contr_loop X)
 
   definition loop_punit : Ω punit ≃* punit :=
   loop_pequiv_punit_of_is_set punit
 
+  definition phomotopy_of_is_contr [constructor] {X Y: Type*} (f g : X →* Y) [is_contr Y] :
+    f ~* g :=
+  phomotopy.mk (λa, !eq_of_is_contr) !eq_of_is_contr
+
+
+
 end pointed
diff --git a/susp_product.hlean b/susp_product.hlean
index ad3d9a1..7c31e4b 100644
--- a/susp_product.hlean
+++ b/susp_product.hlean
@@ -2,4 +2,4 @@ import core
 open susp smash pointed wedge prod
 
 definition susp_product (X Y : Type*) : ⅀ (X × Y) ≃* ⅀ X ∨ (⅀ Y ∨ ⅀ (X ∧ Y)) :=
-  sorry
+sorry