From d014e50cd7b538e9ab36c69cec5417bbdcc181b0 Mon Sep 17 00:00:00 2001
From: favonia <favonia@gmail.com>
Date: Tue, 6 Jun 2017 12:33:22 -0600
Subject: [PATCH 01/18] Add isomorphism_ap.

---
 move_to_lib.hlean | 7 +++++++
 1 file changed, 7 insertions(+)

diff --git a/move_to_lib.hlean b/move_to_lib.hlean
index 59cd841..81cabe3 100644
--- a/move_to_lib.hlean
+++ b/move_to_lib.hlean
@@ -95,6 +95,13 @@ namespace eq
 
 end eq open eq
 
+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)
+
+end group
+
 namespace trunc
 
   -- TODO: redefine loopn_ptrunc_pequiv

From e2a12f7db7a75a80df39cc6dc58a45ff6a6390e0 Mon Sep 17 00:00:00 2001
From: favonia <favonia@gmail.com>
Date: Tue, 6 Jun 2017 12:34:13 -0600
Subject: [PATCH 02/18] Make A in isomorphism_ap implicit.

---
 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 81cabe3..1b52a94 100644
--- a/move_to_lib.hlean
+++ b/move_to_lib.hlean
@@ -97,7 +97,7 @@ end eq open eq
 
 namespace group
 
-  definition isomorphism_ap (A : Type) (F : A → Group) {a b : A} (p : a = b) : F a ≃g F b :=
+  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)
 
 end group

From 61c9f175d38a91c89219254118ff6052dc1410b9 Mon Sep 17 00:00:00 2001
From: favonia <favonia@gmail.com>
Date: Tue, 6 Jun 2017 14:29:41 -0600
Subject: [PATCH 03/18] Add HH_base_indep.

---
 homology/homology.hlean | 40 ++++++++++++++++++++++++++--------------
 1 file changed, 26 insertions(+), 14 deletions(-)

diff --git a/homology/homology.hlean b/homology/homology.hlean
index f5649aa..22f84c7 100644
--- a/homology/homology.hlean
+++ b/homology/homology.hlean
@@ -5,19 +5,31 @@ open eq spectrum int trunc pointed EM group algebra circle sphere nat EM.ops equ
 
 namespace homology
 
-/- homology theory -/
+  /- homology theory -/
+
+  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*} (g : Y →* Z) (f : X →* Y) (x : HH n X),
+      Hh n (g ∘* f) x = Hh n g (Hh n f x))
+    (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)
+    (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))
+  )
+
+  section
+    parameter (theory : homology_theory)
+    open homology_theory
+
+    definition 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)
+
+  end
 
-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*} (g : Y →* Z) (f : X →* Y) (x : HH n X),
-    Hh n (g ∘* f) x = Hh n g (Hh n f x))
-  (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)
-  (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))
-)
 end homology

From 5e4c536d27ec0b9553fdbcd22bc8b2e9ff6041f1 Mon Sep 17 00:00:00 2001
From: Floris van Doorn <fpv@andrew.cmu.edu>
Date: Tue, 6 Jun 2017 17:07:07 -0400
Subject: [PATCH 04/18] progress on spectrify

---
 colim.hlean             | 50 ++++++++++++++++++++++++++++-------------
 homotopy/spectrum.hlean | 10 +++++++--
 2 files changed, 43 insertions(+), 17 deletions(-)

diff --git a/colim.hlean b/colim.hlean
index 5aaf1b5..feb238f 100644
--- a/colim.hlean
+++ b/colim.hlean
@@ -1,6 +1,6 @@
 -- authors: Floris van Doorn, Egbert Rijke
 
-import hit.colimit types.fin homotopy.chain_complex .move_to_lib
+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
 
 namespace seq_colim
@@ -8,7 +8,7 @@ namespace seq_colim
   definition pseq_colim [constructor] {X : ℕ → Type*} (f : Πn, X n →* X (n+1)) : Type* :=
   pointed.MK (seq_colim f) (@sι _ _ 0 pt)
 
-  definition inclusion_pt [constructor] {X : ℕ → Type*} (f : Πn, X n →* X (n+1)) (n : ℕ)
+  definition inclusion_pt {X : ℕ → Type*} (f : Πn, X n →* X (n+1)) (n : ℕ)
     : inclusion f (Point (X n)) = Point (pseq_colim f) :=
   begin
     induction n with n p,
@@ -249,6 +249,10 @@ namespace seq_colim
     { exact ap (ι _) !respect_pt }
   end
 
