From be802be170aa71b711dc4575938aef6cf4c1f72f Mon Sep 17 00:00:00 2001
From: Floris van Doorn <fpv@andrew.cmu.edu>
Date: Wed, 7 Jun 2017 11:34:09 -0400
Subject: [PATCH 01/24] fix [unfold] index

---
 algebra/free_group.hlean | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/algebra/free_group.hlean b/algebra/free_group.hlean
index 291a4a8..e8f53c0 100644
--- a/algebra/free_group.hlean
+++ b/algebra/free_group.hlean
@@ -60,10 +60,10 @@ namespace group
   end
 
   definition free_group_one [constructor] : FG X := class_of []
-  definition free_group_inv [unfold 4] : FG X → FG X :=
+  definition free_group_inv [unfold 3] : FG X → FG X :=
   quotient_unary_map (reverse ∘ map sum.flip)
                      (λl l', trunc_functor -1 (rel_respect_reverse ∘ rel_respect_flip))
-  definition free_group_mul [unfold 4 5] : FG X → FG X → FG X :=
+  definition free_group_mul [unfold 3 4] : FG X → FG X → FG X :=
   quotient_binary_map append (λl l', trunc.elim (λr m m', trunc.elim (λs, tr (resp_append r s))))
 
   section

From 8639eaff7a2fda488bd1cea3c0ba32142e7014d4 Mon Sep 17 00:00:00 2001
From: favonia <favonia@gmail.com>
Date: Wed, 7 Jun 2017 09:38:33 -0600
Subject: [PATCH 02/24] Fix the statement of susp_product.

---
 susp_product.hlean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/susp_product.hlean b/susp_product.hlean
index 3de39d6..ad3d9a1 100644
--- a/susp_product.hlean
+++ b/susp_product.hlean
@@ -1,5 +1,5 @@
 import core
 open susp smash pointed wedge prod
 
-definition susp_product (X Y : Type*) : ⅀ (X × Y) ≃* ⅀ X ∨ (⅀ Y ∨ (X ∧ Y)) :=
+definition susp_product (X Y : Type*) : ⅀ (X × Y) ≃* ⅀ X ∨ (⅀ Y ∨ ⅀ (X ∧ Y)) :=
   sorry

From abe46fd211719a6617fa4662148f47404e319562 Mon Sep 17 00:00:00 2001
From: Yuri Sulyma <yuri.sulyma@gmail.com>
Date: Wed, 7 Jun 2017 09:39:26 -0600
Subject: [PATCH 03/24] Functoriality of smashing a pointed space with a
 prespectrum

---
 homotopy/spectrum.hlean | 17 +++++++++++++++++
 move_to_lib.hlean       | 31 ++++++++++++++++++++++++++++++-
 2 files changed, 47 insertions(+), 1 deletion(-)

diff --git a/homotopy/spectrum.hlean b/homotopy/spectrum.hlean
index 0cf3cf0..735fcbc 100644
--- a/homotopy/spectrum.hlean
+++ b/homotopy/spectrum.hlean
@@ -454,6 +454,23 @@ prespectrum.mk (λ z, X ∧ Y z) begin
   exact !glue
 end
 