+  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 refine !idp_con ⬝ _, esimp, exact sorry end
+
   section functor
   variable {f}
   variables {A' : ℕ → Type} {f' : seq_diagram A'}
@@ -305,6 +309,30 @@ 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 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_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
+
+  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
+
   definition is_equiv_seq_colim_rec (P : seq_colim f → Type) :
     is_equiv (seq_colim_rec_unc :
       (Σ(Pincl : Π ⦃n : ℕ⦄ (a : A n), P (ι f a)),
@@ -327,19 +355,6 @@ namespace seq_colim
   equiv.mk _ !is_equiv_seq_colim_rec
   end functor
 
-  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 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.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
@@ -361,6 +376,7 @@ namespace seq_colim
   theorem prep0_succ_lemma {A : ℕ → Type*} (f : pseq_diagram A) (n : ℕ)
     (p : rep0 (λn x, f x) n pt = rep0 (λn x, f x) n pt)
     (q : prep0 f n (Point (A 0)) = Point (A n))
+
     : loop_equiv_eq_closed (ap (@f n) q ⬝ respect_pt (@f n))
     (ap (@f n) p) = Ω→(@f n) (loop_equiv_eq_closed q p) :=
   by rewrite [▸*, con_inv, ↑ap1_gen, +ap_con, ap_inv, +con.assoc]
@@ -466,6 +482,10 @@ namespace seq_colim
     { exact sorry }
   end
 
+  definition pseq_colim_loop_pinclusion {X : ℕ → Type*} (f : Πn, X n →* X (n+1)) (n : ℕ) :
+    pseq_colim_loop f ∘* Ω→ (pinclusion f n) ~* pinclusion (λn, Ω→(f n)) n :=
+  sorry
+
   -- open succ_str
   -- definition pseq_colim_succ_str_change_index' {N : succ_str} {B : N → Type*} (n : N) (m : ℕ)
   --   (h : Πn, B n →* B (S n)) :
diff --git a/homotopy/spectrum.hlean b/homotopy/spectrum.hlean
index 0cf3cf0..953faf3 100644
--- a/homotopy/spectrum.hlean
+++ b/homotopy/spectrum.hlean
@@ -396,8 +396,8 @@ namespace spectrum
   definition spectrify_pequiv {N : succ_str} (X : gen_prespectrum N) (n : N) :
     spectrify_type X n ≃* Ω (spectrify_type X (S n)) :=
   begin
-    refine _ ⬝e* !pseq_colim_loop⁻¹ᵉ*,
     refine !pshift_equiv ⬝e* _,
+    refine _ ⬝e* !pseq_colim_loop⁻¹ᵉ*,
     transitivity pseq_colim (λk, spectrify_type_fun' X (succ k) (S n +' k)), rotate 1,
     refine pseq_colim_equiv_constant (λn, !ap1_pcompose⁻¹*),
     fapply pseq_colim_pequiv,
@@ -426,7 +426,13 @@ namespace spectrum
   begin
     fapply smap.mk,
     { intro n, exact pinclusion _ 0 },
-    { intro n, exact sorry }
+    { 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,
+      exact sorry
+}
   end
 
   definition spectrify.elim {N : succ_str} {X : gen_prespectrum N} {Y : gen_spectrum N}

From 7940bf0cd601913a94daaccd6eaa77391c0800ab Mon Sep 17 00:00:00 2001
From: favonia <favonia@gmail.com>
Date: Tue, 6 Jun 2017 16:57:17 -0600
Subject: [PATCH 05/18] Add pmap.eta.

---
 move_to_lib.hlean | 7 +++++++
 1 file changed, 7 insertions(+)

diff --git a/move_to_lib.hlean b/move_to_lib.hlean
index 1b52a94..6944a29 100644
--- a/move_to_lib.hlean
+++ b/move_to_lib.hlean
@@ -102,6 +102,13 @@ namespace group
 
 end group
 
+namespace pmap
+
+  definition eta {A B : Type*} (f : A →* B) : pmap.mk f (respect_pt f) = f :=
+  begin induction f, reflexivity end
+
+end pmap
+
 namespace trunc
 
   -- TODO: redefine loopn_ptrunc_pequiv

From 52b8fee078b9179669d6752a5056931421c968aa Mon Sep 17 00:00:00 2001
From: favonia <favonia@gmail.com>
Date: Tue, 6 Jun 2017 16:57:34 -0600
Subject: [PATCH 06/18] Clean up homotopy.hlean a little bit.

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

diff --git a/homology/homology.hlean b/homology/homology.hlean
index 22f84c7..3610243 100644
--- a/homology/homology.hlean
+++ b/homology/homology.hlean
@@ -1,7 +1,7 @@
 import ..homotopy.spectrum ..homotopy.EM ..algebra.arrow_group ..algebra.direct_sum ..homotopy.fwedge ..choice ..homotopy.pushout ..move_to_lib
 
-open eq spectrum int trunc pointed EM group algebra circle sphere nat EM.ops equiv susp is_trunc
-     function fwedge cofiber bool lift sigma is_equiv choice pushout algebra unit pi smash
+open eq spectrum int pointed group algebra sphere nat equiv susp is_trunc
+     function fwedge cofiber lift is_equiv choice algebra pi smash
 
 namespace homology
 

From 32a6cc639d7685bc874f2a0f2bdfa27967e3593b Mon Sep 17 00:00:00 2001
From: favonia <favonia@gmail.com>
Date: Tue, 6 Jun 2017 16:57:55 -0600
Subject: [PATCH 07/18] Add several helper functions.

---
 homology/homology.hlean | 47 +++++++++++++++++++++++++++++++++++------
 1 file changed, 41 insertions(+), 6 deletions(-)

diff --git a/homology/homology.hlean b/homology/homology.hlean
index 3610243..12ecbf7 100644
--- a/homology/homology.hlean
+++ b/homology/homology.hlean
@@ -11,25 +11,60 @@ namespace homology
     (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*} (g : Y →* Z) (f : X →* Y) (x : HH n X),
-      Hh n (g ∘* f) x = Hh n g (Hh n f x))
+    (Hcompose : Π(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)
     (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))
-  )
+    (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)))
 
   section
     parameter (theory : homology_theory)
     open homology_theory
 
     definition HH_base_indep (n : ℤ) {A : Type} (a b : A)
-    : HH theory n (pType.mk A a) ≃g HH theory n (pType.mk A b) :=
+      : 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)
 
+    definition 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 q) x
+               : by exact ap (Hh theory n (pmap.mk f q)) (equiv.to_right_inv (equiv_of_isomorphism (Hsusp theory n A)) x)
+
+    definition 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
+             = Hh theory n (pmap.mk f (respect_pt f)) x : by exact ap (λ f, Hh theory n f x) (pmap.eta f)⁻¹
+         ... = Hh theory n (pmap.mk f (h pt ⬝ respect_pt g)) x : by exact Hh_homotopy' n f (respect_pt f) (h pt ⬝ respect_pt g) x
+         ... = Hh theory n g x : by exact ap (λ f, Hh theory n f x) (@pmap_eq _ _ (pmap.mk f (h pt ⬝ respect_pt g)) _ h (refl (h pt ⬝ respect_pt g)))
+
+    definition is_equiv_Hh (n : ℤ) {A B : Type*} (e : A ≃* B) : is_equiv (Hh theory n e) :=
+    begin
+      fapply adjointify,
+      { 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 !pid x : by exact Hh_homotopy n (e ∘* e⁻¹ᵉ*) !pid (to_right_inv e) x
+        ... = x : by exact Hid 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 !pid x : by exact Hh_homotopy n (e⁻¹ᵉ* ∘* e) !pid (to_left_inv e) x
+        ... = x : by exact Hid theory n x
+      }
+    end
+
   end
 
 end homology

From b6394b97508b6f63f4c979c7e019197d7f433699 Mon Sep 17 00:00:00 2001
From: favonia <favonia@gmail.com>
Date: Tue, 6 Jun 2017 17:12:50 -0600
Subject: [PATCH 08/18] A more useful lemma!

---
 homology/homology.hlean | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

diff --git a/homology/homology.hlean b/homology/homology.hlean
index 12ecbf7..2deb9b5 100644
--- a/homology/homology.hlean
+++ b/homology/homology.hlean
@@ -47,8 +47,11 @@ namespace homology
          ... = Hh theory n (pmap.mk f (h pt ⬝ respect_pt g)) x : by exact Hh_homotopy' n f (respect_pt f) (h pt ⬝ respect_pt g) x
          ... = Hh theory n g x : by exact ap (λ f, Hh theory n f x) (@pmap_eq _ _ (pmap.mk f (h pt ⬝ respect_pt g)) _ h (refl (h pt ⬝ respect_pt g)))
 
-    definition is_equiv_Hh (n : ℤ) {A B : Type*} (e : A ≃* B) : is_equiv (Hh theory n e) :=
+    definition HH_isomorphism (n : ℤ) {A B : Type*} (e : A ≃* B)
+      : HH theory n A ≃g HH theory n B :=
     begin
+      fapply isomorphism.mk,
+      { exact Hh theory n e },
       fapply adjointify,
       { exact Hh theory n e⁻¹ᵉ* },
       { intro x, exact calc

From a292dba89f2dfcc6457d1ba9d0a36d076316fba7 Mon Sep 17 00:00:00 2001
From: favonia <favonia@gmail.com>
Date: Tue, 6 Jun 2017 17:18:10 -0600
Subject: [PATCH 09/18] Merge two group namespaces.

---
 move_to_lib.hlean | 10 +++-------
 1 file changed, 3 insertions(+), 7 deletions(-)

diff --git a/move_to_lib.hlean b/move_to_lib.hlean
index 6944a29..95b6aa4 100644
--- a/move_to_lib.hlean
+++ b/move_to_lib.hlean
@@ -95,13 +95,6 @@ namespace eq
 
 end eq open eq
 
-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)
-
-end group
-
 namespace pmap
 
   definition eta {A B : Type*} (f : A →* B) : pmap.mk f (respect_pt f) = f :=
@@ -184,6 +177,9 @@ namespace group
   --   : @is_mul_hom G G' (@ab_group.to_group _ (AbGroup.struct G)) _ φ :=
   -- homomorphism.struct φ
 
+  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)
+
 end group open group
 
 namespace function

From bf8f77a9e551ea5f6b86b32b4c67cdd85ef933cf Mon Sep 17 00:00:00 2001
From: favonia <favonia@gmail.com>
Date: Tue, 6 Jun 2017 17:30:42 -0600
Subject: [PATCH 10/18] Add Hsphere.

---
 homology/sphere.hlean | 22 +++++++++++++++++-----
 1 file changed, 17 insertions(+), 5 deletions(-)

diff --git a/homology/sphere.hlean b/homology/sphere.hlean
index 30ddc15..e5eb677 100644
--- a/homology/sphere.hlean
+++ b/homology/sphere.hlean
@@ -1,7 +1,7 @@
 -- Author: Kuen-Bang Hou (Favonia)
 