+definition smash_prespectrum_fun {X X' : Type*} {Y Y' : prespectrum} (f : X →* X') (g : Y →ₛ Y') : smash_prespectrum X Y →ₛ smash_prespectrum X' Y' :=
+begin
+  refine smap.mk (λn, smash_functor f (g n)) _,
+  intro n,
+  refine susp_to_loop_psquare _ _ _ _ _,
+  refine pvconcat (psquare_transpose (phinverse (smash_psusp_natural f (g n)))) _,
+  refine vconcat_phomotopy _ (smash_functor_split f (g (S n))),
+  refine phomotopy_vconcat (smash_functor_split f (psusp_functor (g n))) _,
+  refine phconcat _ _,
+  let glue_adjoint := psusp_pelim (Y n) (Y (S n)) (glue Y n),
+  exact pid X' ∧→ glue_adjoint,
+  exact smash_functor_psquare (pvrefl f) (phrefl glue_adjoint),
+  refine smash_functor_psquare (phrefl (pid X')) _,
+  refine loop_to_susp_square _ _ _ _ _,
+  exact smap.glue_square g n
+end
+
   /- Cofibers and stability -/
 
   /- The Eilenberg-MacLane spectrum -/
diff --git a/move_to_lib.hlean b/move_to_lib.hlean
index 59cd841..2f745a8 100644
--- a/move_to_lib.hlean
+++ b/move_to_lib.hlean
@@ -1,6 +1,6 @@
 -- definitions, theorems and attributes which should be moved to files in the HoTT library
 
-import homotopy.sphere2 homotopy.cofiber homotopy.wedge hit.prop_trunc hit.set_quotient eq2
+import homotopy.sphere2 homotopy.cofiber homotopy.wedge hit.prop_trunc hit.set_quotient eq2 types.pointed2 homotopy.smash_adjoint
 
 open eq nat int susp pointed pmap sigma is_equiv equiv fiber algebra trunc trunc_index pi group
      is_trunc function sphere unit sum prod bool
@@ -536,3 +536,32 @@ open trunc fiber image
   end
 
 end injective_surjective
+
+-- Yuri Sulyma's code from HoTT MRC
+
+notation `⅀→`:(max+5) := psusp_functor
+
+namespace pointed
+  variables {A₀₀ A₂₀ A₀₂ A₂₂ : Type*}
+            {f₁₀ : A₀₀ →* A₂₀} {f₁₂ : A₀₂ →* A₂₂}
+            {f₀₁ : A₀₀ →* A₀₂} {f₂₁ : A₂₀ →* A₂₂}
+
+  definition psquare_transpose (p : psquare f₁₀ f₁₂ f₀₁ f₂₁) : psquare f₀₁ f₂₁ f₁₀ f₁₂ := p⁻¹*
+
+  definition suspend_psquare (p : psquare f₁₀ f₁₂ f₀₁ f₂₁) : psquare (⅀→ f₁₀) (⅀→ f₁₂) (⅀→ f₀₁) (⅀→ f₂₁) :=
+sorry
+
+  definition susp_to_loop_psquare (f₁₀ : A₀₀ →* A₂₀) (f₁₂ : A₀₂ →* A₂₂) (f₀₁ : psusp A₀₀ →* A₀₂) (f₂₁ : psusp A₂₀ →* A₂₂) : (psquare (⅀→ f₁₀) f₁₂ f₀₁ f₂₁) → (psquare f₁₀ (Ω→ f₁₂) ((loop_psusp_pintro A₀₀ A₀₂) f₀₁) ((loop_psusp_pintro A₂₀ A₂₂) f₂₁)) :=
+  begin
+    intro p,
+    refine pvconcat _ (ap1_psquare p),
+    exact loop_psusp_unit_natural f₁₀
+  end
+
+  definition loop_to_susp_square (f₁₀ : A₀₀ →* A₂₀) (f₁₂ : A₀₂ →* A₂₂) (f₀₁ : A₀₀ →* Ω A₀₂) (f₂₁ : A₂₀ →* Ω A₂₂) : (psquare f₁₀ (Ω→ f₁₂) f₀₁ f₂₁) → (psquare (⅀→ f₁₀) f₁₂ ((psusp_pelim A₀₀ A₀₂) f₀₁) ((psusp_pelim A₂₀ A₂₂) f₂₁)) :=
+  begin
+    intro p,
+    refine pvconcat (suspend_psquare p) _,
+    exact psquare_transpose (loop_psusp_counit_natural f₁₂)
+  end
+end pointed

From 0a135fbe913fbc9ddde54921165b0b3c0a6ef245 Mon Sep 17 00:00:00 2001
From: favonia <favonia@gmail.com>
Date: Wed, 7 Jun 2017 09:39:33 -0600
Subject: [PATCH 04/24] Remove useless esimp to speed up Lean.

---
 algebra/direct_sum.hlean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/algebra/direct_sum.hlean b/algebra/direct_sum.hlean
index acc32c3..8596dc3 100644
--- a/algebra/direct_sum.hlean
+++ b/algebra/direct_sum.hlean
@@ -114,7 +114,7 @@ namespace group
     dirsum_functor (λi, homomorphism_mul (f i) (f' i)) :=
   begin
     apply dirsum_homotopy,
-    intro i y, esimp, exact sorry
+    intro i y, exact sorry
   end
 
   definition dirsum_functor_homotopy {f f' : Πi, Y i →g Y' i} (p : f ~2 f') :

From 2e9a225a82051462af240707f75a54ac9ddc8fc9 Mon Sep 17 00:00:00 2001
From: spiceghello <stefano.piceghello@uib.no>
Date: Thu, 8 Jun 2017 09:16:57 -0600
Subject: [PATCH 05/24] minor

---
 colim.hlean | 15 ++++++---------
 1 file changed, 6 insertions(+), 9 deletions(-)

diff --git a/colim.hlean b/colim.hlean
index f1b5467..9be26b7 100644
--- a/colim.hlean
+++ b/colim.hlean
@@ -350,16 +350,11 @@ namespace seq_colim
       apply whisker_right, esimp,
       rewrite[(eq_con_inv_of_con_eq (!to_homotopy_pt))],
       rewrite[ap_con], esimp,
-      rewrite[-+con.assoc],
-      rewrite[ap_con], rewrite[-ap_compose'],
-      rewrite[+ap_inv],
+      rewrite[-+con.assoc, ap_con, -ap_compose', +ap_inv],
       rewrite[-+con.assoc],
       refine _ ⬝ whisker_right _ (whisker_right _ (whisker_right _ (whisker_right _ !con.left_inv⁻¹))),
-      rewrite[idp_con],
-      rewrite[+con.assoc], apply whisker_left,
-      rewrite[ap_con], rewrite[-ap_compose'],
-      rewrite[con_inv],
-      rewrite[+con.assoc], apply whisker_left,
+      rewrite[idp_con, +con.assoc], apply whisker_left,
+      rewrite[ap_con, -ap_compose', con_inv, +con.assoc], apply whisker_left,
       refine eq_inv_con_of_con_eq _,
       symmetry, exact eq_of_square !natural_square
     }
@@ -368,7 +363,9 @@ namespace seq_colim
   definition seq_colim_equiv_constant_pinclusion {A : ℕ → Type*} {f f' : Π⦃n⦄, A n →* A (n+1)}
     (p : Π⦃n⦄ (a : A n), f a = f' a) (n : ℕ) :
     pseq_colim_equiv_constant p ∘* pinclusion f n ~* pinclusion f' n  :=
-  sorry
+  begin
+    sorry
+  end
 
   definition is_equiv_seq_colim_rec (P : seq_colim f → Type) :
     is_equiv (seq_colim_rec_unc :

From 877c740ea93119956529c867c223cbc6db89ca3d Mon Sep 17 00:00:00 2001
From: Floris van Doorn <fpv@andrew.cmu.edu>
Date: Thu, 8 Jun 2017 11:19:29 -0400
Subject: [PATCH 06/24] progress on spectrum and colim

---
 algebra/product_group.hlean |  5 ++++-
 colim.hlean                 | 40 ++++++++++++++++++++++---------------
 homotopy/spectrum.hlean     | 15 ++++++++------
 3 files changed, 37 insertions(+), 23 deletions(-)

diff --git a/algebra/product_group.hlean b/algebra/product_group.hlean
index 75c1d66..c1e090c 100644
--- a/algebra/product_group.hlean
+++ b/algebra/product_group.hlean
@@ -8,7 +8,7 @@ Constructions with groups
 
 import algebra.group_theory hit.set_quotient types.list types.sum .subgroup .quotient_group
 
-open eq algebra is_trunc set_quotient relation sigma sigma.ops prod prod.ops sum list trunc function
+open eq algebra is_trunc set_quotient relation sigma prod prod.ops sum list trunc function
      equiv
 namespace group
 
@@ -79,4 +79,7 @@ namespace group
 
   infix ` ×≃g `:60 := group.product_isomorphism
 
+  definition product_group_mul_eq {G H : Group} (g h : G ×g H) : g * h = product_mul g h :=
+  idp
+
 end group
diff --git a/colim.hlean b/colim.hlean
index 9be26b7..8053718 100644
--- a/colim.hlean
+++ b/colim.hlean
@@ -251,7 +251,7 @@ namespace seq_colim
 
   definition pshift_equiv_pinclusion {A : ℕ → Type*} (f : Πn, A n →* A (succ n)) (n : ℕ) :
     psquare (pinclusion f n) (pinclusion (λn, f (n+1)) n) (f n) (pshift_equiv f)  :=
-  phomotopy.mk homotopy.rfl begin 
+  phomotopy.mk homotopy.rfl begin
     refine !idp_con ⬝ _, esimp,
     induction n with n IH,
     { esimp[inclusion_pt], esimp[shift_diag], exact !idp_con⁻¹ },
@@ -259,7 +259,7 @@ namespace seq_colim
       rewrite ap_con, rewrite ap_con,
       refine _ ⬝ whisker_right _ !con.assoc,
       refine _ ⬝ (con.assoc (_ ⬝ _) _ _)⁻¹,
-      xrewrite [-IH], 
+      xrewrite [-IH],
       esimp[shift_up], rewrite [elim_glue,  ap_inv, -ap_compose'], esimp,
       rewrite [-+con.assoc], apply whisker_right,
       rewrite con.assoc, apply !eq_inv_con_of_con_eq,
@@ -285,7 +285,6 @@ namespace seq_colim
   !elim_glue
 
   omit p
-
   definition is_equiv_seq_colim_functor [constructor] [H : Πn, is_equiv (@g n)]
      : is_equiv (seq_colim_functor @g p) :=
   adjointify _ (seq_colim_functor (λn, (@g _)⁻¹) (λn a, inv_commute' g f f' p a))
@@ -323,25 +322,34 @@ namespace seq_colim
     : Π(x : seq_colim f), P x :=
   by induction v with Pincl Pglue; exact seq_colim.rec f Pincl Pglue
 
-  definition pseq_colim_pequiv [constructor] {A A' : ℕ → Type*} {f : Π{n}, A n →* A (n+1)}
-    {f' : Π{n}, A' n →* A' (n+1)} (g : Π{n}, A n ≃* A' n)
-    (p : Π⦃n⦄, g ∘* f ~ f' ∘* g) : pseq_colim @f ≃* pseq_colim @f' :=
-  pequiv_of_equiv (seq_colim_equiv @g p) (ap (ι _) (respect_pt g))
+  definition pseq_colim_pequiv' [constructor] {A A' : ℕ → Type*} {f : Πn, A n →* A (n+1)}
+    {f' : Πn, A' n →* A' (n+1)} (g : Πn, A n ≃* A' n)
+    (p : Π⦃n⦄, g (n+1) ∘* f n ~ f' n ∘* g n) : pseq_colim @f ≃* pseq_colim @f' :=
+  pequiv_of_equiv (seq_colim_equiv g p) (ap (ι _) (respect_pt (g _)))
+
+  definition pseq_colim_pequiv [constructor] {A A' : ℕ → Type*} {f : Πn, A n →* A (n+1)}
+    {f' : Πn, A' n →* A' (n+1)} (g : Πn, A n ≃* A' n)
+    (p : Πn, g (n+1) ∘* f n ~* f' n ∘* g n) : pseq_colim @f ≃* pseq_colim @f' :=
+  pseq_colim_pequiv' g (λn, @p n)
 
   definition seq_colim_equiv_constant [constructor] {A : ℕ → Type*} {f f' : Π⦃n⦄, A n → A (n+1)}
     (p : Π⦃n⦄ (a : A n), f a = f' a) : seq_colim f ≃ seq_colim f' :=
   seq_colim_equiv (λn, erfl) p
 
-  definition pseq_colim_equiv_constant [constructor] {A : ℕ → Type*} {f f' : Π{n}, A n →* A (n+1)}
-    (p : Π⦃n⦄, f ~ f') : pseq_colim @f ≃* pseq_colim @f' :=
-  pseq_colim_pequiv (λn, pequiv.rfl) p
+  definition pseq_colim_equiv_constant' [constructor] {A : ℕ → Type*} {f f' : Πn, A n →* A (n+1)}
+    (p : Π⦃n⦄, f n ~ f' n) : pseq_colim @f ≃* pseq_colim @f' :=
+  pseq_colim_pequiv' (λn, pequiv.rfl) p
 
-  definition pseq_colim_pequiv_pinclusion {A A' : ℕ → Type*} {f : Π(n), A n →* A (n+1)}
-    {f' : Π(n), A' n →* A' (n+1)} (g : Π(n), A n ≃* A' n)
+  definition pseq_colim_equiv_constant [constructor] {A : ℕ → Type*} {f f' : Πn, A n →* A (n+1)}
+    (p : Πn, f n ~* f' n) : pseq_colim @f ≃* pseq_colim @f' :=
+  pseq_colim_pequiv (λn, pequiv.rfl) (λn, !pid_pcompose ⬝* p n ⬝* !pcompose_pid⁻¹*)
+
+  definition pseq_colim_pequiv_pinclusion {A A' : ℕ → Type*} {f : Πn, A n →* A (n+1)}
+    {f' : Πn, A' n →* A' (n+1)} (g : Πn, A n ≃* A' n)
     (p : Π⦃n⦄, g (n+1) ∘* f n ~* f' n ∘* g n) (n : ℕ) :
     psquare (pinclusion f n) (pinclusion f' n) (g n) (pseq_colim_pequiv g p) :=
-  phomotopy.mk homotopy.rfl begin 
-    esimp, refine !idp_con ⬝ _, 
+  phomotopy.mk homotopy.rfl begin
+    esimp, refine !idp_con ⬝ _,
     induction n with n IH,
     { esimp[inclusion_pt], exact !idp_con⁻¹ },
     { esimp[inclusion_pt], rewrite [+ap_con, -+ap_inv, +con.assoc, +seq_colim_functor_glue],
@@ -360,8 +368,8 @@ namespace seq_colim
     }
   end
 
-  definition seq_colim_equiv_constant_pinclusion {A : ℕ → Type*} {f f' : Π⦃n⦄, A n →* A (n+1)}
-    (p : Π⦃n⦄ (a : A n), f a = f' a) (n : ℕ) :
+  definition seq_colim_equiv_constant_pinclusion {A : ℕ → Type*} {f f' : Πn, A n →* A (n+1)}
+    (p : Πn, f n ~* f' n) (n : ℕ) :
     pseq_colim_equiv_constant p ∘* pinclusion f n ~* pinclusion f' n  :=
   begin
     sorry
diff --git a/homotopy/spectrum.hlean b/homotopy/spectrum.hlean
index 33dc6aa..7c6b211 100644
--- a/homotopy/spectrum.hlean
+++ b/homotopy/spectrum.hlean
@@ -381,6 +381,10 @@ namespace spectrum
     spectrify_type_term X n k →* spectrify_type_term X n (k+1) :=
   spectrify_type_fun' X k (n +' k)
 
+  definition spectrify_type_fun_zero {N : succ_str} (X : gen_prespectrum N) (n : N) :
+    spectrify_type_fun X n 0 ~* glue X n :=
+  !pid_pcompose
+
   definition spectrify_type {N : succ_str} (X : gen_prespectrum N) (n : N) : Type* :=
   pseq_colim (spectrify_type_fun X n)
 
@@ -400,11 +404,11 @@ namespace spectrum
     transitivity pseq_colim (λk, spectrify_type_fun' X (succ k) (S n +' k)),
     fapply pseq_colim_pequiv,
     { intro n, apply loopn_pequiv_loopn, apply pequiv_ap X, apply succ_str.add_succ },
-    { intro k, apply to_homotopy,
+    { exact abstract begin intro k, apply to_homotopy,
       refine !passoc⁻¹* ⬝* _, refine pwhisker_right _ (loopn_succ_in_inv_natural (succ k) _) ⬝* _,
       refine !passoc ⬝* _ ⬝* !passoc⁻¹*, apply pwhisker_left,
       refine !apn_pcompose⁻¹* ⬝* _ ⬝* !apn_pcompose, apply apn_phomotopy,
-      exact !glue_ptransport⁻¹* },
+      exact !glue_ptransport⁻¹* end end },
     refine _ ⬝e* !pseq_colim_loop⁻¹ᵉ*,
     refine pseq_colim_equiv_constant (λn, !ap1_pcompose⁻¹*),
   end
@@ -429,10 +433,9 @@ namespace spectrum
     { intro n, apply phomotopy_of_psquare, refine !pid_pcompose⁻¹* ⬝ph* _,
       refine !pid_pcompose⁻¹* ⬝ph* _,
       --pshift_equiv_pinclusion (spectrify_type_fun X n) 0
-      refine _ ⬝v* _,
-      rotate 1, exact pshift_equiv_pinclusion (spectrify_type_fun X n) 0,
---      refine !passoc⁻¹* ⬝* pwhisker_left _ _ ⬝* _,
-      exact sorry
+      refine !passoc ⬝* pwhisker_left _ (pshift_equiv_pinclusion (spectrify_type_fun X n) 0) ⬝* _,
+      --refine !passoc ⬝* pwhisker_left _ _ ⬝* _,
+      --rotate 1, exact phomotopy_of_psquare !pseq_colim_pequiv_pinclusion
 }
   end
 

From 9f1df6becb2682f718592e67a85b4ab96233c9d6 Mon Sep 17 00:00:00 2001
From: spiceghello <stefano.piceghello@uib.no>
Date: Thu, 8 Jun 2017 09:27:57 -0600
Subject: [PATCH 07/24] lemma in colim for spectrification

---
 colim.hlean | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

diff --git a/colim.hlean b/colim.hlean
index 8053718..bdb571e 100644
--- a/colim.hlean
+++ b/colim.hlean
@@ -372,7 +372,9 @@ namespace seq_colim
     (p : Πn, f n ~* f' n) (n : ℕ) :
     pseq_colim_equiv_constant p ∘* pinclusion f n ~* pinclusion f' n  :=
   begin
-    sorry
+    transitivity pinclusion f' n ∘* !pid,
+    refine phomotopy_of_psquare !pseq_colim_pequiv_pinclusion,
+    exact !pcompose_pid
   end
 
   definition is_equiv_seq_colim_rec (P : seq_colim f → Type) :

From 1fee1395edc108d1aaa4d7b14dc4dc465b786db6 Mon Sep 17 00:00:00 2001
From: favonia <favonia@gmail.com>
Date: Wed, 7 Jun 2017 12:30:08 -0600
Subject: [PATCH 08/24] Add Group_sum_elim.

---
 algebra/product_group.hlean | 7 +++++++
 1 file changed, 7 insertions(+)

diff --git a/algebra/product_group.hlean b/algebra/product_group.hlean
index c1e090c..fb36523 100644
--- a/algebra/product_group.hlean
+++ b/algebra/product_group.hlean
@@ -67,6 +67,13 @@ namespace group
   definition product_inr (G H : Group) : H →g G ×g H :=
     homomorphism.mk (λx, (one, x)) (λx y, prod_eq !one_mul⁻¹ !refl)
 
+  definition Group_sum_elim (G H : Group) (I : AbGroup) (φ : G →g I) (ψ : H →g I) : G ×g H →g I :=
+    homomorphism.mk (λx, φ x.1 * ψ x.2) (λx y, calc
+      φ (x.1 * y.1) * ψ (x.2 * y.2) = (φ x.1 * φ y.1) * (ψ x.2 * ψ y.2)
+                                      : by exact ap011 mul (to_respect_mul φ x.1 y.1) (to_respect_mul ψ x.2 y.2)
+                                ... = (φ x.1 * ψ x.2) * (φ y.1 * ψ y.2)
+                                      : by exact interchange I (φ x.1) (φ y.1) (ψ x.2) (ψ y.2))
+
   definition product_functor [constructor] {G G' H H' : Group} (φ : G →g H) (ψ : G' →g H') :
     G ×g G' →g H ×g H' :=
   homomorphism.mk (λx, (φ x.1, ψ x.2)) (λx y, prod_eq !to_respect_mul !to_respect_mul)

From 8e3c2d020f9b626cb3296a07bc3f75be4260b920 Mon Sep 17 00:00:00 2001
From: favonia <favonia@gmail.com>
Date: Thu, 8 Jun 2017 09:28:52 -0600
Subject: [PATCH 09/24] Add binary_dirsum.

---
 algebra/direct_sum.hlean | 33 +++++++++++++++++++++++++++++++--
 1 file changed, 31 insertions(+), 2 deletions(-)

diff --git a/algebra/direct_sum.hlean b/algebra/direct_sum.hlean
index 0d1f6c1..97ad3fa 100644
--- a/algebra/direct_sum.hlean
+++ b/algebra/direct_sum.hlean
@@ -6,9 +6,9 @@ Authors: Floris van Doorn, Egbert Rijke
 Constructions with groups
 -/
 
-import .quotient_group .free_commutative_group
+import .quotient_group .free_commutative_group .product_group
 
-open eq algebra is_trunc set_quotient relation sigma prod sum list trunc function equiv sigma.ops
+open eq is_equiv algebra is_trunc set_quotient relation sigma prod sum list trunc function equiv sigma.ops
 
 namespace group
 
@@ -89,6 +89,35 @@ namespace group
 
   end
 
+  definition binary_dirsum (G H : AbGroup) : dirsum (bool.rec G H) ≃g G ×ag H :=
+  let branch := bool.rec G H in
+  let to_hom := (dirsum_elim (bool.rec (product_inl G H) (product_inr G H))
+                : dirsum (bool.rec G H) →g G ×ag H) in
+  let from_hom := (Group_sum_elim G H (dirsum (bool.rec G H))
+                    (dirsum_incl branch bool.ff) (dirsum_incl branch bool.tt)
+                  : G ×g H →g dirsum branch) in
+  begin
+    fapply isomorphism.mk,
+    { exact dirsum_elim (bool.rec (product_inl G H) (product_inr G H)) },
+    fapply adjointify,
+    { exact from_hom },
+    { intro gh, induction gh with g h,
+        exact prod_eq (mul_one (1 * g) ⬝ one_mul g) (ap (λ o, o * h) (mul_one 1) ⬝ one_mul h) },
+    { refine dirsum.rec _ _ _,
+      { intro b x,
+        refine ap from_hom (dirsum_elim_compute (bool.rec (product_inl G H) (product_inr G H)) b x) ⬝ _,
+        induction b,
+        { exact ap (λ y, dirsum_incl branch bool.ff x * y) (to_respect_one (dirsum_incl branch bool.tt)) ⬝ mul_one _ },
+        { exact ap (λ y, y * dirsum_incl branch bool.tt x) (to_respect_one (dirsum_incl branch bool.ff)) ⬝ one_mul _ }
+      },
+      { refine ap from_hom (to_respect_one to_hom) ⬝ to_respect_one from_hom },
+      { intro g h gβ hβ,
+        refine ap from_hom (to_respect_mul to_hom _ _) ⬝ to_respect_mul from_hom _ _ ⬝ _,
+        exact ap011 mul gβ hβ
+      }
+    }
+  end
+
   variables {I J : Set} {Y Y' Y'' : I → AbGroup}
 
   definition dirsum_functor [constructor] (f : Πi, Y i →g Y' i) : dirsum Y →g dirsum Y' :=

From 4ca9907929a2fa146b7875640e9edc67fe9672dd Mon Sep 17 00:00:00 2001
From: Floris van Doorn <fpv@andrew.cmu.edu>
Date: Thu, 8 Jun 2017 11:33:08 -0400
Subject: [PATCH 10/24] fix spectrum file

---
 homotopy/spectrum.hlean | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

diff --git a/homotopy/spectrum.hlean b/homotopy/spectrum.hlean
index 7c6b211..bb92e64 100644
--- a/homotopy/spectrum.hlean
+++ b/homotopy/spectrum.hlean
@@ -402,7 +402,7 @@ namespace spectrum
   begin
     refine !pshift_equiv ⬝e* _,
     transitivity pseq_colim (λk, spectrify_type_fun' X (succ k) (S n +' k)),
-    fapply pseq_colim_pequiv,
+    fapply pseq_colim_pequiv',
     { intro n, apply loopn_pequiv_loopn, apply pequiv_ap X, apply succ_str.add_succ },
     { exact abstract begin intro k, apply to_homotopy,
       refine !passoc⁻¹* ⬝* _, refine pwhisker_right _ (loopn_succ_in_inv_natural (succ k) _) ⬝* _,
@@ -410,7 +410,7 @@ namespace spectrum
       refine !apn_pcompose⁻¹* ⬝* _ ⬝* !apn_pcompose, apply apn_phomotopy,
       exact !glue_ptransport⁻¹* end end },
     refine _ ⬝e* !pseq_colim_loop⁻¹ᵉ*,
-    refine pseq_colim_equiv_constant (λn, !ap1_pcompose⁻¹*),
+    exact pseq_colim_equiv_constant (λn, begin unfold [spectrify_type_fun], refine sorry ⬝* !ap1_pcompose⁻¹* end),
   end
 
   definition spectrify [constructor] {N : succ_str} (X : gen_prespectrum N) : gen_spectrum N :=
@@ -436,6 +436,7 @@ namespace spectrum
       refine !passoc ⬝* pwhisker_left _ (pshift_equiv_pinclusion (spectrify_type_fun X n) 0) ⬝* _,
       --refine !passoc ⬝* pwhisker_left _ _ ⬝* _,
       --rotate 1, exact phomotopy_of_psquare !pseq_colim_pequiv_pinclusion
+      exact sorry
 }
   end
 

From 664d971d4b765525d9f9ec35ec92de082501721c Mon Sep 17 00:00:00 2001
From: Floris van Doorn <fpv@andrew.cmu.edu>
Date: Thu, 8 Jun 2017 11:41:37 -0400
Subject: [PATCH 11/24] add some constructor attributes to product_group

---
 algebra/direct_sum.hlean    |  2 +-
 algebra/product_group.hlean | 10 +++++-----
 2 files changed, 6 insertions(+), 6 deletions(-)

diff --git a/algebra/direct_sum.hlean b/algebra/direct_sum.hlean
index 97ad3fa..e4fdeef 100644
--- a/algebra/direct_sum.hlean
+++ b/algebra/direct_sum.hlean
@@ -93,7 +93,7 @@ namespace group
   let branch := bool.rec G H in
   let to_hom := (dirsum_elim (bool.rec (product_inl G H) (product_inr G H))
                 : dirsum (bool.rec G H) →g G ×ag H) in
-  let from_hom := (Group_sum_elim G H (dirsum (bool.rec G H))
+  let from_hom := (Group_sum_elim (dirsum (bool.rec G H))
                     (dirsum_incl branch bool.ff) (dirsum_incl branch bool.tt)
                   : G ×g H →g dirsum branch) in
   begin
diff --git a/algebra/product_group.hlean b/algebra/product_group.hlean
index fb36523..2bd56d1 100644
--- a/algebra/product_group.hlean
+++ b/algebra/product_group.hlean
@@ -61,18 +61,18 @@ namespace group
   infix ` ×g `:60 := group.product
   infix ` ×ag `:60 := group.ab_product
 
-  definition product_inl (G H : Group) : G →g G ×g H :=
+  definition product_inl [constructor] (G H : Group) : G →g G ×g H :=
     homomorphism.mk (λx, (x, one)) (λx y, prod_eq !refl !one_mul⁻¹)
 
-  definition product_inr (G H : Group) : H →g G ×g H :=
+  definition product_inr [constructor] (G H : Group) : H →g G ×g H :=
     homomorphism.mk (λx, (one, x)) (λx y, prod_eq !one_mul⁻¹ !refl)
 
-  definition Group_sum_elim (G H : Group) (I : AbGroup) (φ : G →g I) (ψ : H →g I) : G ×g H →g I :=
-    homomorphism.mk (λx, φ x.1 * ψ x.2) (λx y, calc
+  definition Group_sum_elim [constructor] {G H : Group} (I : AbGroup) (φ : G →g I) (ψ : H →g I) : G ×g H →g I :=
+    homomorphism.mk (λx, φ x.1 * ψ x.2) abstract (λx y, calc
       φ (x.1 * y.1) * ψ (x.2 * y.2) = (φ x.1 * φ y.1) * (ψ x.2 * ψ y.2)
                                       : by exact ap011 mul (to_respect_mul φ x.1 y.1) (to_respect_mul ψ x.2 y.2)
                                 ... = (φ x.1 * ψ x.2) * (φ y.1 * ψ y.2)
-                                      : by exact interchange I (φ x.1) (φ y.1) (ψ x.2) (ψ y.2))
+                                      : by exact interchange I (φ x.1) (φ y.1) (ψ x.2) (ψ y.2)) end
 
   definition product_functor [constructor] {G G' H H' : Group} (φ : G →g H) (ψ : G' →g H') :
     G ×g G' →g H ×g H' :=

From 5b384882f83f8c3fbb9fd3f5195aabf3b43b7225 Mon Sep 17 00:00:00 2001
From: Floris van Doorn <fpv@andrew.cmu.edu>
Date: Thu, 8 Jun 2017 11:51:49 -0400
Subject: [PATCH 12/24] rename ordinary_theory to ordinary_cohomology_theory

---
 homotopy/cohomology.hlean | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/homotopy/cohomology.hlean b/homotopy/cohomology.hlean
index 38a7e4c..0317070 100644
--- a/homotopy/cohomology.hlean
+++ b/homotopy/cohomology.hlean
@@ -189,7 +189,7 @@ structure cohomology_theory.{u} : Type.{u+1} :=
   (Hadditive : Π(n : ℤ) {I : Type.{u}} (X : I → Type*), has_choice 0 I →
     is_equiv (Group_pi_intro (λi, Hh n (pinl i)) : HH n (⋁ X) → Πᵍ i, HH n (X i)))
 
-structure ordinary_theory.{u} extends cohomology_theory.{u} : Type.{u+1} :=
+structure ordinary_cohomology_theory.{u} extends cohomology_theory.{u} : Type.{u+1} :=
  (Hdimension : Π(n : ℤ), n ≠ 0 → is_contr (HH n (plift pbool)))
 
 attribute cohomology_theory.HH [coercion]
@@ -270,7 +270,7 @@ cohomology_theory.mk
 -- print has_choice_lift
 -- print equiv_lift
 -- print has_choice_equiv_closed
-definition ordinary_theory_EM [constructor] (G : AbGroup) : ordinary_theory :=
+definition ordinary_cohomology_theory_EM [constructor] (G : AbGroup) : ordinary_theory :=
 ⦃ordinary_theory, cohomology_theory_spectrum (EM_spectrum G), Hdimension := EM_dimension G ⦄
 
 end cohomology

From a8592e01843cee2bf8c24cfafd43bdd0b5cd694c Mon Sep 17 00:00:00 2001
From: favonia <favonia@gmail.com>
Date: Thu, 8 Jun 2017 09:54:47 -0600
Subject: [PATCH 13/24] Add homology_ordinary_theory and copyright statement.

---
 homology/homology.hlean | 11 +++++++++++
 1 file changed, 11 insertions(+)

diff --git a/homology/homology.hlean b/homology/homology.hlean
index 32e79f8..6ddef42 100644
--- a/homology/homology.hlean
+++ b/homology/homology.hlean
@@ -1,3 +1,11 @@
+/-
+Copyright (c) 2017 Yuri Sulyma, Favonia
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Yuri Sulyma, Favonia
+
+Reduced homology theories
+-/
+
 import ..homotopy.spectrum ..homotopy.EM ..algebra.arrow_group ..algebra.direct_sum ..homotopy.fwedge ..choice ..homotopy.pushout ..move_to_lib
 
 open eq spectrum int pointed group algebra sphere nat equiv susp is_trunc
@@ -20,6 +28,9 @@ namespace homology
     (Hadditive : Π(n : ℤ) {I : Set.{u}} (X : I → Type*), is_equiv
       (dirsum_elim (λi, Hh n (pinl i)) : dirsum (λi, HH n (X i)) → HH n (⋁ X)))
 
+  structure ordinary_homology_theory.{u} extends homology_theory.{u} : Type.{u+1} :=
+    (Hdimension : Π(n : ℤ), n ≠ 0 → is_contr (HH n (plift (psphere 0))))
+
   section
     parameter (theory : homology_theory)
     open homology_theory

From 5cda45ae1d2dc7f52aeeb3184adeb760539dcff2 Mon Sep 17 00:00:00 2001
From: favonia <favonia@gmail.com>
Date: Thu, 8 Jun 2017 10:14:07 -0600
Subject: [PATCH 14/24] Add the missing 'p'.

---
 homology/homology.hlean | 36 ++++++++++++++++++------------------
 homology/sphere.hlean   |  5 ++---
 2 files changed, 20 insertions(+), 21 deletions(-)

diff --git a/homology/homology.hlean b/homology/homology.hlean
index 6ddef42..cd15f1d 100644
--- a/homology/homology.hlean
+++ b/homology/homology.hlean
@@ -18,12 +18,12 @@ namespace homology
   structure homology_theory.{u} : Type.{u+1} :=
     (HH : ℤ → pType.{u} → AbGroup.{u})
     (Hh : Π(n : ℤ) {X Y : Type*} (f : X →* Y), HH n X →g HH n Y)
-    (Hid : Π(n : ℤ) {X : Type*} (x : HH n X), Hh n (pid X) x = x)
-    (Hcompose : Π(n : ℤ) {X Y Z : Type*} (f : Y →* Z) (g : X →* Y),
+    (Hpid : Π(n : ℤ) {X : Type*} (x : HH n X), Hh n (pid X) x = x)
+    (Hpcompose : Π(n : ℤ) {X Y Z : Type*} (f : Y →* Z) (g : X →* Y),
       Hh n (f ∘* g) ~ Hh n f ∘ Hh n g)
-    (Hsusp : Π(n : ℤ) (X : Type*), HH (succ n) (psusp X) ≃g HH n X)
-    (Hsusp_natural : Π(n : ℤ) {X Y : Type*} (f : X →* Y),
-      Hsusp n Y ∘ Hh (succ n) (psusp_functor f) ~ Hh n f ∘ Hsusp n X)
+    (Hpsusp : Π(n : ℤ) (X : Type*), HH (succ n) (psusp X) ≃g HH n X)
+    (Hpsusp_natural : Π(n : ℤ) {X Y : Type*} (f : X →* Y),
+      Hpsusp n Y ∘ Hh (succ n) (psusp_functor f) ~ Hh n f ∘ Hpsusp n X)
     (Hexact : Π(n : ℤ) {X Y : Type*} (f : X →* Y), is_exact_g (Hh n f) (Hh n (pcod f)))
     (Hadditive : Π(n : ℤ) {I : Set.{u}} (X : I → Type*), is_equiv
       (dirsum_elim (λi, Hh n (pinl i)) : dirsum (λi, HH n (X i)) → HH n (⋁ X)))
@@ -37,20 +37,20 @@ namespace homology
 
     theorem HH_base_indep (n : ℤ) {A : Type} (a b : A)
       : HH theory n (pType.mk A a) ≃g HH theory n (pType.mk A b) :=
-      calc HH theory n (pType.mk A a) ≃g HH theory (int.succ n) (psusp A) : by exact (Hsusp theory n (pType.mk A a)) ⁻¹ᵍ
-                                  ... ≃g HH theory n (pType.mk A b)       : by exact Hsusp theory n (pType.mk A b)
+      calc HH theory n (pType.mk A a) ≃g HH theory (int.succ n) (psusp A) : by exact (Hpsusp theory n (pType.mk A a)) ⁻¹ᵍ
+                                  ... ≃g HH theory n (pType.mk A b)       : by exact Hpsusp theory n (pType.mk A b)
 
     theorem Hh_homotopy' (n : ℤ) {A B : Type*} (f : A → B) (p q : f pt = pt)
       : Hh theory n (pmap.mk f p) ~ Hh theory n (pmap.mk f q) := λ x,
     calc       Hh theory n (pmap.mk f p) x
-             = Hh theory n (pmap.mk f p) (Hsusp theory n A ((Hsusp theory n A)⁻¹ᵍ x))
-               : by exact ap (Hh theory n (pmap.mk f p)) (equiv.to_right_inv (equiv_of_isomorphism (Hsusp theory n A)) x)⁻¹
-         ... = Hsusp theory n B (Hh theory (succ n) (pmap.mk (susp.functor f) !refl) ((Hsusp theory n A)⁻¹ x))
-               : by exact (Hsusp_natural theory n (pmap.mk f p) ((Hsusp theory n A)⁻¹ᵍ x))⁻¹
-         ... = Hh theory n (pmap.mk f q) (Hsusp theory n A ((Hsusp theory n A)⁻¹ x))
-               : by exact Hsusp_natural theory n (pmap.mk f q) ((Hsusp theory n A)⁻¹ x)
+             = Hh theory n (pmap.mk f p) (Hpsusp theory n A ((Hpsusp theory n A)⁻¹ᵍ x))
+               : by exact ap (Hh theory n (pmap.mk f p)) (equiv.to_right_inv (equiv_of_isomorphism (Hpsusp theory n A)) x)⁻¹
+         ... = Hpsusp theory n B (Hh theory (succ n) (pmap.mk (susp.functor f) !refl) ((Hpsusp theory n A)⁻¹ x))
+               : by exact (Hpsusp_natural theory n (pmap.mk f p) ((Hpsusp theory n A)⁻¹ᵍ x))⁻¹
+         ... = Hh theory n (pmap.mk f q) (Hpsusp theory n A ((Hpsusp theory n A)⁻¹ x))
+               : by exact Hpsusp_natural theory n (pmap.mk f q) ((Hpsusp theory n A)⁻¹ x)
          ... = Hh theory n (pmap.mk f q) x
-               : by exact ap (Hh theory n (pmap.mk f q)) (equiv.to_right_inv (equiv_of_isomorphism (Hsusp theory n A)) x)
+               : by exact ap (Hh theory n (pmap.mk f q)) (equiv.to_right_inv (equiv_of_isomorphism (Hpsusp theory n A)) x)
 
     theorem Hh_homotopy (n : ℤ) {A B : Type*} (f g : A →* B) (h : f ~ g) : Hh theory n f ~ Hh theory n g := λ x,
     calc       Hh theory n f x
@@ -67,15 +67,15 @@ namespace homology
       { exact Hh theory n e⁻¹ᵉ* },
       { intro x, exact calc
               Hh theory n e (Hh theory n e⁻¹ᵉ* x)
-            = Hh theory n (e ∘* e⁻¹ᵉ*) x : by exact (Hcompose theory n e e⁻¹ᵉ* x)⁻¹
+            = Hh theory n (e ∘* e⁻¹ᵉ*) x : by exact (Hpcompose theory n e e⁻¹ᵉ* x)⁻¹
         ... = Hh theory n !pid x : by exact Hh_homotopy n (e ∘* e⁻¹ᵉ*) !pid (to_right_inv e) x
-        ... = x : by exact Hid theory n x
+        ... = x : by exact Hpid theory n x
       },
       { intro x, exact calc
               Hh theory n e⁻¹ᵉ* (Hh theory n e x)
-            = Hh theory n (e⁻¹ᵉ* ∘* e) x : by exact (Hcompose theory n e⁻¹ᵉ* e x)⁻¹
+            = Hh theory n (e⁻¹ᵉ* ∘* e) x : by exact (Hpcompose theory n e⁻¹ᵉ* e x)⁻¹
         ... = Hh theory n !pid x : by exact Hh_homotopy n (e⁻¹ᵉ* ∘* e) !pid (to_left_inv e) x
-        ... = x : by exact Hid theory n x
+        ... = x : by exact Hpid theory n x
       }
     end
 
diff --git a/homology/sphere.hlean b/homology/sphere.hlean
index 6d9ed54..d6f789f 100644
--- a/homology/sphere.hlean
+++ b/homology/sphere.hlean
@@ -5,7 +5,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: Kuen-Bang Hou (Favonia)
 -/
 
-import core
 import .homology
 
 open eq pointed group algebra circle sphere nat equiv susp
@@ -18,7 +17,7 @@ section
 
   open homology_theory
 
-  theorem Hsphere : Π(n : ℤ)(m : ℕ), HH theory n (plift (psphere m)) ≃g HH theory (n - m) (plift (psphere 0)) :=
+  theorem Hpsphere : Π(n : ℤ)(m : ℕ), HH theory n (plift (psphere m)) ≃g HH theory (n - m) (plift (psphere 0)) :=
     begin
       intros n m, revert n, induction m with m,
       { exact λ n, isomorphism_ap (λ n, HH theory n (plift (psphere 0))) (sub_zero n)⁻¹ },
@@ -27,7 +26,7 @@ section
                ≃g HH theory n (psusp (plift (psphere m))) : by exact HH_isomorphism theory n (plift_psusp (psphere m))
            ... ≃g HH theory (succ (pred n)) (psusp (plift (psphere m)))
                   : by exact isomorphism_ap (λ n, HH theory n (psusp (plift (psphere m)))) (succ_pred n)⁻¹
-           ... ≃g HH theory (pred n) (plift (psphere m)) : by exact Hsusp theory (pred n) (plift (psphere m))
+           ... ≃g HH theory (pred n) (plift (psphere m)) : by exact Hpsusp theory (pred n) (plift (psphere m))
            ... ≃g HH theory (pred n - m) (plift (psphere 0)) : by exact v_0 (pred n)
            ... ≃g HH theory (n - succ m) (plift (psphere 0))
                   : by exact isomorphism_ap (λ n, HH theory n (plift (psphere 0))) (sub_sub n 1 m ⬝ ap (λ m, n - m) (add.comm 1 m))

From 3ab890c464256e343137abc270928cb3b461555c Mon Sep 17 00:00:00 2001
From: Floris van Doorn <fpv@andrew.cmu.edu>
Date: Thu, 8 Jun 2017 12:12:46 -0400
Subject: [PATCH 15/24] fix rename ordinary_theory ->
 ordinary_cohomology_theory

---
 homotopy/cohomology.hlean | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/homotopy/cohomology.hlean b/homotopy/cohomology.hlean
index 0317070..8c25b70 100644
--- a/homotopy/cohomology.hlean
+++ b/homotopy/cohomology.hlean
@@ -270,7 +270,7 @@ cohomology_theory.mk
 -- print has_choice_lift
 -- print equiv_lift
 -- print has_choice_equiv_closed
-definition ordinary_cohomology_theory_EM [constructor] (G : AbGroup) : ordinary_theory :=
-⦃ordinary_theory, cohomology_theory_spectrum (EM_spectrum G), Hdimension := EM_dimension G ⦄
+definition ordinary_cohomology_theory_EM [constructor] (G : AbGroup) : ordinary_cohomology_theory :=
+⦃ordinary_cohomology_theory, cohomology_theory_spectrum (EM_spectrum G), Hdimension := EM_dimension G ⦄
 
 end cohomology

From abe62d1f614b9d08cffe42ba1b1934cb17fcfc49 Mon Sep 17 00:00:00 2001
From: spiceghello <stefano.piceghello@uib.no>
Date: Thu, 8 Jun 2017 10:26:21 -0600
Subject: [PATCH 16/24] spectrify_pequiv

---
 homotopy/spectrum.hlean | 20 ++++++++++++++------
 1 file changed, 14 insertions(+), 6 deletions(-)

diff --git a/homotopy/spectrum.hlean b/homotopy/spectrum.hlean
index bb92e64..9e1c8ae 100644
--- a/homotopy/spectrum.hlean
+++ b/homotopy/spectrum.hlean
@@ -373,13 +373,13 @@ namespace spectrum
   definition spectrify_type_term {N : succ_str} (X : gen_prespectrum N) (n : N) (k : ℕ) : Type* :=
   Ω[k] (X (n +' k))
 
-  definition spectrify_type_fun' {N : succ_str} (X : gen_prespectrum N) (k : ℕ) (n : N) :
+  definition spectrify_type_fun' {N : succ_str} (X : gen_prespectrum N) (n : N) (k : ℕ) :
     Ω[k] (X n) →* Ω[k+1] (X (S n)) :=
   !loopn_succ_in⁻¹ᵉ* ∘* Ω→[k] (glue X n)
 
   definition spectrify_type_fun {N : succ_str} (X : gen_prespectrum N) (n : N) (k : ℕ) :
     spectrify_type_term X n k →* spectrify_type_term X n (k+1) :=
-  spectrify_type_fun' X k (n +' k)
+  spectrify_type_fun' X (n +' k) k
 
   definition spectrify_type_fun_zero {N : succ_str} (X : gen_prespectrum N) (n : N) :
     spectrify_type_fun X n 0 ~* glue X n :=
@@ -397,20 +397,28 @@ namespace spectrum
           ... ≡ Y n
   -/
 
+  definition spectrify_type_fun'_succ {N : succ_str} (X : gen_prespectrum N) (n : N) (k : ℕ) :
+    spectrify_type_fun' X n (succ k) ~* Ω→ (spectrify_type_fun' X n k) :=
+  begin
+    refine _ ⬝* !ap1_pcompose⁻¹*,
+    apply !pwhisker_right, 
+    refine !to_pinv_pequiv_MK2
+  end
+
   definition spectrify_pequiv {N : succ_str} (X : gen_prespectrum N) (n : N) :
     spectrify_type X n ≃* Ω (spectrify_type X (S n)) :=
   begin
     refine !pshift_equiv ⬝e* _,
-    transitivity pseq_colim (λk, spectrify_type_fun' X (succ k) (S n +' k)),
-    fapply pseq_colim_pequiv',
+    transitivity pseq_colim (λk, spectrify_type_fun' X (S n +' k) (succ k)),
+    fapply pseq_colim_pequiv,
     { intro n, apply loopn_pequiv_loopn, apply pequiv_ap X, apply succ_str.add_succ },
-    { exact abstract begin intro k, apply to_homotopy,
+    { exact abstract begin intro k,
       refine !passoc⁻¹* ⬝* _, refine pwhisker_right _ (loopn_succ_in_inv_natural (succ k) _) ⬝* _,
       refine !passoc ⬝* _ ⬝* !passoc⁻¹*, apply pwhisker_left,
       refine !apn_pcompose⁻¹* ⬝* _ ⬝* !apn_pcompose, apply apn_phomotopy,
       exact !glue_ptransport⁻¹* end end },
     refine _ ⬝e* !pseq_colim_loop⁻¹ᵉ*,
-    exact pseq_colim_equiv_constant (λn, begin unfold [spectrify_type_fun], refine sorry ⬝* !ap1_pcompose⁻¹* end),
+    exact pseq_colim_equiv_constant (λn, !spectrify_type_fun'_succ),
   end
 
   definition spectrify [constructor] {N : succ_str} (X : gen_prespectrum N) : gen_spectrum N :=

From 15cc880b15df811f911f50ab0d58e5237ab7d279 Mon Sep 17 00:00:00 2001
From: spiceghello <stefano.piceghello@uib.no>
Date: Thu, 8 Jun 2017 12:13:01 -0600
Subject: [PATCH 17/24] spectrify_map (last triangle missing)

---
 homotopy/spectrum.hlean | 15 +++++++++------
 1 file changed, 9 insertions(+), 6 deletions(-)

diff --git a/homotopy/spectrum.hlean b/homotopy/spectrum.hlean
index 9e1c8ae..597fa76 100644
--- a/homotopy/spectrum.hlean
+++ b/homotopy/spectrum.hlean
@@ -438,14 +438,17 @@ namespace spectrum
   begin
     fapply smap.mk,
     { intro n, exact pinclusion _ 0 },
-    { intro n, apply phomotopy_of_psquare, refine !pid_pcompose⁻¹* ⬝ph* _,
+    { intro n, apply phomotopy_of_psquare,
       refine !pid_pcompose⁻¹* ⬝ph* _,
-      --pshift_equiv_pinclusion (spectrify_type_fun X n) 0
       refine !passoc ⬝* pwhisker_left _ (pshift_equiv_pinclusion (spectrify_type_fun X n) 0) ⬝* _,
-      --refine !passoc ⬝* pwhisker_left _ _ ⬝* _,
-      --rotate 1, exact phomotopy_of_psquare !pseq_colim_pequiv_pinclusion
-      exact sorry
-}
+      refine !passoc⁻¹* ⬝* _,
+      refine _ ◾* (spectrify_type_fun_zero X n ⬝* !pid_pcompose⁻¹*),
+      refine !passoc ⬝* pwhisker_left _ !pseq_colim_pequiv_pinclusion ⬝* _,
+      refine pwhisker_left _ (pwhisker_left _ (ap1_pid) ⬝* !pcompose_pid) ⬝* _,
+      refine !passoc ⬝* pwhisker_left _ !seq_colim_equiv_constant_pinclusion ⬝* _, 
+      apply pinv_left_phomotopy_of_phomotopy,
+      exact !pseq_colim_loop_pinclusion⁻¹*
+    }
   end
 
   definition spectrify.elim {N : succ_str} {X : gen_prespectrum N} {Y : gen_spectrum N}

From 1b2176539196750b3fb2eca71f3f463e864f9ac2 Mon Sep 17 00:00:00 2001
From: Floris van Doorn <fpv@andrew.cmu.edu>
Date: Thu, 8 Jun 2017 15:41:57 -0400
Subject: [PATCH 18/24] work on spectrify elim

---
 colim.hlean             |  6 +++++-
 homotopy/spectrum.hlean | 15 ++++++++++++---
 2 files changed, 17 insertions(+), 4 deletions(-)

diff --git a/colim.hlean b/colim.hlean
index bdb571e..7619b49 100644
--- a/colim.hlean
+++ b/colim.hlean
@@ -399,7 +399,7 @@ namespace seq_colim
   equiv.mk _ !is_equiv_seq_colim_rec
   end functor
 
-  definition pseq_colim.elim [constructor] {A : ℕ → Type*} {B : Type*} {f : Π{n}, A n →* A (n+1)}
+  definition pseq_colim.elim' [constructor] {A : ℕ → Type*} {B : Type*} {f : Π{n}, A n →* A (n+1)}
     (g : Πn, A n →* B) (p : Πn, g (n+1) ∘* f ~ g n) : pseq_colim @f →* B :=
   begin
     fapply pmap.mk,
@@ -409,6 +409,10 @@ namespace seq_colim
     { esimp, apply respect_pt }
   end
 
+  definition pseq_colim.elim [constructor] {A : ℕ → Type*} {B : Type*} {f : Π{n}, A n →* A (n+1)}
+    (g : Πn, A n →* B) (p : Πn, g (n+1) ∘* f ~* g n) : pseq_colim @f →* B :=
+  pseq_colim.elim' g p
+
   definition prep0 [constructor] {A : ℕ → Type*} (f : pseq_diagram A) (k : ℕ) : A 0 →* A k :=
   pmap.mk (rep0 (λn x, f x) k)
           begin induction k with k p, reflexivity, exact ap (@f k) p ⬝ !respect_pt end
diff --git a/homotopy/spectrum.hlean b/homotopy/spectrum.hlean
index 597fa76..5f39b59 100644
--- a/homotopy/spectrum.hlean
+++ b/homotopy/spectrum.hlean
@@ -431,8 +431,15 @@ namespace spectrum
   -- note: the forward map is (currently) not definitionally equal to gluen. Is that a problem?
   definition equiv_gluen {N : succ_str} (X : gen_spectrum N) (n : N) (k : ℕ)
     : X n ≃* Ω[k] (X (n +' k)) :=
-  by induction k with k f; reflexivity; exact f ⬝e* loopn_pequiv_loopn k (equiv_glue X (n +' k))
-                                                ⬝e* !loopn_succ_in⁻¹ᵉ*
+  by induction k with k f; reflexivity; exact f ⬝e* (loopn_pequiv_loopn k (equiv_glue X (n +' k))
+                                                ⬝e* !loopn_succ_in⁻¹ᵉ*)
+
+  definition equiv_gluen_inv_succ {N : succ_str} (X : gen_spectrum N) (n : N) (k : ℕ) :
+    (equiv_gluen X n (k+1))⁻¹ᵉ* ~*
+    (equiv_gluen X n k)⁻¹ᵉ* ∘* Ω→[k] (equiv_glue X (n +' k))⁻¹ᵉ* ∘* !loopn_succ_in :=
+  begin
+    refine !trans_pinv ⬝* pwhisker_left _ _, refine !trans_pinv ⬝* _, refine !to_pinv_pequiv_MK2 ◾* !pinv_pinv
+  end
 
   definition spectrify_map {N : succ_str} {X : gen_prespectrum N} : X →ₛ spectrify X :=
   begin
@@ -457,7 +464,9 @@ namespace spectrum
     fapply smap.mk,
     { intro n, fapply pseq_colim.elim,
       { intro k, refine !equiv_gluen⁻¹ᵉ* ∘* apn k (f (n +' k)) },
-      { intro k, apply to_homotopy, exact sorry }},
+      { intro k, refine !passoc ⬝* pwhisker_right _ !equiv_gluen_inv_succ ⬝* _,
+        refine !passoc ⬝* _, apply pwhisker_left,
+        refine !passoc ⬝* _, exact sorry }},
     { intro n, exact sorry }
   end
 

From daf34724689d753b2dfa921db869525d7de4cc74 Mon Sep 17 00:00:00 2001
From: Yuri Sulyma <yuri.sulyma@gmail.com>
Date: Thu, 8 Jun 2017 14:02:28 -0600
Subject: [PATCH 19/24] Start proving that the homology theory associated to a
 spectrum satisfies the ES axioms

---
 homology/homology.hlean | 53 +++++++++++++++++++++++++++++++++++++++++
 1 file changed, 53 insertions(+)

diff --git a/homology/homology.hlean b/homology/homology.hlean
index 32e79f8..ed8eeff 100644
--- a/homology/homology.hlean
+++ b/homology/homology.hlean
@@ -70,4 +70,57 @@ namespace homology
 
   end
 
+/- homology theory associated to a spectrum -/
+definition homology (X : Type*) (E : spectrum) (n : ℤ) : AbGroup :=
+shomotopy_group n (smash_spectrum X E)
+
+definition parametrized_homology {X : Type*} (E : X → spectrum) (n : ℤ) : AbGroup :=
+sorry
+
+definition ordinary_homology [reducible] (X : Type*) (G : AbGroup) (n : ℤ) : AbGroup :=
+homology X (EM_spectrum G) n
+
+definition ordinary_homology_Z [reducible] (X : Type*) (n : ℤ) : AbGroup :=
+ordinary_homology X agℤ n
+
+notation `H_` n `[`:0 X:0 `, ` E:0 `]`:0 := homology X E n
+notation `H_` n `[`:0 X:0 `]`:0 := ordinary_homology_Z X n
+notation `pH_` n `[`:0 binders `, ` r:(scoped E, parametrized_homology E n) `]`:0 := r
+
+definition unpointed_homology (X : Type) (E : spectrum) (n : ℤ) : AbGroup :=
+H_ n[X₊, E]
+
+definition homology_functor [constructor] {X Y : Type*} {E F : spectrum} (f : X →* Y) (g : E →ₛ F) (n : ℤ) : homology X E n →g homology Y F n :=
+shomotopy_group_fun n (smash_spectrum_fun f g)
+
+definition homology_theory_spectrum.{u} [constructor] (E : spectrum.{u}) : homology_theory.{u} :=
+begin
+  refine homology_theory.mk _ _ _ _ _ _ _ _,
+  exact (λn X, H_ n[X, E]),
+  exact (λn X Y f, homology_functor f (sid E) n),
+  exact sorry, -- Hid is uninteresting but potentially very hard to prove
+  exact sorry,
+  exact sorry,
+  exact sorry,
+  exact sorry,
+  exact sorry
+  -- sorry
+  -- sorry
+  -- sorry
+  -- sorry
+  -- sorry
+  -- sorry
+--  (λn A, H^n[A, Y])
+--  (λn A B f, cohomology_isomorphism f Y n)
+--  (λn A, cohomology_isomorphism_refl A Y n)
+--  (λn A B f, cohomology_functor f Y n)
+--  (λn A B f g p, cohomology_functor_phomotopy p Y n)
+--  (λn A B f x, cohomology_functor_phomotopy_refl f Y n x)
+--  (λn A x, cohomology_functor_pid A Y n x)
+--  (λn A B C g f x, cohomology_functor_pcompose g f Y n x)
+--  (λn A, cohomology_psusp A Y n)
+--  (λn A B f, cohomology_psusp_natural f Y n)
+--  (λn A B f, cohomology_exact f Y n)
+--  (λn I A H, spectrum_additive H A Y n)
+end
 end homology

From 7f637206a0348cf34d349134b870ee05bc4b494f Mon Sep 17 00:00:00 2001
From: Yuri Sulyma <yuri.sulyma@gmail.com>
Date: Thu, 8 Jun 2017 14:03:10 -0600
Subject: [PATCH 20/24] Add a few spectrification things

---
 homotopy/spectrum.hlean | 14 +++++++++++---
 1 file changed, 11 insertions(+), 3 deletions(-)

diff --git a/homotopy/spectrum.hlean b/homotopy/spectrum.hlean
index be199dd..03e3e39 100644
--- a/homotopy/spectrum.hlean
+++ b/homotopy/spectrum.hlean
@@ -146,7 +146,7 @@ namespace spectrum
     -- I guess this manual eta-expansion is necessary because structures lack definitional eta?
     := phomotopy.mk (glue_square f n) (to_homotopy_pt (glue_square f n))
 
-  definition sid {N : succ_str} (E : gen_spectrum N) : E →ₛ E :=
+  definition sid {N : succ_str} (E : gen_prespectrum N) : E →ₛ E :=
     smap.mk (λn, pid (E n))
     (λn, calc glue E n ∘* pid (E n) ~* glue E n                   : pcompose_pid
                               ...   ~* pid (Ω(E (S n))) ∘* glue E n : pid_pcompose
@@ -446,6 +446,9 @@ namespace spectrum
     { intro n, exact sorry }
   end
 
+  definition spectrify_fun {N : succ_str} {X Y : gen_prespectrum N} (f : X →ₛ Y) : spectrify X →ₛ spectrify Y :=
+  spectrify.elim ((@spectrify_map _ Y) ∘ₛ f)
+
   /- Tensor by spaces -/
 
   /- Smash product of spectra -/
@@ -462,8 +465,7 @@ prespectrum.mk (λ z, X ∧ Y z) begin
 end
 
 definition smash_prespectrum_fun {X X' : Type*} {Y Y' : prespectrum} (f : X →* X') (g : Y →ₛ Y') : smash_prespectrum X Y →ₛ smash_prespectrum X' Y' :=
-begin
-  refine smap.mk (λn, smash_functor f (g n)) _,
+smap.mk (λn, smash_functor f (g n)) begin
   intro n,
   refine susp_to_loop_psquare _ _ _ _ _,
   refine pvconcat (psquare_transpose (phinverse (smash_psusp_natural f (g n)))) _,
@@ -478,6 +480,12 @@ begin
   exact smap.glue_square g n
 end
 
+definition smash_spectrum (X : Type*) (Y : spectrum) : spectrum :=
+spectrify (smash_prespectrum X Y)
+
+definition smash_spectrum_fun {X X' : Type*} {Y Y' : spectrum} (f : X →* X') (g : Y →ₛ Y') : smash_spectrum X Y →ₛ smash_spectrum X' Y' :=
+spectrify_fun (smash_prespectrum_fun f g)
+
   /- Cofibers and stability -/
 
   /- The Eilenberg-MacLane spectrum -/

From a3146d0d2a0c62da296fabee2729db3c8a9c1c6a Mon Sep 17 00:00:00 2001
From: Yuri Sulyma <yuri.sulyma@gmail.com>
Date: Thu, 8 Jun 2017 14:03:29 -0600
Subject: [PATCH 21/24] Fix bug

---
 move_to_lib.hlean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/move_to_lib.hlean b/move_to_lib.hlean
index 556ec6c..340eb82 100644
--- a/move_to_lib.hlean
+++ b/move_to_lib.hlean
@@ -1,6 +1,6 @@
 -- definitions, theorems and attributes which should be moved to files in the HoTT library
 
-import homotopy.sphere2 homotopy.cofiber homotopy.wedge hit.prop_trunc hit.set_quotient eq2 types.pointed2 homotopy.smash_adjoint
+import homotopy.sphere2 homotopy.cofiber homotopy.wedge hit.prop_trunc hit.set_quotient eq2 types.pointed2 .homotopy.smash_adjoint
 
 open eq nat int susp pointed pmap sigma is_equiv equiv fiber algebra trunc trunc_index pi group
      is_trunc function sphere unit sum prod bool

From 3fd6e8e8521dc927350b462f2c32f03c2d6a2833 Mon Sep 17 00:00:00 2001
From: Yuri Sulyma <yuri.sulyma@gmail.com>
Date: Thu, 8 Jun 2017 14:04:58 -0600
Subject: [PATCH 22/24] Merge branch 'master' of github.com:fpvandoorn/Spectral

---
 algebra/direct_sum.hlean     | 39 +++++++++++++++++---
 algebra/product_group.hlean  | 18 +++++++++-
 algebra/quotient_group.hlean | 10 +++---
 algebra/seq_colim.hlean      | 13 +++++--
 colim.hlean                  | 70 ++++++++++++++++++++++++++----------
 homology/homology.hlean      | 47 ++++++++++++++----------
 homology/sphere.hlean        | 12 ++++---
 homotopy/cohomology.hlean    |  6 ++--
 homotopy/spectrum.hlean      | 56 ++++++++++++++++++++---------
 move_to_lib.hlean            |  7 ++++
 10 files changed, 205 insertions(+), 73 deletions(-)

diff --git a/algebra/direct_sum.hlean b/algebra/direct_sum.hlean
index 8596dc3..e4fdeef 100644
--- a/algebra/direct_sum.hlean
+++ b/algebra/direct_sum.hlean
@@ -6,9 +6,9 @@ Authors: Floris van Doorn, Egbert Rijke
 Constructions with groups
 -/
 
-import .quotient_group .free_commutative_group
+import .quotient_group .free_commutative_group .product_group
 
-open eq algebra is_trunc set_quotient relation sigma prod sum list trunc function equiv sigma.ops
+open eq is_equiv algebra is_trunc set_quotient relation sigma prod sum list trunc function equiv sigma.ops
 
 namespace group
 
@@ -73,10 +73,10 @@ namespace group
     definition dirsum_elim [constructor] (f : Πi, Y i →g A') : dirsum →g A' :=
     gqg_elim _ (free_ab_group_elim (λv, f v.1 v.2)) (dirsum_elim_resp_quotient f)
 
-    definition dirsum_elim_compute (f : Πi, Y i →g A') (i : I) :
-      dirsum_elim f ∘g dirsum_incl i ~ f i :=
+    definition dirsum_elim_compute (f : Πi, Y i →g A') (i : I) (y : Y i) :
+      dirsum_elim f (dirsum_incl i y) = f i y :=
     begin
-      intro g, apply one_mul
+      apply one_mul
     end
 
     definition dirsum_elim_unique (f : Πi, Y i →g A') (k : dirsum →g A')
@@ -89,6 +89,35 @@ namespace group
 
   end
 
+  definition binary_dirsum (G H : AbGroup) : dirsum (bool.rec G H) ≃g G ×ag H :=
+  let branch := bool.rec G H in
+  let to_hom := (dirsum_elim (bool.rec (product_inl G H) (product_inr G H))
+                : dirsum (bool.rec G H) →g G ×ag H) in
+  let from_hom := (Group_sum_elim (dirsum (bool.rec G H))
+                    (dirsum_incl branch bool.ff) (dirsum_incl branch bool.tt)
+                  : G ×g H →g dirsum branch) in
+  begin
+    fapply isomorphism.mk,
+    { exact dirsum_elim (bool.rec (product_inl G H) (product_inr G H)) },
+    fapply adjointify,
+    { exact from_hom },
+    { intro gh, induction gh with g h,
+        exact prod_eq (mul_one (1 * g) ⬝ one_mul g) (ap (λ o, o * h) (mul_one 1) ⬝ one_mul h) },
+    { refine dirsum.rec _ _ _,
+      { intro b x,
+        refine ap from_hom (dirsum_elim_compute (bool.rec (product_inl G H) (product_inr G H)) b x) ⬝ _,
+        induction b,
+        { exact ap (λ y, dirsum_incl branch bool.ff x * y) (to_respect_one (dirsum_incl branch bool.tt)) ⬝ mul_one _ },
+        { exact ap (λ y, y * dirsum_incl branch bool.tt x) (to_respect_one (dirsum_incl branch bool.ff)) ⬝ one_mul _ }
+      },
+      { refine ap from_hom (to_respect_one to_hom) ⬝ to_respect_one from_hom },
+      { intro g h gβ hβ,
+        refine ap from_hom (to_respect_mul to_hom _ _) ⬝ to_respect_mul from_hom _ _ ⬝ _,
+        exact ap011 mul gβ hβ
+      }
+    }
+  end
+
   variables {I J : Set} {Y Y' Y'' : I → AbGroup}
 
   definition dirsum_functor [constructor] (f : Πi, Y i →g Y' i) : dirsum Y →g dirsum Y' :=
diff --git a/algebra/product_group.hlean b/algebra/product_group.hlean
index 63fa749..2bd56d1 100644
--- a/algebra/product_group.hlean
+++ b/algebra/product_group.hlean
@@ -8,7 +8,7 @@ Constructions with groups
 
 import algebra.group_theory hit.set_quotient types.list types.sum .subgroup .quotient_group
 
-open eq algebra is_trunc set_quotient relation sigma sigma.ops prod prod.ops sum list trunc function
+open eq algebra is_trunc set_quotient relation sigma prod prod.ops sum list trunc function
      equiv
 namespace group
 
@@ -61,6 +61,19 @@ namespace group
   infix ` ×g `:60 := group.product
   infix ` ×ag `:60 := group.ab_product
 
+  definition product_inl [constructor] (G H : Group) : G →g G ×g H :=
+    homomorphism.mk (λx, (x, one)) (λx y, prod_eq !refl !one_mul⁻¹)
+
+  definition product_inr [constructor] (G H : Group) : H →g G ×g H :=
+    homomorphism.mk (λx, (one, x)) (λx y, prod_eq !one_mul⁻¹ !refl)
+
+  definition Group_sum_elim [constructor] {G H : Group} (I : AbGroup) (φ : G →g I) (ψ : H →g I) : G ×g H →g I :=
+    homomorphism.mk (λx, φ x.1 * ψ x.2) abstract (λx y, calc
+      φ (x.1 * y.1) * ψ (x.2 * y.2) = (φ x.1 * φ y.1) * (ψ x.2 * ψ y.2)
+                                      : by exact ap011 mul (to_respect_mul φ x.1 y.1) (to_respect_mul ψ x.2 y.2)
+                                ... = (φ x.1 * ψ x.2) * (φ y.1 * ψ y.2)
+                                      : by exact interchange I (φ x.1) (φ y.1) (ψ x.2) (ψ y.2)) end
+
   definition product_functor [constructor] {G G' H H' : Group} (φ : G →g H) (ψ : G' →g H') :
     G ×g G' →g H ×g H' :=
   homomorphism.mk (λx, (φ x.1, ψ x.2)) (λx y, prod_eq !to_respect_mul !to_respect_mul)
@@ -73,4 +86,7 @@ namespace group
 
   infix ` ×≃g `:60 := group.product_isomorphism
 
+  definition product_group_mul_eq {G H : Group} (g h : G ×g H) : g * h = product_mul g h :=
+  idp
+
 end group
diff --git a/algebra/quotient_group.hlean b/algebra/quotient_group.hlean
index ad81334..b2961ae 100644
--- a/algebra/quotient_group.hlean
+++ b/algebra/quotient_group.hlean
@@ -227,10 +227,10 @@ namespace group
       unfold qg_map, esimp, exact to_respect_mul f g h }
   end
 
-  definition quotient_group_compute (f : G →g G') (H : Π⦃g⦄, N g → f g = 1) :
-    quotient_group_elim f H ∘g qg_map N ~ f :=
+  definition quotient_group_compute (f : G →g G') (H : Π⦃g⦄, N g → f g = 1) (g : G) :
+    quotient_group_elim f H (qg_map N g) = f g :=
   begin
-    intro g, reflexivity
+    reflexivity
   end
 
   definition gelim_unique (f : G →g G') (H : Π⦃g⦄, N g → f g = 1) (k : quotient_group N →g G')
@@ -247,7 +247,7 @@ namespace group
   end
 
   definition qg_universal_property (f : G →g G') (H : Π⦃g⦄, N g → f g = 1)  :
-    is_contr (Σ(g : quotient_group N →g G'), g ∘g qg_map N ~ f) :=
+    is_contr (Σ(g : quotient_group N →g G'), g ∘ qg_map N ~ f) :=
   begin
     fapply is_contr.mk,
       -- give center of contraction
@@ -442,7 +442,7 @@ definition kernel_quotient_extension {A B : AbGroup} (f : A →g B) : quotient_a
   end
 
 definition kernel_quotient_extension_triangle {A B : AbGroup} (f : A →g B) :
-  kernel_quotient_extension f ∘g ab_qg_map (kernel_subgroup f) ~ f :=
+  kernel_quotient_extension f ∘ ab_qg_map (kernel_subgroup f) ~ f :=
   begin
     intro a,
     apply quotient_group_compute
diff --git a/algebra/seq_colim.hlean b/algebra/seq_colim.hlean
index 76b1491..b6824cc 100644
--- a/algebra/seq_colim.hlean
+++ b/algebra/seq_colim.hlean
@@ -18,14 +18,21 @@ namespace group
     definition seq_colim_incl [constructor] (i : ℕ) : A i →g seq_colim :=
       qg_map _ ∘g dirsum_incl A i
 
-    definition seq_colim_quotient (h : Πi, A i →g A') (k : Πi a, h i a = h (i + 1) (f i a))
+    definition seq_colim_quotient (h : Πi, A i →g A') (k : Πi a, h i a = h (succ i) (f i a))
                                   (v : seq_colim_carrier) (r : ∥seq_colim_rel v∥) : dirsum_elim h v = 1 :=
       begin
-        induction r with r, induction r, exact sorry
+        induction r with r, induction r, 
+        refine !to_respect_mul ⬝ _,
+        refine ap (λγ, group_fun (dirsum_elim h) (group_fun (dirsum_incl A i) a) * group_fun (dirsum_elim h) γ) (!to_respect_inv)⁻¹ ⬝ _,
+        refine ap (λγ, γ * group_fun (dirsum_elim h) (group_fun (dirsum_incl A (succ i)) (f i a)⁻¹)) !dirsum_elim_compute ⬝ _,
+        refine ap (λγ, (h i a) * γ) !dirsum_elim_compute ⬝ _,
+        refine ap (λγ, γ * group_fun (h (succ i)) (f i a)⁻¹) !k ⬝ _,
+        refine ap (λγ, group_fun (h (succ i)) (f i a) * γ) (!to_respect_inv) ⬝ _,
+        exact !mul.right_inv
       end
 
     definition seq_colim_elim [constructor] (h : Πi, A i →g A')
-                                            (k : Πi a, h i a = h (i + 1) (f i a)) : seq_colim →g A' :=
+                                            (k : Πi a, h i a = h (succ i) (f i a)) : seq_colim →g A' :=
       gqg_elim _ (dirsum_elim h) (seq_colim_quotient h k)
 
   end
diff --git a/colim.hlean b/colim.hlean
index e772352..7619b49 100644
--- a/colim.hlean
+++ b/colim.hlean
@@ -251,7 +251,7 @@ namespace seq_colim
 
   definition pshift_equiv_pinclusion {A : ℕ → Type*} (f : Πn, A n →* A (succ n)) (n : ℕ) :
     psquare (pinclusion f n) (pinclusion (λn, f (n+1)) n) (f n) (pshift_equiv f)  :=
-  phomotopy.mk homotopy.rfl begin 
+  phomotopy.mk homotopy.rfl begin
     refine !idp_con ⬝ _, esimp,
     induction n with n IH,
     { esimp[inclusion_pt], esimp[shift_diag], exact !idp_con⁻¹ },
@@ -259,7 +259,7 @@ namespace seq_colim
       rewrite ap_con, rewrite ap_con,
       refine _ ⬝ whisker_right _ !con.assoc,
       refine _ ⬝ (con.assoc (_ ⬝ _) _ _)⁻¹,
-      xrewrite [-IH], 
+      xrewrite [-IH],
       esimp[shift_up], rewrite [elim_glue,  ap_inv, -ap_compose'], esimp,
       rewrite [-+con.assoc], apply whisker_right,
       rewrite con.assoc, apply !eq_inv_con_of_con_eq,
@@ -285,7 +285,6 @@ namespace seq_colim
   !elim_glue
 
   omit p
-
   definition is_equiv_seq_colim_functor [constructor] [H : Πn, is_equiv (@g n)]
      : is_equiv (seq_colim_functor @g p) :=
   adjointify _ (seq_colim_functor (λn, (@g _)⁻¹) (λn a, inv_commute' g f f' p a))
@@ -323,29 +322,60 @@ namespace seq_colim
     : Π(x : seq_colim f), P x :=
   by induction v with Pincl Pglue; exact seq_colim.rec f Pincl Pglue
 
-  definition pseq_colim_pequiv [constructor] {A A' : ℕ → Type*} {f : Π{n}, A n →* A (n+1)}
-    {f' : Π{n}, A' n →* A' (n+1)} (g : Π{n}, A n ≃* A' n)
-    (p : Π⦃n⦄, g ∘* f ~ f' ∘* g) : pseq_colim @f ≃* pseq_colim @f' :=
-  pequiv_of_equiv (seq_colim_equiv @g p) (ap (ι _) (respect_pt g))
+  definition pseq_colim_pequiv' [constructor] {A A' : ℕ → Type*} {f : Πn, A n →* A (n+1)}
+    {f' : Πn, A' n →* A' (n+1)} (g : Πn, A n ≃* A' n)
+    (p : Π⦃n⦄, g (n+1) ∘* f n ~ f' n ∘* g n) : pseq_colim @f ≃* pseq_colim @f' :=
+  pequiv_of_equiv (seq_colim_equiv g p) (ap (ι _) (respect_pt (g _)))
+
+  definition pseq_colim_pequiv [constructor] {A A' : ℕ → Type*} {f : Πn, A n →* A (n+1)}
+    {f' : Πn, A' n →* A' (n+1)} (g : Πn, A n ≃* A' n)
+    (p : Πn, g (n+1) ∘* f n ~* f' n ∘* g n) : pseq_colim @f ≃* pseq_colim @f' :=
+  pseq_colim_pequiv' g (λn, @p n)
 
   definition seq_colim_equiv_constant [constructor] {A : ℕ → Type*} {f f' : Π⦃n⦄, A n → A (n+1)}
     (p : Π⦃n⦄ (a : A n), f a = f' a) : seq_colim f ≃ seq_colim f' :=
   seq_colim_equiv (λn, erfl) p
 
-  definition pseq_colim_equiv_constant [constructor] {A : ℕ → Type*} {f f' : Π{n}, A n →* A (n+1)}
-    (p : Π⦃n⦄, f ~ f') : pseq_colim @f ≃* pseq_colim @f' :=
-  pseq_colim_pequiv (λn, pequiv.rfl) p
+  definition pseq_colim_equiv_constant' [constructor] {A : ℕ → Type*} {f f' : Πn, A n →* A (n+1)}
+    (p : Π⦃n⦄, f n ~ f' n) : pseq_colim @f ≃* pseq_colim @f' :=
+  pseq_colim_pequiv' (λn, pequiv.rfl) p
 
-  definition pseq_colim_pequiv_pinclusion {A A' : ℕ → Type*} {f : Π(n), A n →* A (n+1)}
-    {f' : Π(n), A' n →* A' (n+1)} (g : Π(n), A n ≃* A' n)
-    (p : Π⦃n⦄, g (n+1) ∘* f n ~ f' n ∘* g n) (n : ℕ) :
+  definition pseq_colim_equiv_constant [constructor] {A : ℕ → Type*} {f f' : Πn, A n →* A (n+1)}
+    (p : Πn, f n ~* f' n) : pseq_colim @f ≃* pseq_colim @f' :=
+  pseq_colim_pequiv (λn, pequiv.rfl) (λn, !pid_pcompose ⬝* p n ⬝* !pcompose_pid⁻¹*)
+
+  definition pseq_colim_pequiv_pinclusion {A A' : ℕ → Type*} {f : Πn, A n →* A (n+1)}
+    {f' : Πn, A' n →* A' (n+1)} (g : Πn, A n ≃* A' n)
+    (p : Π⦃n⦄, g (n+1) ∘* f n ~* f' n ∘* g n) (n : ℕ) :
     psquare (pinclusion f n) (pinclusion f' n) (g n) (pseq_colim_pequiv g p) :=
-  sorry
+  phomotopy.mk homotopy.rfl begin
+    esimp, refine !idp_con ⬝ _,
+    induction n with n IH,
+    { esimp[inclusion_pt], exact !idp_con⁻¹ },
+    { esimp[inclusion_pt], rewrite [+ap_con, -+ap_inv, +con.assoc, +seq_colim_functor_glue],
+      xrewrite[-IH],
+      rewrite[-+ap_compose', -+con.assoc],
+      apply whisker_right, esimp,
+      rewrite[(eq_con_inv_of_con_eq (!to_homotopy_pt))],
+      rewrite[ap_con], esimp,
+      rewrite[-+con.assoc, ap_con, -ap_compose', +ap_inv],
+      rewrite[-+con.assoc],
+      refine _ ⬝ whisker_right _ (whisker_right _ (whisker_right _ (whisker_right _ !con.left_inv⁻¹))),
+      rewrite[idp_con, +con.assoc], apply whisker_left,
+      rewrite[ap_con, -ap_compose', con_inv, +con.assoc], apply whisker_left,
+      refine eq_inv_con_of_con_eq _,
+      symmetry, exact eq_of_square !natural_square
+    }
+  end
 
-  definition seq_colim_equiv_constant_pinclusion {A : ℕ → Type*} {f f' : Π⦃n⦄, A n →* A (n+1)}
-    (p : Π⦃n⦄ (a : A n), f a = f' a) (n : ℕ) :
+  definition seq_colim_equiv_constant_pinclusion {A : ℕ → Type*} {f f' : Πn, A n →* A (n+1)}
+    (p : Πn, f n ~* f' n) (n : ℕ) :
     pseq_colim_equiv_constant p ∘* pinclusion f n ~* pinclusion f' n  :=
-  sorry
+  begin
+    transitivity pinclusion f' n ∘* !pid,
+    refine phomotopy_of_psquare !pseq_colim_pequiv_pinclusion,
+    exact !pcompose_pid
+  end
 
   definition is_equiv_seq_colim_rec (P : seq_colim f → Type) :
     is_equiv (seq_colim_rec_unc :
@@ -369,7 +399,7 @@ namespace seq_colim
   equiv.mk _ !is_equiv_seq_colim_rec
   end functor
 
-  definition pseq_colim.elim [constructor] {A : ℕ → Type*} {B : Type*} {f : Π{n}, A n →* A (n+1)}
+  definition pseq_colim.elim' [constructor] {A : ℕ → Type*} {B : Type*} {f : Π{n}, A n →* A (n+1)}
     (g : Πn, A n →* B) (p : Πn, g (n+1) ∘* f ~ g n) : pseq_colim @f →* B :=
   begin
     fapply pmap.mk,
@@ -379,6 +409,10 @@ namespace seq_colim
     { esimp, apply respect_pt }
   end
 
+  definition pseq_colim.elim [constructor] {A : ℕ → Type*} {B : Type*} {f : Π{n}, A n →* A (n+1)}
+    (g : Πn, A n →* B) (p : Πn, g (n+1) ∘* f ~* g n) : pseq_colim @f →* B :=
+  pseq_colim.elim' g p
+
   definition prep0 [constructor] {A : ℕ → Type*} (f : pseq_diagram A) (k : ℕ) : A 0 →* A k :=
   pmap.mk (rep0 (λn x, f x) k)
           begin induction k with k p, reflexivity, exact ap (@f k) p ⬝ !respect_pt end
diff --git a/homology/homology.hlean b/homology/homology.hlean
index ed8eeff..6fe727b 100644
--- a/homology/homology.hlean
+++ b/homology/homology.hlean
@@ -1,3 +1,11 @@
+/-
+Copyright (c) 2017 Yuri Sulyma, Favonia
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Yuri Sulyma, Favonia
+
+Reduced homology theories
+-/
+
 import ..homotopy.spectrum ..homotopy.EM ..algebra.arrow_group ..algebra.direct_sum ..homotopy.fwedge ..choice ..homotopy.pushout ..move_to_lib
 
 open eq spectrum int pointed group algebra sphere nat equiv susp is_trunc
@@ -10,36 +18,39 @@ namespace homology
   structure homology_theory.{u} : Type.{u+1} :=
     (HH : ℤ → pType.{u} → AbGroup.{u})
     (Hh : Π(n : ℤ) {X Y : Type*} (f : X →* Y), HH n X →g HH n Y)
-    (Hid : Π(n : ℤ) {X : Type*} (x : HH n X), Hh n (pid X) x = x)
-    (Hcompose : Π(n : ℤ) {X Y Z : Type*} (f : Y →* Z) (g : X →* Y),
+    (Hpid : Π(n : ℤ) {X : Type*} (x : HH n X), Hh n (pid X) x = x)
+    (Hpcompose : Π(n : ℤ) {X Y Z : Type*} (f : Y →* Z) (g : X →* Y),
       Hh n (f ∘* g) ~ Hh n f ∘ Hh n g)
-    (Hsusp : Π(n : ℤ) (X : Type*), HH (succ n) (psusp X) ≃g HH n X)
-    (Hsusp_natural : Π(n : ℤ) {X Y : Type*} (f : X →* Y),
-      Hsusp n Y ∘ Hh (succ n) (psusp_functor f) ~ Hh n f ∘ Hsusp n X)
+    (Hpsusp : Π(n : ℤ) (X : Type*), HH (succ n) (psusp X) ≃g HH n X)
+    (Hpsusp_natural : Π(n : ℤ) {X Y : Type*} (f : X →* Y),
+      Hpsusp n Y ∘ Hh (succ n) (psusp_functor f) ~ Hh n f ∘ Hpsusp n X)
     (Hexact : Π(n : ℤ) {X Y : Type*} (f : X →* Y), is_exact_g (Hh n f) (Hh n (pcod f)))
     (Hadditive : Π(n : ℤ) {I : Set.{u}} (X : I → Type*), is_equiv
       (dirsum_elim (λi, Hh n (pinl i)) : dirsum (λi, HH n (X i)) → HH n (⋁ X)))
 
+  structure ordinary_homology_theory.{u} extends homology_theory.{u} : Type.{u+1} :=
+    (Hdimension : Π(n : ℤ), n ≠ 0 → is_contr (HH n (plift (psphere 0))))
+
   section
     parameter (theory : homology_theory)
     open homology_theory
 
     theorem HH_base_indep (n : ℤ) {A : Type} (a b : A)
       : HH theory n (pType.mk A a) ≃g HH theory n (pType.mk A b) :=
-      calc HH theory n (pType.mk A a) ≃g HH theory (int.succ n) (psusp A) : by exact (Hsusp theory n (pType.mk A a)) ⁻¹ᵍ
-                                  ... ≃g HH theory n (pType.mk A b)       : by exact Hsusp theory n (pType.mk A b)
+      calc HH theory n (pType.mk A a) ≃g HH theory (int.succ n) (psusp A) : by exact (Hpsusp theory n (pType.mk A a)) ⁻¹ᵍ
+                                  ... ≃g HH theory n (pType.mk A b)       : by exact Hpsusp theory n (pType.mk A b)
 
     theorem Hh_homotopy' (n : ℤ) {A B : Type*} (f : A → B) (p q : f pt = pt)
       : Hh theory n (pmap.mk f p) ~ Hh theory n (pmap.mk f q) := λ x,
     calc       Hh theory n (pmap.mk f p) x
-             = Hh theory n (pmap.mk f p) (Hsusp theory n A ((Hsusp theory n A)⁻¹ᵍ x))
-               : by exact ap (Hh theory n (pmap.mk f p)) (equiv.to_right_inv (equiv_of_isomorphism (Hsusp theory n A)) x)⁻¹
-         ... = Hsusp theory n B (Hh theory (succ n) (pmap.mk (susp.functor f) !refl) ((Hsusp theory n A)⁻¹ x))
-               : by exact (Hsusp_natural theory n (pmap.mk f p) ((Hsusp theory n A)⁻¹ᵍ x))⁻¹
-         ... = Hh theory n (pmap.mk f q) (Hsusp theory n A ((Hsusp theory n A)⁻¹ x))
-               : by exact Hsusp_natural theory n (pmap.mk f q) ((Hsusp theory n A)⁻¹ x)
+             = Hh theory n (pmap.mk f p) (Hpsusp theory n A ((Hpsusp theory n A)⁻¹ᵍ x))
+               : by exact ap (Hh theory n (pmap.mk f p)) (equiv.to_right_inv (equiv_of_isomorphism (Hpsusp theory n A)) x)⁻¹
+         ... = Hpsusp theory n B (Hh theory (succ n) (pmap.mk (susp.functor f) !refl) ((Hpsusp theory n A)⁻¹ x))
+               : by exact (Hpsusp_natural theory n (pmap.mk f p) ((Hpsusp theory n A)⁻¹ᵍ x))⁻¹
+         ... = Hh theory n (pmap.mk f q) (Hpsusp theory n A ((Hpsusp theory n A)⁻¹ x))
+               : by exact Hpsusp_natural theory n (pmap.mk f q) ((Hpsusp theory n A)⁻¹ x)
          ... = Hh theory n (pmap.mk f q) x
-               : by exact ap (Hh theory n (pmap.mk f q)) (equiv.to_right_inv (equiv_of_isomorphism (Hsusp theory n A)) x)
+               : by exact ap (Hh theory n (pmap.mk f q)) (equiv.to_right_inv (equiv_of_isomorphism (Hpsusp theory n A)) x)
 
     theorem Hh_homotopy (n : ℤ) {A B : Type*} (f g : A →* B) (h : f ~ g) : Hh theory n f ~ Hh theory n g := λ x,
     calc       Hh theory n f x
@@ -56,15 +67,15 @@ namespace homology
       { exact Hh theory n e⁻¹ᵉ* },
       { intro x, exact calc
               Hh theory n e (Hh theory n e⁻¹ᵉ* x)
-            = Hh theory n (e ∘* e⁻¹ᵉ*) x : by exact (Hcompose theory n e e⁻¹ᵉ* x)⁻¹
+            = Hh theory n (e ∘* e⁻¹ᵉ*) x : by exact (Hpcompose theory n e e⁻¹ᵉ* x)⁻¹
         ... = Hh theory n !pid x : by exact Hh_homotopy n (e ∘* e⁻¹ᵉ*) !pid (to_right_inv e) x
-        ... = x : by exact Hid theory n x
+        ... = x : by exact Hpid theory n x
       },
       { intro x, exact calc
               Hh theory n e⁻¹ᵉ* (Hh theory n e x)
-            = Hh theory n (e⁻¹ᵉ* ∘* e) x : by exact (Hcompose theory n e⁻¹ᵉ* e x)⁻¹
+            = Hh theory n (e⁻¹ᵉ* ∘* e) x : by exact (Hpcompose theory n e⁻¹ᵉ* e x)⁻¹
         ... = Hh theory n !pid x : by exact Hh_homotopy n (e⁻¹ᵉ* ∘* e) !pid (to_left_inv e) x
-        ... = x : by exact Hid theory n x
+        ... = x : by exact Hpid theory n x
       }
     end
 
diff --git a/homology/sphere.hlean b/homology/sphere.hlean
index e5eb677..d6f789f 100644
--- a/homology/sphere.hlean
+++ b/homology/sphere.hlean
@@ -1,6 +1,10 @@
--- Author: Kuen-Bang Hou (Favonia)
+/-
+Copyright (c) 2017 Kuen-Bang Hou (Favonia).
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Kuen-Bang Hou (Favonia)
+-/
 
-import core
 import .homology
 
 open eq pointed group algebra circle sphere nat equiv susp
@@ -13,7 +17,7 @@ section
 
   open homology_theory
 
-  theorem Hsphere : Π(n : ℤ)(m : ℕ), HH theory n (plift (psphere m)) ≃g HH theory (n - m) (plift (psphere 0)) :=
+  theorem Hpsphere : Π(n : ℤ)(m : ℕ), HH theory n (plift (psphere m)) ≃g HH theory (n - m) (plift (psphere 0)) :=
     begin
       intros n m, revert n, induction m with m,
       { exact λ n, isomorphism_ap (λ n, HH theory n (plift (psphere 0))) (sub_zero n)⁻¹ },
@@ -22,7 +26,7 @@ section
                ≃g HH theory n (psusp (plift (psphere m))) : by exact HH_isomorphism theory n (plift_psusp (psphere m))
            ... ≃g HH theory (succ (pred n)) (psusp (plift (psphere m)))
                   : by exact isomorphism_ap (λ n, HH theory n (psusp (plift (psphere m)))) (succ_pred n)⁻¹
-           ... ≃g HH theory (pred n) (plift (psphere m)) : by exact Hsusp theory (pred n) (plift (psphere m))
+           ... ≃g HH theory (pred n) (plift (psphere m)) : by exact Hpsusp theory (pred n) (plift (psphere m))
            ... ≃g HH theory (pred n - m) (plift (psphere 0)) : by exact v_0 (pred n)
            ... ≃g HH theory (n - succ m) (plift (psphere 0))
                   : by exact isomorphism_ap (λ n, HH theory n (plift (psphere 0))) (sub_sub n 1 m ⬝ ap (λ m, n - m) (add.comm 1 m))
diff --git a/homotopy/cohomology.hlean b/homotopy/cohomology.hlean
index 38a7e4c..8c25b70 100644
--- a/homotopy/cohomology.hlean
+++ b/homotopy/cohomology.hlean
@@ -189,7 +189,7 @@ structure cohomology_theory.{u} : Type.{u+1} :=
   (Hadditive : Π(n : ℤ) {I : Type.{u}} (X : I → Type*), has_choice 0 I →
     is_equiv (Group_pi_intro (λi, Hh n (pinl i)) : HH n (⋁ X) → Πᵍ i, HH n (X i)))
 
-structure ordinary_theory.{u} extends cohomology_theory.{u} : Type.{u+1} :=
+structure ordinary_cohomology_theory.{u} extends cohomology_theory.{u} : Type.{u+1} :=
  (Hdimension : Π(n : ℤ), n ≠ 0 → is_contr (HH n (plift pbool)))
 
 attribute cohomology_theory.HH [coercion]
@@ -270,7 +270,7 @@ cohomology_theory.mk
 -- print has_choice_lift
 -- print equiv_lift
 -- print has_choice_equiv_closed
-definition ordinary_theory_EM [constructor] (G : AbGroup) : ordinary_theory :=
-⦃ordinary_theory, cohomology_theory_spectrum (EM_spectrum G), Hdimension := EM_dimension G ⦄
+definition ordinary_cohomology_theory_EM [constructor] (G : AbGroup) : ordinary_cohomology_theory :=
+⦃ordinary_cohomology_theory, cohomology_theory_spectrum (EM_spectrum G), Hdimension := EM_dimension G ⦄
 
 end cohomology
diff --git a/homotopy/spectrum.hlean b/homotopy/spectrum.hlean
index 03e3e39..9ed3f7d 100644
--- a/homotopy/spectrum.hlean
+++ b/homotopy/spectrum.hlean
@@ -373,13 +373,17 @@ namespace spectrum
   definition spectrify_type_term {N : succ_str} (X : gen_prespectrum N) (n : N) (k : ℕ) : Type* :=
   Ω[k] (X (n +' k))
 
-  definition spectrify_type_fun' {N : succ_str} (X : gen_prespectrum N) (k : ℕ) (n : N) :
+  definition spectrify_type_fun' {N : succ_str} (X : gen_prespectrum N) (n : N) (k : ℕ) :
     Ω[k] (X n) →* Ω[k+1] (X (S n)) :=
   !loopn_succ_in⁻¹ᵉ* ∘* Ω→[k] (glue X n)
 
   definition spectrify_type_fun {N : succ_str} (X : gen_prespectrum N) (n : N) (k : ℕ) :
     spectrify_type_term X n k →* spectrify_type_term X n (k+1) :=
-  spectrify_type_fun' X k (n +' k)
+  spectrify_type_fun' X (n +' k) k
+
+  definition spectrify_type_fun_zero {N : succ_str} (X : gen_prespectrum N) (n : N) :
+    spectrify_type_fun X n 0 ~* glue X n :=
+  !pid_pcompose
 
   definition spectrify_type {N : succ_str} (X : gen_prespectrum N) (n : N) : Type* :=
   pseq_colim (spectrify_type_fun X n)
@@ -393,20 +397,28 @@ namespace spectrum
           ... ≡ Y n
   -/
 
+  definition spectrify_type_fun'_succ {N : succ_str} (X : gen_prespectrum N) (n : N) (k : ℕ) :
+    spectrify_type_fun' X n (succ k) ~* Ω→ (spectrify_type_fun' X n k) :=
+  begin
+    refine _ ⬝* !ap1_pcompose⁻¹*,
+    apply !pwhisker_right, 
+    refine !to_pinv_pequiv_MK2
+  end
+
   definition spectrify_pequiv {N : succ_str} (X : gen_prespectrum N) (n : N) :
     spectrify_type X n ≃* Ω (spectrify_type X (S n)) :=
   begin
     refine !pshift_equiv ⬝e* _,
-    transitivity pseq_colim (λk, spectrify_type_fun' X (succ k) (S n +' k)),
+    transitivity pseq_colim (λk, spectrify_type_fun' X (S n +' k) (succ k)),
     fapply pseq_colim_pequiv,
     { intro n, apply loopn_pequiv_loopn, apply pequiv_ap X, apply succ_str.add_succ },
-    { intro k, apply to_homotopy,
+    { exact abstract begin intro k,
       refine !passoc⁻¹* ⬝* _, refine pwhisker_right _ (loopn_succ_in_inv_natural (succ k) _) ⬝* _,
       refine !passoc ⬝* _ ⬝* !passoc⁻¹*, apply pwhisker_left,
       refine !apn_pcompose⁻¹* ⬝* _ ⬝* !apn_pcompose, apply apn_phomotopy,
-      exact !glue_ptransport⁻¹* },
+      exact !glue_ptransport⁻¹* end end },
     refine _ ⬝e* !pseq_colim_loop⁻¹ᵉ*,
-    refine pseq_colim_equiv_constant (λn, !ap1_pcompose⁻¹*),
+    exact pseq_colim_equiv_constant (λn, !spectrify_type_fun'_succ),
   end
 
   definition spectrify [constructor] {N : succ_str} (X : gen_prespectrum N) : gen_spectrum N :=
@@ -419,21 +431,31 @@ namespace spectrum
   -- note: the forward map is (currently) not definitionally equal to gluen. Is that a problem?
   definition equiv_gluen {N : succ_str} (X : gen_spectrum N) (n : N) (k : ℕ)
     : X n ≃* Ω[k] (X (n +' k)) :=
-  by induction k with k f; reflexivity; exact f ⬝e* loopn_pequiv_loopn k (equiv_glue X (n +' k))
-                                                ⬝e* !loopn_succ_in⁻¹ᵉ*
+  by induction k with k f; reflexivity; exact f ⬝e* (loopn_pequiv_loopn k (equiv_glue X (n +' k))
+                                                ⬝e* !loopn_succ_in⁻¹ᵉ*)
+
+  definition equiv_gluen_inv_succ {N : succ_str} (X : gen_spectrum N) (n : N) (k : ℕ) :
+    (equiv_gluen X n (k+1))⁻¹ᵉ* ~*
+    (equiv_gluen X n k)⁻¹ᵉ* ∘* Ω→[k] (equiv_glue X (n +' k))⁻¹ᵉ* ∘* !loopn_succ_in :=
+  begin
+    refine !trans_pinv ⬝* pwhisker_left _ _, refine !trans_pinv ⬝* _, refine !to_pinv_pequiv_MK2 ◾* !pinv_pinv
+  end
 
   definition spectrify_map {N : succ_str} {X : gen_prespectrum N} : X →ₛ spectrify X :=
   begin
     fapply smap.mk,
     { intro n, exact pinclusion _ 0 },
-    { intro n, apply phomotopy_of_psquare, refine !pid_pcompose⁻¹* ⬝ph* _,
+    { intro n, apply phomotopy_of_psquare,
       refine !pid_pcompose⁻¹* ⬝ph* _,
-      --pshift_equiv_pinclusion (spectrify_type_fun X n) 0
-      refine _ ⬝v* _,
-      rotate 1, exact pshift_equiv_pinclusion (spectrify_type_fun X n) 0,
---      refine !passoc⁻¹* ⬝* pwhisker_left _ _ ⬝* _,
-      exact sorry
-}
+      refine !passoc ⬝* pwhisker_left _ (pshift_equiv_pinclusion (spectrify_type_fun X n) 0) ⬝* _,
+      refine !passoc⁻¹* ⬝* _,
+      refine _ ◾* (spectrify_type_fun_zero X n ⬝* !pid_pcompose⁻¹*),
+      refine !passoc ⬝* pwhisker_left _ !pseq_colim_pequiv_pinclusion ⬝* _,
+      refine pwhisker_left _ (pwhisker_left _ (ap1_pid) ⬝* !pcompose_pid) ⬝* _,
+      refine !passoc ⬝* pwhisker_left _ !seq_colim_equiv_constant_pinclusion ⬝* _, 
+      apply pinv_left_phomotopy_of_phomotopy,
+      exact !pseq_colim_loop_pinclusion⁻¹*
+    }
   end
 
   definition spectrify.elim {N : succ_str} {X : gen_prespectrum N} {Y : gen_spectrum N}
@@ -442,7 +464,9 @@ namespace spectrum
     fapply smap.mk,
     { intro n, fapply pseq_colim.elim,
       { intro k, refine !equiv_gluen⁻¹ᵉ* ∘* apn k (f (n +' k)) },
-      { intro k, apply to_homotopy, exact sorry }},
+      { intro k, refine !passoc ⬝* pwhisker_right _ !equiv_gluen_inv_succ ⬝* _,
+        refine !passoc ⬝* _, apply pwhisker_left,
+        refine !passoc ⬝* _, exact sorry }},
     { intro n, exact sorry }
   end
 
diff --git a/move_to_lib.hlean b/move_to_lib.hlean
index 340eb82..14bf911 100644
--- a/move_to_lib.hlean
+++ b/move_to_lib.hlean
@@ -180,6 +180,13 @@ namespace group
   definition isomorphism_ap {A : Type} (F : A → Group) {a b : A} (p : a = b) : F a ≃g F b :=
     isomorphism_of_eq (ap F p)
 
+  definition interchange (G : AbGroup) (a b c d : G) : (a * b) * (c * d) = (a * c) * (b * d) :=
+  calc (a * b) * (c * d) = a * (b * (c * d)) : by exact mul.assoc a b (c * d)
+                     ... = a * ((b * c) * d) : by exact ap (λ bcd, a * bcd) (mul.assoc b c d)⁻¹
+                     ... = a * ((c * b) * d) : by exact ap (λ bc, a * (bc * d)) (mul.comm b c)
+                     ... = a * (c * (b * d)) : by exact ap (λ bcd, a * bcd) (mul.assoc c b d)
+                     ... = (a * c) * (b * d) : by exact (mul.assoc a c (b * d))⁻¹
+
 end group open group
 
 namespace function

From db6fccc971ed0a439904eabb021fc1b1739a0d7f Mon Sep 17 00:00:00 2001
From: spiceghello <stefano.piceghello@uib.no>
Date: Thu, 8 Jun 2017 14:50:25 -0600
Subject: [PATCH 23/24] pmap_eta

---
 pointed.hlean | 9 +++++++++
 1 file changed, 9 insertions(+)

diff --git a/pointed.hlean b/pointed.hlean
index 8f1ea82..778f3bb 100644
--- a/pointed.hlean
+++ b/pointed.hlean
@@ -142,5 +142,14 @@ namespace pointed
   -- definition phomotopy_eq_equiv_phomotopy2 : p = q ≃ p ~*2 q :=
   -- sorry
 
+/- Homotopy between a function and its eta expansion -/
+
+  definition pmap_eta {X Y : Type*} (f : X →* Y) : f ~* pmap.mk f (pmap.resp_pt f) :=
+  begin
+    fapply phomotopy.mk,
+    reflexivity,
+    esimp, exact !idp_con
+  end
+
 
 end pointed

From a06ecd45233bc3e7215c109cb60e5e318f0e6c19 Mon Sep 17 00:00:00 2001
From: spiceghello <stefano.piceghello@uib.no>
Date: Thu, 8 Jun 2017 15:07:50 -0600
Subject: [PATCH 24/24] part of spectrify_elim

---
 homotopy/spectrum.hlean | 12 +++++++++++-
 pointed.hlean           |  1 -
 2 files changed, 11 insertions(+), 2 deletions(-)

diff --git a/homotopy/spectrum.hlean b/homotopy/spectrum.hlean
index 9ed3f7d..7e4fdb2 100644
--- a/homotopy/spectrum.hlean
+++ b/homotopy/spectrum.hlean
@@ -466,7 +466,17 @@ namespace spectrum
       { intro k, refine !equiv_gluen⁻¹ᵉ* ∘* apn k (f (n +' k)) },
       { intro k, refine !passoc ⬝* pwhisker_right _ !equiv_gluen_inv_succ ⬝* _,
         refine !passoc ⬝* _, apply pwhisker_left,
-        refine !passoc ⬝* _, exact sorry }},
+        refine !passoc ⬝* _,
+        refine pwhisker_left _ ((passoc _ _ (_ ∘* _))⁻¹*) ⬝* _,
+        refine pwhisker_left _ !passoc⁻¹* ⬝* _,
+        refine pwhisker_left _ (pwhisker_right _ (phomotopy_pinv_right_of_phomotopy (!loopn_succ_in_natural)⁻¹*)⁻¹*) ⬝* _,
+        refine pwhisker_right _ !apn_pinv ⬝* _,
+        refine (phomotopy_pinv_left_of_phomotopy _)⁻¹*,
+        refine pwhisker_right _ !pmap_eta⁻¹* ⬝* _,
+        refine apn_psquare k _,
+        refine pwhisker_right _ _  ⬝* psquare_of_phomotopy !smap.glue_square,
+        exact !pmap_eta⁻¹*
+      }},
     { intro n, exact sorry }
   end
 
diff --git a/pointed.hlean b/pointed.hlean
index 778f3bb..453a3cd 100644
--- a/pointed.hlean
+++ b/pointed.hlean
@@ -151,5 +151,4 @@ namespace pointed
     esimp, exact !idp_con
   end
 
-
 end pointed