-import core types.lift
-import ..homotopy.homology
+import core
+import .homology
 
 open eq pointed group algebra circle sphere nat equiv susp
      function sphere homology int lift
@@ -13,9 +13,21 @@ section
 
   open homology_theory
 
-  theorem Hsphere : Π(n : ℕ), HH theory n (plift (psphere n)) ≃g HH theory 0 (plift (psphere 0)) :=
-    sorry
-
+  theorem Hsphere : Π(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)⁻¹ },
+      { intro n, exact calc
+                  HH theory n (plift (psusp (psphere m)))
+               ≃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 - 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))
+      }
+    end
 end
 
 end homology

From 5afbc4afddd5156d3c06334bc30eca83f5cca072 Mon Sep 17 00:00:00 2001
From: spiceghello <stefano.piceghello@uib.no>
Date: Tue, 6 Jun 2017 17:52:30 -0600
Subject: [PATCH 11/18] a lemma for spectrification

---
 colim.hlean | 18 ++++++++++++++++--
 1 file changed, 16 insertions(+), 2 deletions(-)

diff --git a/colim.hlean b/colim.hlean
index feb238f..e772352 100644
--- a/colim.hlean
+++ b/colim.hlean
@@ -13,7 +13,7 @@ namespace seq_colim
   begin
     induction n with n p,
       reflexivity,
-      exact (ap (sι f) (respect_pt _))⁻¹ᵖ ⬝ !glue ⬝ p
+      exact (ap (sι f) (respect_pt _))⁻¹ᵖ ⬝ (!glue ⬝ p)
   end
 
   definition pinclusion [constructor] {X : ℕ → Type*} (f : Πn, X n →* X (n+1)) (n : ℕ)
@@ -251,7 +251,21 @@ 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 refine !idp_con ⬝ _, esimp, exact sorry end
+  phomotopy.mk homotopy.rfl begin 
+    refine !idp_con ⬝ _, esimp,
+    induction n with n IH,
+    { esimp[inclusion_pt], esimp[shift_diag], exact !idp_con⁻¹ },
+    { esimp[inclusion_pt], refine !con_inv_cancel_left ⬝ _,
+      rewrite ap_con, rewrite ap_con,
+      refine _ ⬝ whisker_right _ !con.assoc,
+      refine _ ⬝ (con.assoc (_ ⬝ _) _ _)⁻¹,
+      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,
+      symmetry, exact eq_of_square !natural_square
+  }
+  end
 
   section functor
   variable {f}

From fecc9b4a701d1d93b72017cd5ef3945ad617c49a Mon Sep 17 00:00:00 2001
From: favonia <favonia@gmail.com>
Date: Tue, 6 Jun 2017 18:09:19 -0600
Subject: [PATCH 12/18] The statement of susp_product.

---
 susp_product.hlean | 5 +++++
 1 file changed, 5 insertions(+)
 create mode 100644 susp_product.hlean

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

From 74955d5a755f92dab8d273b218b5d4ca9e4824f5 Mon Sep 17 00:00:00 2001
From: Robert Rose <rrose1@indiana.edu>
Date: Tue, 6 Jun 2017 21:53:45 -0600
Subject: [PATCH 13/18] Stub of seq_colim

---
 algebra/seq_colim.hlean | 34 ++++++++++++++++++++++++++++++++++
 1 file changed, 34 insertions(+)
 create mode 100644 algebra/seq_colim.hlean

diff --git a/algebra/seq_colim.hlean b/algebra/seq_colim.hlean
new file mode 100644
index 0000000..6619686
--- /dev/null
+++ b/algebra/seq_colim.hlean
@@ -0,0 +1,34 @@
+import .direct_sum .quotient_group
+
+open eq algebra is_trunc set_quotient relation sigma prod sum list trunc function equiv sigma.ops nat
+
+namespace group
+
+  section
+
+    parameters (A : @trunctype.mk 0 ℕ _ → AddAbGroup) (f : Πi , A i → A (i + 1))
+    variables {A' : AddAbGroup}
+
+    definition seq_colim_carrier : AddAbGroup := dirsum A
+    inductive seq_colim_rel : seq_colim_carrier → Type :=
+    | rmk : Πi a, seq_colim_rel ((dirsum_incl A i a) - (dirsum_incl A (i + 1) (f i a)))
+   
+    definition seq_colim : AddAbGroup := quotient_ab_group_gen seq_colim_carrier (λa, ∥seq_colim_rel a∥)
+ 
+    definition seq_colim_incl [constructor] (i : ℕ) : A i →a seq_colim :=
+      qg_map _ ∘g dirsum_incl A i
+
+    definition seq_colim_quotient (h : Πi, A i →a A') (k : Πi a, h i a = h (i + 1) (f i a))
+                                  (v : seq_colim_carrier) (r : ∥seq_colim_rel v∥) : dirsum_elim h v = 0 :=
+      begin
+        induction r with r, induction r,
+      end
+
+    definition seq_colim_elim [constructor] (h : Πi, A i →a A') 
+                                            (k : Πi a, h i a = h (i + 1) (f i a)) : seq_colim →a A' :=
+      gqg_elim _ (dirsum_elim h) (seq_colim_quotient h k)
+
+  end
+
+end group
+

From 3881982774f9c60e7a920f7b8b9a816ed5905c33 Mon Sep 17 00:00:00 2001
From: Floris van Doorn <fpv@andrew.cmu.edu>
Date: Wed, 7 Jun 2017 00:54:52 -0400
Subject: [PATCH 14/18] small changes to spectrum

---
 homotopy/smash.hlean    | 2 +-
 homotopy/spectrum.hlean | 9 +++++----
 2 files changed, 6 insertions(+), 5 deletions(-)

diff --git a/homotopy/smash.hlean b/homotopy/smash.hlean
index 4b6d875..82d5a98 100644
--- a/homotopy/smash.hlean
+++ b/homotopy/smash.hlean
@@ -5,7 +5,7 @@ import homotopy.smash types.pointed2 .pushout homotopy.red_susp
 open bool pointed eq equiv is_equiv sum bool prod unit circle cofiber prod.ops wedge is_trunc
      function red_susp unit
 
-  /- To prove: Σ(X × Y) ≃ ΣX ∨ ΣY ∨ Σ(X ∧ Y) (?) (notation means suspension, wedge, smash) -/
+  /- To prove: Σ(X × Y) ≃ ΣX ∨ ΣY ∨ Σ(X ∧ Y) (notation means suspension, wedge, smash) -/
 
   /- To prove: Σ(X ∧ Y) ≃ X ★ Y (?) (notation means suspension, smash, join) -/
 
diff --git a/homotopy/spectrum.hlean b/homotopy/spectrum.hlean
index 953faf3..33dc6aa 100644
--- a/homotopy/spectrum.hlean
+++ b/homotopy/spectrum.hlean
@@ -397,16 +397,16 @@ namespace spectrum
     spectrify_type X n ≃* Ω (spectrify_type X (S n)) :=
   begin
     refine !pshift_equiv ⬝e* _,
-    refine _ ⬝e* !pseq_colim_loop⁻¹ᵉ*,
-    transitivity pseq_colim (λk, spectrify_type_fun' X (succ k) (S n +' k)), rotate 1,
-    refine pseq_colim_equiv_constant (λn, !ap1_pcompose⁻¹*),
+    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,
       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⁻¹* },
+    refine _ ⬝e* !pseq_colim_loop⁻¹ᵉ*,
+    refine pseq_colim_equiv_constant (λn, !ap1_pcompose⁻¹*),
   end
 
   definition spectrify [constructor] {N : succ_str} (X : gen_prespectrum N) : gen_spectrum N :=
@@ -431,6 +431,7 @@ namespace spectrum
       --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
 }
   end

From 18ee7ce41080447ae943c015f87e8d49d98e22ef Mon Sep 17 00:00:00 2001
From: Floris van Doorn <fpv@andrew.cmu.edu>
Date: Wed, 7 Jun 2017 01:01:19 -0400
Subject: [PATCH 15/18] redefine direct_sum to use multiplicative groups

---
 algebra/direct_sum.hlean | 65 +++++++++++++++++++---------------------
 algebra/graded.hlean     |  2 +-
 algebra/seq_colim.hlean  | 27 ++++++++---------
 3 files changed, 44 insertions(+), 50 deletions(-)

diff --git a/algebra/direct_sum.hlean b/algebra/direct_sum.hlean
index e5eaf82..5d8e388 100644
--- a/algebra/direct_sum.hlean
+++ b/algebra/direct_sum.hlean
@@ -12,32 +12,27 @@ open eq algebra is_trunc set_quotient relation sigma prod sum list trunc functio
 
 namespace group
 
-  variables {G G' : AddGroup} (H : subgroup_rel G) (N : normal_subgroup_rel G) {g g' h h' k : G}
-            {A B : AddAbGroup}
-
-  variables (X : Set) {l l' : list (X ⊎ X)}
-
   section
 
-    parameters {I : Set} (Y : I → AddAbGroup)
-    variables {A' : AddAbGroup} {Y' : I → AddAbGroup}
+    parameters {I : Set} (Y : I → AbGroup)
+    variables {A' : AbGroup} {Y' : I → AbGroup}
 
-    definition dirsum_carrier : AddAbGroup := free_ab_group (trunctype.mk (Σi, Y i) _)
+    definition dirsum_carrier : AbGroup := free_ab_group (trunctype.mk (Σi, Y i) _)
     local abbreviation ι [constructor] := @free_ab_group_inclusion
     inductive dirsum_rel : dirsum_carrier → Type :=
-    | rmk : Πi y₁ y₂, dirsum_rel (ι ⟨i, y₁⟩ + ι ⟨i, y₂⟩ +  -(ι ⟨i, y₁ + y₂⟩))
+    | rmk : Πi y₁ y₂, dirsum_rel (ι ⟨i, y₁⟩ * ι ⟨i, y₂⟩ *  (ι ⟨i, y₁ * y₂⟩)⁻¹)
 
-    definition dirsum : AddAbGroup := quotient_ab_group_gen dirsum_carrier (λg, ∥dirsum_rel g∥)
+    definition dirsum : AbGroup := quotient_ab_group_gen dirsum_carrier (λg, ∥dirsum_rel g∥)
 
-    -- definition dirsum_carrier_incl [constructor] (i : I) : Y i →a dirsum_carrier :=
+    -- definition dirsum_carrier_incl [constructor] (i : I) : Y i →g dirsum_carrier :=
 
-    definition dirsum_incl [constructor] (i : I) : Y i →a dirsum :=
-    add_homomorphism.mk (λy, class_of (ι ⟨i, y⟩))
+    definition dirsum_incl [constructor] (i : I) : Y i →g dirsum :=
+    homomorphism.mk (λy, class_of (ι ⟨i, y⟩))
       begin intro g h, symmetry, apply gqg_eq_of_rel, apply tr, apply dirsum_rel.rmk end
 
     parameter {Y}
     definition dirsum.rec {P : dirsum → Type} [H : Πg, is_prop (P g)]
-      (h₁ : Πi (y : Y i), P (dirsum_incl i y)) (h₂ : P 0) (h₃ : Πg h, P g → P h → P (g + h)) :
+      (h₁ : Πi (y : Y i), P (dirsum_incl i y)) (h₂ : P 1) (h₃ : Πg h, P g → P h → P (g * h)) :
       Πg, P g :=
     begin
       refine @set_quotient.rec_prop _ _ _ H _,
@@ -49,42 +44,42 @@ namespace group
         exact h₃ _ _ (h₁ i y) ih,
       induction v with i y,
       refine h₃ (gqg_map _ _ (class_of [inr ⟨i, y⟩])) _ _ ih,
-      refine transport P _ (h₁ i (-y)),
+      refine transport P _ (h₁ i y⁻¹),
       refine _ ⬝ !one_mul,
       refine _ ⬝ ap (λx, mul x _) (to_respect_zero (dirsum_incl i)),
       apply gqg_eq_of_rel',
       apply tr, esimp,
-      refine transport dirsum_rel _ (dirsum_rel.rmk i (-y) y),
-      rewrite [add.left_inv, add.assoc],
+      refine transport dirsum_rel _ (dirsum_rel.rmk i y⁻¹ y),
+      rewrite [mul.left_inv, mul.assoc],
     end
 
-    definition dirsum_homotopy {φ ψ : dirsum →a A'}
+    definition dirsum_homotopy {φ ψ : dirsum →g A'}
       (h : Πi (y : Y i), φ (dirsum_incl i y) = ψ (dirsum_incl i y)) : φ ~ ψ :=
     begin
       refine dirsum.rec _ _ _,
           exact h,
         refine !to_respect_zero ⬝ !to_respect_zero⁻¹,
-      intro g₁ g₂ h₁ h₂, rewrite [+ to_respect_add', h₁, h₂]
+      intro g₁ g₂ h₁ h₂, rewrite [* to_respect_mul, h₁, h₂]
     end
 
-    definition dirsum_elim_resp_quotient (f : Πi, Y i →a A') (g : dirsum_carrier)
+    definition dirsum_elim_resp_quotient (f : Πi, Y i →g A') (g : dirsum_carrier)
       (r : ∥dirsum_rel g∥) : free_ab_group_elim (λv, f v.1 v.2) g = 1 :=
     begin
       induction r with r, induction r,
-      rewrite [to_respect_add, to_respect_neg, to_respect_add, ▸*, ↑foldl, +one_mul,
-        to_respect_add'], apply mul.right_inv
+      rewrite [to_respect_mul, to_respect_inv, to_respect_mul, ▸*, ↑foldl, *one_mul,
+        to_respect_mul], apply mul.right_inv
     end
 
-    definition dirsum_elim [constructor] (f : Πi, Y i →a A') : dirsum →a A' :=
+    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 →a A') (i : I) :
+    definition dirsum_elim_compute (f : Πi, Y i →g A') (i : I) :
       dirsum_elim f ∘g dirsum_incl i ~ f i :=
     begin
-      intro g, apply zero_add
+      intro g, apply one_mul
     end
 
-    definition dirsum_elim_unique (f : Πi, Y i →a A') (k : dirsum →a A')
+    definition dirsum_elim_unique (f : Πi, Y i →g A') (k : dirsum →g A')
       (H : Πi, k ∘g dirsum_incl i ~ f i) : k ~ dirsum_elim f :=
     begin
       apply gqg_elim_unique,
@@ -94,12 +89,12 @@ namespace group
 
   end
 
-  variables {I J : Set} {Y Y' Y'' : I → AddAbGroup}
+  variables {I J : Set} {Y Y' Y'' : I → AbGroup}
 
-  definition dirsum_functor [constructor] (f : Πi, Y i →a Y' i) : dirsum Y →a dirsum Y' :=
+  definition dirsum_functor [constructor] (f : Πi, Y i →g Y' i) : dirsum Y →g dirsum Y' :=
   dirsum_elim (λi, dirsum_incl Y' i ∘g f i)
 
-  theorem dirsum_functor_compose (f' : Πi, Y' i →a Y'' i) (f : Πi, Y i →a Y' i) :
+  theorem dirsum_functor_compose (f' : Πi, Y' i →g Y'' i) (f : Πi, Y i →g Y' i) :
     dirsum_functor f' ∘a dirsum_functor f ~ dirsum_functor (λi, f' i ∘a f i) :=
   begin
     apply dirsum_homotopy,
@@ -107,29 +102,29 @@ namespace group
   end
 
   variable (Y)
-  definition dirsum_functor_gid : dirsum_functor (λi, aid (Y i)) ~ aid (dirsum Y) :=
+  definition dirsum_functor_gid : dirsum_functor (λi, gid (Y i)) ~ gid (dirsum Y) :=
   begin
     apply dirsum_homotopy,
     intro i y, reflexivity,
   end
   variable {Y}
 
-  definition dirsum_functor_add (f f' : Πi, Y i →a Y' i) :
-    homomorphism_add (dirsum_functor f) (dirsum_functor f') ~
-    dirsum_functor (λi, homomorphism_add (f i) (f' i)) :=
+  definition dirsum_functor_mul (f f' : Πi, Y i →g Y' i) :
+    homomorphism_mul (dirsum_functor f) (dirsum_functor f') ~
+    dirsum_functor (λi, homomorphism_mul (f i) (f' i)) :=
   begin
     apply dirsum_homotopy,
     intro i y, esimp, exact sorry
   end
 
-  definition dirsum_functor_homotopy {f f' : Πi, Y i →a Y' i} (p : f ~2 f') :
+  definition dirsum_functor_homotopy {f f' : Πi, Y i →g Y' i} (p : f ~2 f') :
     dirsum_functor f ~ dirsum_functor f' :=
   begin
     apply dirsum_homotopy,
     intro i y, exact sorry
   end
 
-  definition dirsum_functor_left [constructor] (f : J → I) : dirsum (Y ∘ f) →a dirsum Y :=
+  definition dirsum_functor_left [constructor] (f : J → I) : dirsum (Y ∘ f) →g dirsum Y :=
   dirsum_elim (λj, dirsum_incl Y (f j))
 
 end group
diff --git a/algebra/graded.hlean b/algebra/graded.hlean
index e7a5053..a34dd62 100644
--- a/algebra/graded.hlean
+++ b/algebra/graded.hlean
@@ -391,7 +391,7 @@ dirsum_functor (λi, smul_homomorphism (N i) r)
 definition dirsum_smul_right_distrib (r s : R) (n : dirsum' N) :
   dirsum_smul (r + s) n = dirsum_smul r n + dirsum_smul s n :=
 begin
-  refine dirsum_functor_homotopy _ n ⬝ !dirsum_functor_add⁻¹,
+  refine dirsum_functor_homotopy _ n ⬝ !dirsum_functor_mul⁻¹,
   intro i ni, exact to_smul_right_distrib r s ni
 end
 
diff --git a/algebra/seq_colim.hlean b/algebra/seq_colim.hlean
index 6619686..76b1491 100644
--- a/algebra/seq_colim.hlean
+++ b/algebra/seq_colim.hlean
@@ -6,29 +6,28 @@ namespace group
 
   section
 
-    parameters (A : @trunctype.mk 0 ℕ _ → AddAbGroup) (f : Πi , A i → A (i + 1))
-    variables {A' : AddAbGroup}
+    parameters (A : @trunctype.mk 0 ℕ _ → AbGroup) (f : Πi , A i → A (i + 1))
+    variables {A' : AbGroup}
 
-    definition seq_colim_carrier : AddAbGroup := dirsum A
+    definition seq_colim_carrier : AbGroup := dirsum A
     inductive seq_colim_rel : seq_colim_carrier → Type :=
-    | rmk : Πi a, seq_colim_rel ((dirsum_incl A i a) - (dirsum_incl A (i + 1) (f i a)))
-   
-    definition seq_colim : AddAbGroup := quotient_ab_group_gen seq_colim_carrier (λa, ∥seq_colim_rel a∥)
- 
-    definition seq_colim_incl [constructor] (i : ℕ) : A i →a seq_colim :=
+    | rmk : Πi a, seq_colim_rel ((dirsum_incl A i a) * (dirsum_incl A (i + 1) (f i a))⁻¹)
+
+    definition seq_colim : AbGroup := quotient_ab_group_gen seq_colim_carrier (λa, ∥seq_colim_rel a∥)
+
+    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 →a A') (k : Πi a, h i a = h (i + 1) (f i a))
-                                  (v : seq_colim_carrier) (r : ∥seq_colim_rel v∥) : dirsum_elim h v = 0 :=
+    definition seq_colim_quotient (h : Πi, A i →g A') (k : Πi a, h i a = h (i + 1) (f i a))
+                                  (v : seq_colim_carrier) (r : ∥seq_colim_rel v∥) : dirsum_elim h v = 1 :=
       begin
-        induction r with r, induction r,
+        induction r with r, induction r, exact sorry
       end
 
-    definition seq_colim_elim [constructor] (h : Πi, A i →a A') 
-                                            (k : Πi a, h i a = h (i + 1) (f i a)) : seq_colim →a A' :=
+    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' :=
       gqg_elim _ (dirsum_elim h) (seq_colim_quotient h k)
 
   end
 
 end group
-

From 5fdc8ad2c8ee4d01ef7b8b9478c523e5e1b9f18c Mon Sep 17 00:00:00 2001
From: favonia <favonia@gmail.com>
Date: Tue, 6 Jun 2017 23:10:25 -0600
Subject: [PATCH 16/18] Seal several definitions as theorems.

---
 homology/homology.hlean | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/homology/homology.hlean b/homology/homology.hlean
index 2deb9b5..32e79f8 100644
--- a/homology/homology.hlean
+++ b/homology/homology.hlean
@@ -24,12 +24,12 @@ namespace homology
     parameter (theory : homology_theory)
     open homology_theory
 
-    definition HH_base_indep (n : ℤ) {A : Type} (a b : A)
+    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)
 
-    definition Hh_homotopy' (n : ℤ) {A B : Type*} (f : A → B) (p q : f pt = pt)
+    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))
@@ -41,7 +41,7 @@ namespace homology
          ... = 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)
 
-    definition Hh_homotopy (n : ℤ) {A B : Type*} (f g : A →* B) (h : f ~ g) : Hh theory n f ~ Hh theory n g := λ 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
              = Hh theory n (pmap.mk f (respect_pt f)) x : by exact ap (λ f, Hh theory n f x) (pmap.eta f)⁻¹
          ... = Hh theory n (pmap.mk f (h pt ⬝ respect_pt g)) x : by exact Hh_homotopy' n f (respect_pt f) (h pt ⬝ respect_pt g) x

From 984d564cc626c78b445c55167076938ac223d1b2 Mon Sep 17 00:00:00 2001
From: Floris van Doorn <fpv@andrew.cmu.edu>
Date: Wed, 7 Jun 2017 11:30:09 -0400
Subject: [PATCH 17/18] unbundle set in direct_sum

---
 algebra/direct_sum.hlean             | 4 ++--
 algebra/free_commutative_group.hlean | 2 +-
 algebra/free_group.hlean             | 8 ++++----
 3 files changed, 7 insertions(+), 7 deletions(-)

diff --git a/algebra/direct_sum.hlean b/algebra/direct_sum.hlean
index 5d8e388..acc32c3 100644
--- a/algebra/direct_sum.hlean
+++ b/algebra/direct_sum.hlean
@@ -14,10 +14,10 @@ namespace group
 
   section
 
-    parameters {I : Set} (Y : I → AbGroup)
+    parameters {I : Type} [is_set I] (Y : I → AbGroup)
     variables {A' : AbGroup} {Y' : I → AbGroup}
 
-    definition dirsum_carrier : AbGroup := free_ab_group (trunctype.mk (Σi, Y i) _)
+    definition dirsum_carrier : AbGroup := free_ab_group (Σi, Y i)
     local abbreviation ι [constructor] := @free_ab_group_inclusion
     inductive dirsum_rel : dirsum_carrier → Type :=
     | rmk : Πi y₁ y₂, dirsum_rel (ι ⟨i, y₁⟩ * ι ⟨i, y₂⟩ *  (ι ⟨i, y₁ * y₂⟩)⁻¹)
diff --git a/algebra/free_commutative_group.hlean b/algebra/free_commutative_group.hlean
index 759be30..d34fef9 100644
--- a/algebra/free_commutative_group.hlean
+++ b/algebra/free_commutative_group.hlean
@@ -15,7 +15,7 @@ namespace group
 
   variables {G G' : Group} {g g' h h' k : G} {A B : AbGroup}
 
-  variables (X : Set) {Y : Set} {l l' : list (X ⊎ X)}
+  variables (X : Type) {Y : Type} [is_set X] [is_set Y] {l l' : list (X ⊎ X)}
 
   /- Free Abelian Group of a set -/
   namespace free_ab_group
diff --git a/algebra/free_group.hlean b/algebra/free_group.hlean
index 125332d..291a4a8 100644
--- a/algebra/free_group.hlean
+++ b/algebra/free_group.hlean
@@ -15,7 +15,7 @@ namespace group
   variables {G G' : Group} {g g' h h' k : G} {A B : AbGroup}
 
   /- Free Group of a set -/
-  variables (X : Set) {l l' : list (X ⊎ X)}
+  variables (X : Type) [is_set X] {l l' : list (X ⊎ X)}
   namespace free_group
 
   inductive free_group_rel : list (X ⊎ X) → list (X ⊎ X) → Type :=
@@ -60,10 +60,10 @@ namespace group
   end
 
   definition free_group_one [constructor] : FG X := class_of []
-  definition free_group_inv [unfold 3] : FG X → FG X :=
+  definition free_group_inv [unfold 4] : 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 3 4] : FG X → FG X → FG X :=
+  definition free_group_mul [unfold 4 5] : 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
@@ -123,7 +123,7 @@ namespace group
   definition free_group_inclusion [constructor] (x : X) : free_group X :=
   class_of [inl x]
 
-  definition fgh_helper [unfold 5] (f : X → G) (g : G) (x : X + X) : G :=
+  definition fgh_helper [unfold 6] (f : X → G) (g : G) (x : X + X) : G :=
   g * sum.rec (λx, f x) (λx, (f x)⁻¹) x
 
   theorem fgh_helper_respect_rel (f : X → G) (r : free_group_rel X l l')

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 18/18] 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