diff --git a/group_theory/basic.hlean b/group_theory/basic.hlean
index e6d1ea7..7d26d9d 100644
--- a/group_theory/basic.hlean
+++ b/group_theory/basic.hlean
@@ -21,12 +21,9 @@ set_option class.force_new true
 namespace group
 
   definition pointed_Group [instance] (G : Group) : pointed G := pointed.mk one
-  definition pType_of_Group (G : Group) : Type* := pointed.mk' G
+  definition pType_of_Group [reducible] (G : Group) : Type* := pointed.mk' G
   definition Set_of_Group (G : Group) : Set := trunctype.mk G _
 
- -- print Type*
- -- print pType
-
   definition Group_of_CommGroup [coercion] [constructor] (G : CommGroup) : Group :=
   Group.mk G _
 
@@ -34,30 +31,79 @@ namespace group
     : comm_group (Group_of_CommGroup G) :=
   begin esimp, exact _ end
 
+  definition group_pType_of_Group [instance] (G : Group) : group (pType_of_Group G) :=
+  Group.struct G
+
   /- group homomorphisms -/
 
-  structure homomorphism (G₁ G₂ : Group) : Type :=
-    (φ : G₁ → G₂)
-    (p : Π(g h : G₁), φ (g * h) = φ g * φ h)
+  definition is_homomorphism [class] [reducible]
+    {G₁ G₂ : Type} [group G₁] [group G₂] (φ : G₁ → G₂) : Type :=
+  Π(g h : G₁), φ (g * h) = φ g * φ h
 
-  attribute homomorphism.φ [coercion]
-  abbreviation group_fun [unfold 3] := @homomorphism.φ
-  abbreviation respect_mul := @homomorphism.p
-  infix ` →g `:55 := homomorphism
+  section
+  variables {G G₁ G₂ G₃ : Type} {g h : G₁} (ψ : G₂ → G₃) {φ₁ φ₂ : G₁ → G₂} (φ : G₁ → G₂)
+            [group G] [group G₁] [group G₂] [group G₃]
+            [is_homomorphism ψ] [is_homomorphism φ₁] [is_homomorphism φ₂] [is_homomorphism φ]
 
-  variables {G G₁ G₂ G₃ : Group} {g h : G₁} {ψ : G₂ →g G₃} {φ φ' : G₁ →g G₂}
+  definition respect_mul /- φ -/ : Π(g h : G₁), φ (g * h) = φ g * φ h :=
+  by assumption
 
-  theorem respect_one (φ : G₁ →g G₂) : φ 1 = 1 :=
+  theorem respect_one /- φ -/ : φ 1 = 1 :=
   mul.right_cancel
     (calc
-      φ 1 * φ 1 = φ (1 * 1) : respect_mul
+      φ 1 * φ 1 = φ (1 * 1) : respect_mul φ
             ... = φ 1 : ap φ !one_mul
             ... = 1 * φ 1 : one_mul)
 
-  theorem respect_inv (φ : G₁ →g G₂) (g : G₁) : φ g⁻¹ = (φ g)⁻¹ :=
+  theorem respect_inv /- φ -/ (g : G₁) : φ g⁻¹ = (φ g)⁻¹ :=
   eq_inv_of_mul_eq_one (!respect_mul⁻¹ ⬝ ap φ !mul.left_inv ⬝ !respect_one)
 
-  definition is_set_homomorphism [instance] (G₁ G₂ : Group) : is_set (homomorphism G₁ G₂) :=
+  definition is_embedding_homomorphism /- φ -/ (H : Π{g}, φ g = 1 → g = 1) : is_embedding φ :=
+  begin
+    apply function.is_embedding_of_is_injective,
+    intro g g' p,
+    apply eq_of_mul_inv_eq_one,
+    apply H,
+    refine !respect_mul ⬝ _,
+    rewrite [respect_inv φ, p],
+    apply mul.right_inv
+  end
+
+  definition is_homomorphism_compose {ψ : G₂ → G₃} {φ : G₁ → G₂}
+    (H1 : is_homomorphism ψ) (H2 : is_homomorphism φ) : is_homomorphism (ψ ∘ φ) :=
+  λg h, ap ψ !respect_mul ⬝ !respect_mul
+
+  definition is_homomorphism_id (G : Type) [group G] : is_homomorphism (@id G) :=
+  λg h, idp
+
+  end
+
+  structure homomorphism (G₁ G₂ : Group) : Type :=
+    (φ : G₁ → G₂)
+    (p : is_homomorphism φ)
+
+  infix ` →g `:55 := homomorphism
+
+  definition group_fun [unfold 3] [coercion] := @homomorphism.φ
+  definition homomorphism.struct [instance] [priority 2000] {G₁ G₂ : Group} (φ : G₁ →g G₂)
+    : is_homomorphism φ :=
+  homomorphism.p φ
+
+  variables {G G₁ G₂ G₃ : Group} {g h : G₁} {ψ : G₂ →g G₃} {φ₁ φ₂ : G₁ →g G₂} (φ : G₁ →g G₂)
+
+  definition to_respect_mul /- φ -/ (g h : G₁) : φ (g * h) = φ g * φ h :=
+  respect_mul φ g h
+
+  theorem to_respect_one /- φ -/ : φ 1 = 1 :=
+  respect_one φ
+
+  theorem to_respect_inv /- φ -/ (g : G₁) : φ g⁻¹ = (φ g)⁻¹ :=
+  respect_inv φ g
+
+  definition to_is_embedding_homomorphism /- φ -/ (H : Π{g}, φ g = 1 → g = 1) : is_embedding φ :=
+  is_embedding_homomorphism φ @H
+
+  definition is_set_homomorphism [instance] (G₁ G₂ : Group) : is_set (G₁ →g G₂) :=
   begin
     assert H : G₁ →g G₂ ≃ Σ(f : G₁ → G₂), Π(g₁ g₂ : G₁), f (g₁ * g₂) = f g₁ * f g₂,
     { fapply equiv.MK,
@@ -68,23 +114,23 @@ namespace group
     apply is_trunc_equiv_closed_rev, exact H
   end
 
-  definition pmap_of_homomorphism [constructor] (φ : G₁ →g G₂)
-    : pType_of_Group G₁ →* pType_of_Group G₂ :=
-  pmap.mk φ !respect_one
+  local attribute group_pType_of_Group pointed.mk' [reducible]
+  definition pmap_of_homomorphism [constructor] /- φ -/ : pType_of_Group G₁ →* pType_of_Group G₂ :=
+  pmap.mk φ (respect_one φ)
 
-  definition homomorphism_eq (p : group_fun φ ~ group_fun φ') : φ = φ' :=
+  definition homomorphism_eq (p : group_fun φ₁ ~ group_fun φ₂) : φ₁ = φ₂ :=
   begin
-    induction φ with φ q, induction φ' with φ' q', esimp at p, induction p,
-    exact ap (homomorphism.mk φ) !is_prop.elim
+    induction φ₁ with φ₁ q₁, induction φ₂ with φ₂ q₂, esimp at p, induction p,
+    exact ap (homomorphism.mk φ₁) !is_prop.elim
   end
 
   /- categorical structure of groups + homomorphisms -/
 
   definition homomorphism_compose [constructor] (ψ : G₂ →g G₃) (φ : G₁ →g G₂) : G₁ →g G₃ :=
-  homomorphism.mk (ψ ∘ φ) (λg h, ap ψ !respect_mul ⬝ !respect_mul)
+  homomorphism.mk (ψ ∘ φ) (is_homomorphism_compose _ _)
 
   definition homomorphism_id [constructor] (G : Group) : G →g G :=
-  homomorphism.mk id (λg h, idp)
+  homomorphism.mk (@id G) (is_homomorphism_id G)
 
   infixr ` ∘g `:75 := homomorphism_compose
   notation 1       := homomorphism_id _
@@ -104,7 +150,7 @@ namespace group
   homomorphism.mk φ⁻¹
     abstract begin
     intro g₁ g₂, apply eq_of_fn_eq_fn' φ,
-    rewrite [respect_mul, +right_inv φ]
+    rewrite [respect_mul φ, +right_inv φ]
     end end
 
   definition isomorphism.refl [refl] [constructor] (G : Group) : G ≃g G :=
diff --git a/group_theory/constructions.hlean b/group_theory/constructions.hlean
index 3ef8a15..2867b8a 100644
--- a/group_theory/constructions.hlean
+++ b/group_theory/constructions.hlean
@@ -416,10 +416,10 @@ namespace group
     { intro f, apply eq_of_homotopy, intro x, esimp, unfold [foldl], apply one_mul},
     { intro φ, apply homomorphism_eq, refine set_quotient.rec_prop _, intro l, esimp,
       induction l with s l IH,
-      { esimp [foldl], exact !respect_one⁻¹},
+      { esimp [foldl], exact (respect_one φ)⁻¹},
       { rewrite [foldl_cons, fgh_helper_mul],
         refine _ ⬝ (respect_mul φ (class_of [s]) (class_of l))⁻¹,
-        rewrite [IH], induction s: rewrite [▸*, one_mul], rewrite [-respect_inv]}}
+        rewrite [IH], induction s: rewrite [▸*, one_mul], rewrite [-respect_inv φ]}}
   end
 
   /- Free Commutative Group of a set -/
@@ -589,11 +589,11 @@ namespace group
     { intro f, apply eq_of_homotopy, intro x, esimp, unfold [foldl], apply one_mul},
     { intro φ, apply homomorphism_eq, refine set_quotient.rec_prop _, intro l, esimp,
       induction l with s l IH,
-      { esimp [foldl], exact !respect_one⁻¹},
+      { esimp [foldl], symmetry, exact to_respect_one φ},
       { rewrite [foldl_cons, fgh_helper_mul],
-        refine _ ⬝ (respect_mul φ (class_of [s]) (class_of l))⁻¹,
+        refine _ ⬝ (to_respect_mul φ (class_of [s]) (class_of l))⁻¹,
         rewrite [▸*,IH], induction s: rewrite [▸*, one_mul], apply ap (λx, x * _),
-        exact !respect_inv⁻¹}}
+        exact !to_respect_inv⁻¹}}
   end
 
   /- Free Commutative Group of a set -/
@@ -631,7 +631,7 @@ namespace group
   begin
     esimp at *,
     exact calc
-      φ (g * h) = (φ g) * (φ h) : respect_mul
+      φ (g * h) = (φ g) * (φ h) : to_respect_mul
             ... = 1 * (φ h)     : H₁
             ... = 1 * 1         : H₂
             ... = 1             : one_mul
@@ -641,12 +641,12 @@ namespace group
   begin
     esimp at *,
     exact calc
-      φ g⁻¹ = (φ g)⁻¹ : respect_inv
+      φ g⁻¹ = (φ g)⁻¹ : to_respect_inv
         ... = 1⁻¹     : H
         ... = 1       : one_inv
   end
 
-  definition kernel_subgroup [constructor] (φ : G₁ →g G₂) : subgroup_rel G₁ :=
+  definition subgroup_kernel [constructor] (φ : G₁ →g G₂) : subgroup_rel G₁ :=
   ⦃ subgroup_rel,
     R := kernel φ,
     Rone := respect_one φ,
@@ -654,24 +654,24 @@ namespace group
     Rinv := kernel_inv φ
   ⦄
 
-  theorem kernel_subgroup_isnormal (φ : G₁ →g G₂) (g : G₁) (h : G₁)
+  theorem is_normal_subgroup_kernel (φ : G₁ →g G₂) (g : G₁) (h : G₁)
     : kernel φ g → kernel φ (h * g * h⁻¹) :=
   begin
     esimp at *,
     intro p,
     exact calc
-      φ (h * g * h⁻¹) = (φ (h * g)) * φ (h⁻¹)   : respect_mul
-                  ... = (φ h) * (φ g) * (φ h⁻¹) : respect_mul
+      φ (h * g * h⁻¹) = (φ (h * g)) * φ (h⁻¹)   : to_respect_mul
+                  ... = (φ h) * (φ g) * (φ h⁻¹) : to_respect_mul
                   ... = (φ h) * 1 * (φ h⁻¹)     : p
                   ... = (φ h) * (φ h⁻¹)         : mul_one
-                  ... = (φ h) * (φ h)⁻¹         : respect_inv
+                  ... = (φ h) * (φ h)⁻¹         : to_respect_inv
                   ... = 1                       : mul.right_inv
   end
 
-  definition kernel_normal_subgroup [constructor] (φ : G₁ →g G₂) : normal_subgroup_rel G₁ :=
+  definition normal_subgroup_kernel [constructor] (φ : G₁ →g G₂) : normal_subgroup_rel G₁ :=
   ⦃ normal_subgroup_rel,
-    kernel_subgroup φ,
-    is_normal := kernel_subgroup_isnormal φ
+    subgroup_kernel φ,
+    is_normal := is_normal_subgroup_kernel φ
   ⦄
 
   end kernels
diff --git a/homotopy/LES_applications.hlean b/homotopy/LES_applications.hlean
new file mode 100644
index 0000000..61e2a2b
--- /dev/null
+++ b/homotopy/LES_applications.hlean
@@ -0,0 +1,17 @@
+import .LES_of_homotopy_groups homotopy.connectedness homotopy.homotopy_group
+
+open eq is_trunc pointed homotopy is_equiv fiber equiv trunc nat
+
+namespace is_conn
+
+  theorem is_contr_HG_fiber_of_is_connected {A B : Type*} (n k : ℕ) (f : A →* B)
+    [H : is_conn_map n f] (H2 : k ≤ n) : is_contr (π[k] (pfiber f)) :=
+  @(trivial_homotopy_group_of_is_conn (pfiber f) H2) (H pt)
+
+  theorem is_equiv_π_of_is_connected {A B : Type*} (n k : ℕ) (f : A →* B)
+    [H : is_conn_map n f] (H : k ≤ n) : is_equiv (π→[k] f) :=
+  begin
+    exact sorry
+  end
+
+end is_conn
diff --git a/homotopy/LES_of_homotopy_groups.hlean b/homotopy/LES_of_homotopy_groups.hlean
index 9e9f28c..9559b02 100644
--- a/homotopy/LES_of_homotopy_groups.hlean
+++ b/homotopy/LES_of_homotopy_groups.hlean
@@ -35,12 +35,15 @@ f'(n+6) := Ω²(f'(n))
 
 We can show that these sequences are equivalent, hence the sequence (X',f') is an exact
 sequence. Now we get the fiber sequence by taking the set-truncation of this sequence.
-
 -/
 
 import .chain_complex algebra.homotopy_group
 
-open eq pointed sigma fiber equiv is_equiv sigma.ops is_trunc equiv.ops nat trunc algebra
+open eq pointed sigma fiber equiv is_equiv sigma.ops is_trunc equiv.ops nat trunc algebra function
+
+/--------------
+    PART 1
+ --------------/
 
 namespace chain_complex
 
@@ -64,7 +67,7 @@ namespace chain_complex
   (fiber_sequence_helpern ⟨X, Y, f⟩ n).2.2
 
   /- Definition 8.4.3 -/
-  definition fiber_sequence : left_type_chain_complex.{u} :=
+  definition fiber_sequence : type_chain_complex.{0 u} +ℕ :=
   begin
     fconstructor,
     { exact fiber_sequence_carrier f},
@@ -74,7 +77,7 @@ namespace chain_complex
       { exact point_eq x}}
   end
 
-  definition is_exact_fiber_sequence : is_exact_lt (fiber_sequence f) :=
+  definition is_exact_fiber_sequence : is_exact_t (fiber_sequence f) :=
   λn x p, fiber.mk (fiber.mk x p) rfl
 
   /- (generalization of) Lemma 8.4.4(i)(ii) -/
@@ -221,6 +224,10 @@ namespace chain_complex
   definition boundary_map : Ω Y →* pfiber f :=
   fiber_sequence_fun f 2 ∘* (fiber_sequence_carrier_pequiv f 0)⁻¹ᵉ*
 
+/--------------
+    PART 2
+ --------------/
+
   /- Now we are ready to define the long exact sequence of homotopy groups.
      First we define its carrier -/
   definition homotopy_groups : ℕ → Type*
@@ -231,7 +238,7 @@ namespace chain_complex
 
   definition homotopy_groups_add3 [unfold_full] :
     homotopy_groups f (n+3) = Ω (homotopy_groups f n) :=
-  proof idp qed
+  by reflexivity
 
   definition homotopy_groups_mul3
     : Πn, homotopy_groups f (3 * n) = Ω[n] Y :> Type*
@@ -240,12 +247,12 @@ namespace chain_complex
 
   definition homotopy_groups_mul3add1
     : Πn, homotopy_groups f (3 * n + 1) = Ω[n] X :> Type*
-  | 0     := proof rfl qed
+  | 0     := by reflexivity
   | (k+1) := proof ap (λX, Ω X) (homotopy_groups_mul3add1 k) qed
 
   definition homotopy_groups_mul3add2
     : Πn, homotopy_groups f (3 * n + 2) = Ω[n] (pfiber f) :> Type*
-  | 0     := proof rfl qed
+  | 0     := by reflexivity
   | (k+1) := proof ap (λX, Ω X) (homotopy_groups_mul3add2 k) qed
 
   /- The maps between the homotopy groups -/
@@ -278,12 +285,12 @@ namespace chain_complex
 
   theorem homotopy_groups_fun_eq
     : Π(n : ℕ), homotopy_groups_fun f n ~* homotopy_groups_fun' f n
-  | 0     := proof phomotopy.rfl qed
-  | 1     := proof phomotopy.rfl qed
-  | 2     := proof phomotopy.rfl qed
-  | 3     := proof phomotopy.rfl qed
-  | 4     := proof phomotopy.rfl qed
-  | 5     := proof phomotopy.rfl qed
+  | 0     := by reflexivity
+  | 1     := by reflexivity
+  | 2     := by reflexivity
+  | 3     := by reflexivity
+  | 4     := by reflexivity
+  | 5     := by reflexivity
   | (k+6) :=
     begin
       rewrite [homotopy_groups_fun_add6 f k],
@@ -301,11 +308,18 @@ namespace chain_complex
         { reflexivity}}
     end
 
+  definition homotopy_groups_fun_add3 :
+    homotopy_groups_fun f (n + 3) ~* ap1 (homotopy_groups_fun f n)  ∘* pinverse :=
+  begin
+    refine homotopy_groups_fun_eq f (n+3) ⬝* _,
+    exact pwhisker_right _ (ap1_phomotopy (homotopy_groups_fun_eq f n)⁻¹*),
+  end
+
   definition fiber_sequence_pequiv_homotopy_groups :
     Πn, fiber_sequence_carrier f n ≃* homotopy_groups f n
-  | 0     := proof pequiv.rfl qed
-  | 1     := proof pequiv.rfl qed
-  | 2     := proof pequiv.rfl qed
+  | 0     := by reflexivity
+  | 1     := by reflexivity
+  | 2     := by reflexivity
   | (k+3) :=
     begin
       refine fiber_sequence_carrier_pequiv f k ⬝e* _,
@@ -368,22 +382,35 @@ namespace chain_complex
     exact (homotopy_groups_fun_eq f n _)⁻¹
   end
 
+  definition type_LES_of_homotopy_groups [constructor] : type_chain_complex +ℕ :=
+  transfer_type_chain_complex
+    (fiber_sequence f)
+    (homotopy_groups_fun f)
+    (fiber_sequence_pequiv_homotopy_groups f)
+    (fiber_sequence_phomotopy_homotopy_groups f)
+
+  definition is_exact_type_LES_of_homotopy_groups : is_exact_t (type_LES_of_homotopy_groups f) :=
+  begin
+    intro n,
+    apply is_exact_at_t_transfer,
+    apply is_exact_fiber_sequence
+  end
+
   /- the long exact sequence of homotopy groups -/
-  definition LES_of_homotopy_groups [constructor] : left_chain_complex :=
-  trunc_left_chain_complex
-    (transfer_left_type_chain_complex
+  definition LES_of_homotopy_groups [constructor] : chain_complex +ℕ :=
+  trunc_chain_complex
+    (transfer_type_chain_complex
       (fiber_sequence f)
       (homotopy_groups_fun f)
       (fiber_sequence_pequiv_homotopy_groups f)
       (fiber_sequence_phomotopy_homotopy_groups f))
 
   /- the fiber sequence is exact -/
-  definition is_exact_LES_of_homotopy_groups : is_exact_l (LES_of_homotopy_groups f) :=
+  definition is_exact_LES_of_homotopy_groups : is_exact (LES_of_homotopy_groups f) :=
   begin
     intro n,
-    apply is_exact_at_l_trunc,
-    apply is_exact_at_lt_transfer,
-    apply is_exact_fiber_sequence
+    apply is_exact_at_trunc,
+    apply is_exact_type_LES_of_homotopy_groups
   end
 
   /- for a numeral, the carrier of the fiber sequence is definitionally what we want
@@ -396,30 +423,32 @@ namespace chain_complex
      (as pointed function). All these functions have at most one "pinverse" in them, and these
      inverses are inside the π→*[2*k].
   -/
-  example : lcc_to_fn (LES_of_homotopy_groups f)  6 = π→*[2] f
+  example : cc_to_fn (LES_of_homotopy_groups f)  6 = π→*[2] f
     :> (_ →* _) := by reflexivity
-  example : lcc_to_fn (LES_of_homotopy_groups f)  7 = π→*[2] (ppoint f)
+  example : cc_to_fn (LES_of_homotopy_groups f)  7 = π→*[2] (ppoint f)
     :> (_ →* _) := by reflexivity
-  example : lcc_to_fn (LES_of_homotopy_groups f)  8 = π→*[2] (boundary_map f)
+  example : cc_to_fn (LES_of_homotopy_groups f)  8 = π→*[2] (boundary_map f)
     :> (_ →* _) := by reflexivity
-  example : lcc_to_fn (LES_of_homotopy_groups f)  9 = π→*[2] (ap1 f ∘* pinverse)
+  example : cc_to_fn (LES_of_homotopy_groups f)  9 = π→*[2] (ap1 f ∘* pinverse)
     :> (_ →* _) := by reflexivity
-  example : lcc_to_fn (LES_of_homotopy_groups f) 10 = π→*[2] (ap1 (ppoint f) ∘* pinverse)
+  example : cc_to_fn (LES_of_homotopy_groups f) 10 = π→*[2] (ap1 (ppoint f) ∘* pinverse)
     :> (_ →* _) := by reflexivity
-  example : lcc_to_fn (LES_of_homotopy_groups f) 11 = π→*[2] (ap1 (boundary_map f) ∘* pinverse)
+  example : cc_to_fn (LES_of_homotopy_groups f) 11 = π→*[2] (ap1 (boundary_map f) ∘* pinverse)
     :> (_ →* _) := by reflexivity
-  example : lcc_to_fn (LES_of_homotopy_groups f) 12 = π→*[4] f
+  example : cc_to_fn (LES_of_homotopy_groups f) 12 = π→*[4] f
     :> (_ →* _) := by reflexivity
 
   /- the carrier of the fiber sequence is what we want for natural numbers of the form
      3n, 3n+1 and 3n+2 -/
-  definition LES_of_homotopy_groups_mul3 (n : ℕ) : LES_of_homotopy_groups f (3 * n) = π*[n] Y :> Set* :=
+  definition LES_of_homotopy_groups_mul3 (n : ℕ)
+    : LES_of_homotopy_groups f (3 * n) = π*[n] Y :> Set* :=
   begin
    apply ptrunctype_eq_of_pType_eq,
    exact ap (ptrunc 0) (homotopy_groups_mul3 f n)
   end
 
-  definition LES_of_homotopy_groups_mul3add1 (n : ℕ) : LES_of_homotopy_groups f (3 * n + 1) = π*[n] X :> Set* :=
+  definition LES_of_homotopy_groups_mul3add1 (n : ℕ)
+    : LES_of_homotopy_groups f (3 * n + 1) = π*[n] X :> Set* :=
   begin
    apply ptrunctype_eq_of_pType_eq,
    exact ap (ptrunc 0) (homotopy_groups_mul3add1 f n)
@@ -432,12 +461,530 @@ namespace chain_complex
    exact ap (ptrunc 0) (homotopy_groups_mul3add2 f n)
   end
 
+  definition LES_of_homotopy_groups_mul3' (n : ℕ)
+    : LES_of_homotopy_groups f (3 * n) = π*[n] Y :> Type :=
+  begin
+   exact ap (ptrunc 0) (homotopy_groups_mul3 f n)
+  end
+
+  definition LES_of_homotopy_groups_mul3add1' (n : ℕ)
+    : LES_of_homotopy_groups f (3 * n + 1) = π*[n] X :> Type :=
+  begin
+   exact ap (ptrunc 0) (homotopy_groups_mul3add1 f n)
+  end
+
+  definition LES_of_homotopy_groups_mul3add2' (n : ℕ)
+    : LES_of_homotopy_groups f (3 * n + 2) = π*[n] (pfiber f) :> Type :=
+  begin
+   exact ap (ptrunc 0) (homotopy_groups_mul3add2 f n)
+  end
+
   definition group_LES_of_homotopy_groups (n : ℕ) : group (LES_of_homotopy_groups f (n + 3)) :=
   group_homotopy_group 0 (homotopy_groups f n)
 
   definition comm_group_LES_of_homotopy_groups (n : ℕ) : comm_group (LES_of_homotopy_groups f (n + 6)) :=
   comm_group_homotopy_group 0 (homotopy_groups f n)
 
-  -- TODO: the pointed maps are what we want for 3n, 3n+1 and 3n+2
-  -- TODO: they are group homomorphisms for n+3
+end chain_complex
+
+open group prod succ_str fin
+
+/--------------
+    PART 3
+ --------------/
+
+namespace chain_complex
+
+  --TODO: move
+  definition tr_mul_tr {A : Type*} (n : ℕ) (p q : Ω[n + 1] A) :
+    tr p *[πg[n+1] A] tr q = tr (p ⬝ q) :=
+  by reflexivity
+
+  definition is_homomorphism_cast_loop_space_succ_eq_in {A : Type*} (n : ℕ) :
+    is_homomorphism
+      (cast (ap (trunc 0 ∘ pointed.carrier) (loop_space_succ_eq_in A (succ n)))
+        : πg[n+1+1] A → πg[n+1] Ω A) :=
+  begin
+    intro g h, induction g with g, induction h with h,
+    xrewrite [tr_mul_tr, - + fn_cast_eq_cast_fn _ (λn, tr), tr_mul_tr, ↑cast, -tr_compose,
+              loop_space_succ_eq_in_concat, - + tr_compose],
+  end
+
+  definition is_homomorphism_inverse (A : Type*) (n : ℕ)
+    : is_homomorphism (λp, p⁻¹ : πag[n+2] A → πag[n+2] A) :=
+  begin
+    intro g h, rewrite mul.comm,
+    induction g with g, induction h with h,
+    exact ap tr !con_inv
+  end
+
+  section
+  universe variable u
+  parameters {X Y : pType.{u}} (f : X →* Y)
+
+  definition homotopy_groups2 [reducible] : +6ℕ → Type*
+  | (n, fin.mk 0 H) := Ω[2*n] Y
+  | (n, fin.mk 1 H) := Ω[2*n] X
+  | (n, fin.mk 2 H) := Ω[2*n] (pfiber f)
+  | (n, fin.mk 3 H) := Ω[2*n + 1] Y
+  | (n, fin.mk 4 H) := Ω[2*n + 1] X
+  | (n, fin.mk k H) := Ω[2*n + 1] (pfiber f)
+
+  definition homotopy_groups2_add1 (n : ℕ) : Π(x : fin (succ 5)),
+    homotopy_groups2 (n+1, x) = Ω Ω(homotopy_groups2 (n, x))
+  | (fin.mk 0 H) := by reflexivity
+  | (fin.mk 1 H) := by reflexivity
+  | (fin.mk 2 H) := by reflexivity
+  | (fin.mk 3 H) := by reflexivity
+  | (fin.mk 4 H) := by reflexivity
+  | (fin.mk 5 H) := by reflexivity
+  | (fin.mk (k+6) H) := begin exfalso, apply lt_le_antisymm H, apply le_add_left end
+
+  definition homotopy_groups_fun2 : Π(n : +6ℕ), homotopy_groups2 (S n) →* homotopy_groups2 n
+  | (n, fin.mk 0 H) := proof Ω→[2*n] f qed
+  | (n, fin.mk 1 H) := proof Ω→[2*n] (ppoint f) qed
+  | (n, fin.mk 2 H) :=
+    proof Ω→[2*n] (boundary_map f) ∘* pcast (loop_space_succ_eq_in Y (2*n)) qed
+  | (n, fin.mk 3 H) := proof Ω→[2*n + 1] f ∘* pinverse qed
+  | (n, fin.mk 4 H) := proof Ω→[2*n + 1] (ppoint f) ∘* pinverse qed
+  | (n, fin.mk 5 H) :=
+    proof (Ω→[2*n + 1] (boundary_map f) ∘* pinverse) ∘* pcast (loop_space_succ_eq_in Y (2*n+1)) qed
+  | (n, fin.mk (k+6) H) := begin exfalso, apply lt_le_antisymm H, apply le_add_left end
+
+  definition homotopy_groups_fun2_add1_0 (n : ℕ) (H : 0 < succ 5)
+    : homotopy_groups_fun2 (n+1, fin.mk 0 H) ~*
+      cast proof idp qed ap1 (ap1 (homotopy_groups_fun2 (n, fin.mk 0 H))) :=
+  by reflexivity
+
+  definition homotopy_groups_fun2_add1_1 (n : ℕ) (H : 1 < succ 5)
+    : homotopy_groups_fun2 (n+1, fin.mk 1 H) ~*
+      cast proof idp qed ap1 (ap1 (homotopy_groups_fun2 (n, fin.mk 1 H))) :=
+  by reflexivity
+
+  definition homotopy_groups_fun2_add1_2 (n : ℕ) (H : 2 < succ 5)
+    : homotopy_groups_fun2 (n+1, fin.mk 2 H) ~*
+      cast proof idp qed ap1 (ap1 (homotopy_groups_fun2 (n, fin.mk 2 H))) :=
+  begin
+    esimp, refine _ ⬝* (ap1_phomotopy !ap1_compose)⁻¹*, refine _ ⬝* !ap1_compose⁻¹*,
+    apply pwhisker_left,
+    refine !pcast_ap_loop_space ⬝* ap1_phomotopy !pcast_ap_loop_space,
+  end
+
+  definition homotopy_groups_fun2_add1_3 (n : ℕ) (H : 3 < succ 5)
+    : homotopy_groups_fun2 (n+1, fin.mk 3 H) ~*
+      cast proof idp qed ap1 (ap1 (homotopy_groups_fun2 (n, fin.mk 3 H))) :=
+  begin
+    esimp, refine _ ⬝* (ap1_phomotopy !ap1_compose)⁻¹*, refine _ ⬝* !ap1_compose⁻¹*,
+    apply pwhisker_left,
+    exact ap1_pinverse⁻¹* ⬝* ap1_phomotopy !ap1_pinverse⁻¹*
+  end
+
+  definition homotopy_groups_fun2_add1_4 (n : ℕ) (H : 4 < succ 5)
+    : homotopy_groups_fun2 (n+1, fin.mk 4 H) ~*
+      cast proof idp qed ap1 (ap1 (homotopy_groups_fun2 (n, fin.mk 4 H))) :=
+  begin
+    esimp, refine _ ⬝* (ap1_phomotopy !ap1_compose)⁻¹*, refine _ ⬝* !ap1_compose⁻¹*,
+    apply pwhisker_left,
+    exact ap1_pinverse⁻¹* ⬝* ap1_phomotopy !ap1_pinverse⁻¹*
+  end
+
+  definition homotopy_groups_fun2_add1_5 (n : ℕ) (H : 5 < succ 5)
+    : homotopy_groups_fun2 (n+1, fin.mk 5 H) ~*
+      cast proof idp qed ap1 (ap1 (homotopy_groups_fun2 (n, fin.mk 5 H))) :=
+  begin
+    esimp, refine _ ⬝* (ap1_phomotopy !ap1_compose)⁻¹*, refine _ ⬝* !ap1_compose⁻¹*,
+    apply pconcat2,
+    { esimp, refine _ ⬝* (ap1_phomotopy !ap1_compose)⁻¹*, refine _ ⬝* !ap1_compose⁻¹*,
+      apply pwhisker_left,
+      exact ap1_pinverse⁻¹* ⬝* ap1_phomotopy !ap1_pinverse⁻¹*},
+    { refine !pcast_ap_loop_space ⬝* ap1_phomotopy !pcast_ap_loop_space}
+  end
+
+  definition nat_of_str [unfold 2] [reducible] {n : ℕ} : ℕ × fin (succ n) → ℕ :=
+  λx, succ n * pr1 x + val (pr2 x)
+
+  definition str_of_nat {n : ℕ} : ℕ → ℕ × fin (succ n) :=
+  λm, (m / (succ n), mk_mod n m)
+
+  definition nat_of_str_6S [unfold 2] [reducible]
+    : Π(x : stratified +ℕ 5), nat_of_str x + 1 = nat_of_str (@S (stratified +ℕ 5) x)
+  | (n, fin.mk 0 H) := by reflexivity
+  | (n, fin.mk 1 H) := by reflexivity
+  | (n, fin.mk 2 H) := by reflexivity
+  | (n, fin.mk 3 H) := by reflexivity
+  | (n, fin.mk 4 H) := by reflexivity
+  | (n, fin.mk 5 H) := by reflexivity
+  | (n, fin.mk (k+6) H) := begin exfalso, apply lt_le_antisymm H, apply le_add_left end
+
+  definition fin_prod_nat_equiv_nat [constructor] (n : ℕ) : ℕ × fin (succ n) ≃ ℕ :=
+  equiv.MK nat_of_str str_of_nat
+    abstract begin
+      intro m, unfold [nat_of_str, str_of_nat, mk_mod],
+      refine _ ⬝ (eq_div_mul_add_mod m (succ n))⁻¹,
+      rewrite [mul.comm]
+    end end
+    abstract begin
+      intro x, cases x with m k,
+      cases k with k H,
+      apply prod_eq: esimp [str_of_nat],
+      { rewrite [add.comm, add_mul_div_self_left _ _ (!zero_lt_succ),
+                 div_eq_zero_of_lt H, zero_add]},
+      { apply eq_of_veq, esimp [mk_mod],
+        rewrite [add.comm, add_mul_mod_self_left, mod_eq_of_lt H]}
+    end end
+
+  /-
+    note: in the following theorem the (n+1) case is 6 times the same,
+    so maybe this can be simplified
+  -/
+  definition homotopy_groups2_pequiv' : Π(n : ℕ) (x : fin (nat.succ 5)),
+    homotopy_groups f (nat_of_str (n, x)) ≃* homotopy_groups2 (n, x)
+  |  0    (fin.mk 0 H)     := by reflexivity
+  |  0    (fin.mk 1 H)     := by reflexivity
+  |  0    (fin.mk 2 H)     := by reflexivity
+  |  0    (fin.mk 3 H)     := by reflexivity
+  |  0    (fin.mk 4 H)     := by reflexivity
+  |  0    (fin.mk 5 H)     := by reflexivity
+  | (n+1) (fin.mk 0 H)     :=
+    begin
+      -- uncomment the next two lines to have prettier subgoals
+      -- esimp, replace (succ 5 * (n + 1) + 0) with (6*n+3+3),
+      -- rewrite [+homotopy_groups_add3, homotopy_groups2_add1],
+      apply loop_space_pequiv, apply loop_space_pequiv,
+      rexact homotopy_groups2_pequiv' n (fin.mk 0 H)
+    end
+  | (n+1) (fin.mk 1 H)     :=
+    begin
+      apply loop_space_pequiv, apply loop_space_pequiv,
+      rexact homotopy_groups2_pequiv' n (fin.mk 1 H)
+    end
+  | (n+1) (fin.mk 2 H)     :=
+    begin
+      apply loop_space_pequiv, apply loop_space_pequiv,
+      rexact homotopy_groups2_pequiv' n (fin.mk 2 H)
+    end
+  | (n+1) (fin.mk 3 H)     :=
+    begin
+      apply loop_space_pequiv, apply loop_space_pequiv,
+      rexact homotopy_groups2_pequiv' n (fin.mk 3 H)
+    end
+  | (n+1) (fin.mk 4 H)     :=
+    begin
+      apply loop_space_pequiv, apply loop_space_pequiv,
+      rexact homotopy_groups2_pequiv' n (fin.mk 4 H)
+    end
+  | (n+1) (fin.mk 5 H)     :=
+    begin
+      apply loop_space_pequiv, apply loop_space_pequiv,
+      rexact homotopy_groups2_pequiv' n (fin.mk 5 H)
+    end
+  | n     (fin.mk (k+6) H) := begin exfalso, apply lt_le_antisymm H, apply le_add_left end
+
+  definition homotopy_groups2_pequiv : Π(x : +6ℕ),
+    homotopy_groups f (nat_of_str x) ≃* homotopy_groups2 x
+  | (n, x) := homotopy_groups2_pequiv' n x
+
+  /- all cases where n>0 are basically the same -/
+  definition homotopy_groups_fun2_phomotopy (x : +6ℕ) :
+    homotopy_groups2_pequiv x ∘* homotopy_groups_fun f (nat_of_str x) ~*
+      (homotopy_groups_fun2 x ∘* homotopy_groups2_pequiv (S x))
+    ∘* pcast (ap (homotopy_groups f) (nat_of_str_6S x)) :=
+  begin
+    cases x with n x, cases x with k H,
+    cases k with k, rotate 1, cases k with k, rotate 1, cases k with k, rotate 1,
+    cases k with k, rotate 1, cases k with k, rotate 1, cases k with k, rotate 2,
+    { /-k=0-/
+      induction n with n IH,
+      { refine !pid_comp ⬝* _ ⬝* !comp_pid⁻¹* ⬝* !comp_pid⁻¹*,
+        reflexivity},
+      { refine _ ⬝* !comp_pid⁻¹*,
+        refine _ ⬝* pwhisker_right _ (!homotopy_groups_fun2_add1_0)⁻¹*,
+        refine !ap1_compose⁻¹* ⬝* _ ⬝* !ap1_compose, apply ap1_phomotopy,
+        refine !ap1_compose⁻¹* ⬝* _ ⬝* !ap1_compose, apply ap1_phomotopy,
+        exact IH ⬝* !comp_pid}},
+    { /-k=1-/
+      induction n with n IH,
+      { refine !pid_comp ⬝* _ ⬝* !comp_pid⁻¹* ⬝* !comp_pid⁻¹*,
+        reflexivity},
+      { refine _ ⬝* !comp_pid⁻¹*,
+        refine _ ⬝* pwhisker_right _ (!homotopy_groups_fun2_add1_1)⁻¹*,
+        refine !ap1_compose⁻¹* ⬝* _ ⬝* !ap1_compose, apply ap1_phomotopy,
+        refine !ap1_compose⁻¹* ⬝* _ ⬝* !ap1_compose, apply ap1_phomotopy,
+        exact IH ⬝* !comp_pid}},
+    { /-k=2-/
+      induction n with n IH,
+      { refine !pid_comp ⬝* _ ⬝* !comp_pid⁻¹* ⬝* !comp_pid⁻¹*,
+        refine _ ⬝* !comp_pid⁻¹*,
+        reflexivity},
+      { refine _ ⬝* !comp_pid⁻¹*,
+        refine _ ⬝* pwhisker_right _ (!homotopy_groups_fun2_add1_2)⁻¹*,
+        refine !ap1_compose⁻¹* ⬝* _ ⬝* !ap1_compose, apply ap1_phomotopy,
+        refine !ap1_compose⁻¹* ⬝* _ ⬝* !ap1_compose, apply ap1_phomotopy,
+        exact IH ⬝* !comp_pid}},
+    { /-k=3-/
+      induction n with n IH,
+      { refine !pid_comp ⬝* _ ⬝* !comp_pid⁻¹* ⬝* !comp_pid⁻¹*,
+        reflexivity},
+      { refine _ ⬝* !comp_pid⁻¹*,
+        refine _ ⬝* pwhisker_right _ (!homotopy_groups_fun2_add1_3)⁻¹*,
+        refine !ap1_compose⁻¹* ⬝* _ ⬝* !ap1_compose, apply ap1_phomotopy,
+        refine !ap1_compose⁻¹* ⬝* _ ⬝* !ap1_compose, apply ap1_phomotopy,
+        exact IH ⬝* !comp_pid}},
+    { /-k=4-/
+      induction n with n IH,
+      { refine !pid_comp ⬝* _ ⬝* !comp_pid⁻¹* ⬝* !comp_pid⁻¹*,
+        reflexivity},
+      { refine _ ⬝* !comp_pid⁻¹*,
+        refine _ ⬝* pwhisker_right _ (!homotopy_groups_fun2_add1_4)⁻¹*,
+        refine !ap1_compose⁻¹* ⬝* _ ⬝* !ap1_compose, apply ap1_phomotopy,
+        refine !ap1_compose⁻¹* ⬝* _ ⬝* !ap1_compose, apply ap1_phomotopy,
+        exact IH ⬝* !comp_pid}},
+    { /-k=5-/
+      induction n with n IH,
+      { refine !pid_comp ⬝* _ ⬝* !comp_pid⁻¹*,
+        refine !comp_pid⁻¹* ⬝* pconcat2 _ _,
+        { exact !comp_pid⁻¹*},
+        { refine cast (ap (λx, _ ~* loop_space_pequiv x) !loop_space_pequiv_rfl)⁻¹ _,
+          refine cast (ap (λx, _ ~* x) !loop_space_pequiv_rfl)⁻¹ _, reflexivity}},
+      { refine _ ⬝* !comp_pid⁻¹*,
+        refine _ ⬝* pwhisker_right _ (!homotopy_groups_fun2_add1_5)⁻¹*,
+        refine !ap1_compose⁻¹* ⬝* _ ⬝* !ap1_compose, apply ap1_phomotopy,
+        refine !ap1_compose⁻¹* ⬝* _ ⬝* !ap1_compose, apply ap1_phomotopy,
+        exact IH ⬝* !comp_pid}},
+    { /-k=k'+6-/ exfalso, apply lt_le_antisymm H, apply le_add_left}
+  end
+
+  definition type_LES_of_homotopy_groups2 [constructor] : type_chain_complex +6ℕ :=
+  transfer_type_chain_complex2
+    (type_LES_of_homotopy_groups f)
+    !fin_prod_nat_equiv_nat
+    nat_of_str_6S
+    @homotopy_groups_fun2
+    @homotopy_groups2_pequiv
+    begin
+      intro m x,
+      refine homotopy_groups_fun2_phomotopy m x ⬝ _,
+      apply ap (homotopy_groups_fun2 m), apply ap (homotopy_groups2_pequiv (S m)),
+      esimp, exact ap010 cast !ap_compose⁻¹ x
+    end
+
+  definition is_exact_type_LES_of_homotopy_groups2 : is_exact_t (type_LES_of_homotopy_groups2) :=
+  begin
+    intro n,
+    apply is_exact_at_transfer2,
+    apply is_exact_type_LES_of_homotopy_groups
+  end
+
+  definition LES_of_homotopy_groups2 [constructor] : chain_complex +6ℕ :=
+  trunc_chain_complex type_LES_of_homotopy_groups2
+
+/--------------
+    PART 4
+ --------------/
+
+  definition homotopy_groups3 [reducible] : +6ℕ → Set*
+  | (n, fin.mk 0 H) := π*[2*n] Y
+  | (n, fin.mk 1 H) := π*[2*n] X
+  | (n, fin.mk 2 H) := π*[2*n] (pfiber f)
+  | (n, fin.mk 3 H) := π*[2*n + 1] Y
+  | (n, fin.mk 4 H) := π*[2*n + 1] X
+  | (n, fin.mk k H) := π*[2*n + 1] (pfiber f)
+
+  definition homotopy_groups3eq2 [reducible]
+    : Π(n : +6ℕ), ptrunc 0 (homotopy_groups2 n) ≃* homotopy_groups3 n
+  | (n, fin.mk 0 H) := by reflexivity
+  | (n, fin.mk 1 H) := by reflexivity
+  | (n, fin.mk 2 H) := by reflexivity
+  | (n, fin.mk 3 H) := by reflexivity
+  | (n, fin.mk 4 H) := by reflexivity
+  | (n, fin.mk 5 H) := by reflexivity
+  | (n, fin.mk (k+6) H) := begin exfalso, apply lt_le_antisymm H, apply le_add_left end
+
+  definition homotopy_groups_fun3 : Π(n : +6ℕ), homotopy_groups3 (S n) →* homotopy_groups3 n
+  | (n, fin.mk 0 H) := proof π→*[2*n] f qed
+  | (n, fin.mk 1 H) := proof π→*[2*n] (ppoint f) qed
+  | (n, fin.mk 2 H) :=
+    proof π→*[2*n] (boundary_map f) ∘* pcast (ap (ptrunc 0) (loop_space_succ_eq_in Y (2*n))) qed
+  | (n, fin.mk 3 H) := proof π→*[2*n + 1] f ∘* tinverse qed
+  | (n, fin.mk 4 H) := proof π→*[2*n + 1] (ppoint f) ∘* tinverse qed
+  | (n, fin.mk 5 H) :=
+    proof (π→*[2*n + 1] (boundary_map f) ∘* tinverse)
+          ∘* pcast (ap (ptrunc 0) (loop_space_succ_eq_in Y (2*n+1))) qed
+  | (n, fin.mk (k+6) H) := begin exfalso, apply lt_le_antisymm H, apply le_add_left end
+
+  definition homotopy_groups_fun3eq2 [reducible]
+    : Π(n : +6ℕ), homotopy_groups3eq2 n ∘* ptrunc_functor 0 (homotopy_groups_fun2 n) ~*
+      homotopy_groups_fun3 n ∘* homotopy_groups3eq2 (S n)
+  | (n, fin.mk 0 H) := by reflexivity
+  | (n, fin.mk 1 H) := by reflexivity
+  | (n, fin.mk 2 H) :=
+    begin
+      refine !pid_comp ⬝* _ ⬝* !comp_pid⁻¹*,
+      refine !ptrunc_functor_pcompose ⬝* _,
+      apply pwhisker_left, apply ptrunc_functor_pcast,
+    end
+  | (n, fin.mk 3 H) :=
+    begin
+      refine !pid_comp ⬝* _ ⬝* !comp_pid⁻¹*,
+      refine !ptrunc_functor_pcompose ⬝* _,
+      apply pwhisker_left, apply ptrunc_functor_pinverse
+    end
+  | (n, fin.mk 4 H) :=
+    begin
+      refine !pid_comp ⬝* _ ⬝* !comp_pid⁻¹*,
+      refine !ptrunc_functor_pcompose ⬝* _,
+      apply pwhisker_left, apply ptrunc_functor_pinverse
+    end
+  | (n, fin.mk 5 H) :=
+    begin
+      refine !pid_comp ⬝* _ ⬝* !comp_pid⁻¹*,
+      refine !ptrunc_functor_pcompose ⬝* _,
+      apply pconcat2,
+      { refine !ptrunc_functor_pcompose ⬝* _,
+        apply pwhisker_left, apply ptrunc_functor_pinverse},
+      { apply ptrunc_functor_pcast}
+    end
+  | (n, fin.mk (k+6) H) := begin exfalso, apply lt_le_antisymm H, apply le_add_left end
+
+  definition LES_of_homotopy_groups3 [constructor] : chain_complex +6ℕ :=
+  transfer_chain_complex
+    LES_of_homotopy_groups2
+    homotopy_groups_fun3
+    homotopy_groups3eq2
+    homotopy_groups_fun3eq2
+
+  definition is_exact_LES_of_homotopy_groups3 : is_exact (LES_of_homotopy_groups3) :=
+  begin
+    intro n,
+    apply is_exact_at_transfer,
+    apply is_exact_at_trunc,
+    apply is_exact_type_LES_of_homotopy_groups2
+  end
+
+  end
+
+  open is_trunc
+  universe variable u
+  variables {X Y : pType.{u}} (f : X →* Y) (n : ℕ)
+  include f
+
+  /- the carrier of the fiber sequence is definitionally what we want (as pointed sets) -/
+  example : LES_of_homotopy_groups3 f (str_of_nat 6)  = π*[2] Y          :> Set* := by reflexivity
+  example : LES_of_homotopy_groups3 f (str_of_nat 7)  = π*[2] X          :> Set* := by reflexivity
+  example : LES_of_homotopy_groups3 f (str_of_nat 8)  = π*[2] (pfiber f) :> Set* := by reflexivity
+  example : LES_of_homotopy_groups3 f (str_of_nat 9)  = π*[3] Y          :> Set* := by reflexivity
+  example : LES_of_homotopy_groups3 f (str_of_nat 10) = π*[3] X          :> Set* := by reflexivity
+  example : LES_of_homotopy_groups3 f (str_of_nat 11) = π*[3] (pfiber f) :> Set* := by reflexivity
+
+  definition LES_of_homotopy_groups3_0 : LES_of_homotopy_groups3 f (n, 0) = π*[2*n] Y :=
+  by reflexivity
+  definition LES_of_homotopy_groups3_1 : LES_of_homotopy_groups3 f (n, 1) = π*[2*n] X :=
+  by reflexivity
+  definition LES_of_homotopy_groups3_2 : LES_of_homotopy_groups3 f (n, 2) = π*[2*n] (pfiber f) :=
+  by reflexivity
+  definition LES_of_homotopy_groups3_3 : LES_of_homotopy_groups3 f (n, 3) = π*[2*n + 1] Y :=
+  by reflexivity
+  definition LES_of_homotopy_groups3_4 : LES_of_homotopy_groups3 f (n, 4) = π*[2*n + 1] X :=
+  by reflexivity
+  definition LES_of_homotopy_groups3_5 : LES_of_homotopy_groups3 f (n, 5) = π*[2*n + 1] (pfiber f):=
+  by reflexivity
+
+  /- the functions of the fiber sequence is definitionally what we want (as pointed function).
+      -/
+
+  definition LES_of_homotopy_groups_fun3_0 :
+    cc_to_fn (LES_of_homotopy_groups3 f) (n, 0) = π→*[2*n] f :=
+  by reflexivity
+  definition LES_of_homotopy_groups_fun3_1 :
+    cc_to_fn (LES_of_homotopy_groups3 f) (n, 1) = π→*[2*n] (ppoint f) :=
+  by reflexivity
+  definition LES_of_homotopy_groups_fun3_2 : cc_to_fn (LES_of_homotopy_groups3 f) (n, 2) =
+    π→*[2*n] (boundary_map f) ∘* pcast (ap (ptrunc 0) (loop_space_succ_eq_in Y (2*n))) :=
+  by reflexivity
+  definition LES_of_homotopy_groups_fun3_3 :
+    cc_to_fn (LES_of_homotopy_groups3 f) (n, 3) = π→*[2*n + 1] f ∘* tinverse :=
+  by reflexivity
+  definition LES_of_homotopy_groups_fun3_4 :
+    cc_to_fn (LES_of_homotopy_groups3 f) (n, 4) = π→*[2*n + 1] (ppoint f) ∘* tinverse :=
+  by reflexivity
+  definition LES_of_homotopy_groups_fun3_5 : cc_to_fn (LES_of_homotopy_groups3 f) (n, 5) =
+    (π→*[2*n + 1] (boundary_map f) ∘* tinverse) ∘*
+    pcast (ap (ptrunc 0) (loop_space_succ_eq_in Y (2*n+1))) :=
+  by reflexivity
+
+  definition group_LES_of_homotopy_groups3_4 :
+    Π(k : ℕ) (H : k + 3 < succ 5), group (LES_of_homotopy_groups3 f (0, fin.mk (k+3) H))
+  | 0     H := begin rexact group_homotopy_group 0 Y end
+  | 1     H := begin rexact group_homotopy_group 0 X end
+  | 2     H := begin rexact group_homotopy_group 0 (pfiber f) end
+  | (k+3) H := begin exfalso, apply lt_le_antisymm H, apply le_add_left end
+
+  definition comm_group_LES_of_homotopy_groups3 (n : ℕ) : Π(x : fin (succ 5)),
+    comm_group (LES_of_homotopy_groups3 f (n + 1, x))
+  | (fin.mk 0 H) := proof comm_group_homotopy_group (2*n) Y qed
+  | (fin.mk 1 H) := proof comm_group_homotopy_group (2*n) X qed
+  | (fin.mk 2 H) := proof comm_group_homotopy_group (2*n) (pfiber f) qed
+  | (fin.mk 3 H) := proof comm_group_homotopy_group (2*n+1) Y qed
+  | (fin.mk 4 H) := proof comm_group_homotopy_group (2*n+1) X qed
+  | (fin.mk 5 H) := proof comm_group_homotopy_group (2*n+1) (pfiber f) qed
+  | (fin.mk (k+6) H) := begin exfalso, apply lt_le_antisymm H, apply le_add_left end
+
+  definition CommGroup_LES_of_homotopy_groups3 (n : +6ℕ) : CommGroup.{u} :=
+  CommGroup.mk (LES_of_homotopy_groups3 f (pr1 n + 1, pr2 n))
+               (comm_group_LES_of_homotopy_groups3 f (pr1 n) (pr2 n))
+
+  definition homomorphism_LES_of_homotopy_groups_fun3 : Π(k : +6ℕ),
+    CommGroup_LES_of_homotopy_groups3 f (S k) →g CommGroup_LES_of_homotopy_groups3 f k
+  | (k, fin.mk 0 H) :=
+    proof homomorphism.mk (cc_to_fn (LES_of_homotopy_groups3 f) (k + 1, 0))
+                          (phomotopy_group_functor_mul _ _) qed
+  | (k, fin.mk 1 H) :=
+    proof homomorphism.mk (cc_to_fn (LES_of_homotopy_groups3 f) (k + 1, 1))
+                          (phomotopy_group_functor_mul _ _) qed
+  | (k, fin.mk 2 H) :=
+    begin
+      apply homomorphism.mk (cc_to_fn (LES_of_homotopy_groups3 f) (k + 1, 2)),
+      exact abstract begin rewrite [LES_of_homotopy_groups_fun3_2],
+      refine @is_homomorphism_compose _ _ _ _ _ _ (π→*[2 * (k + 1)] boundary_map f) _ _ _,
+      { apply group_homotopy_group ((2 * k) + 1)},
+      { apply phomotopy_group_functor_mul},
+      { rewrite [▸*, -ap_compose', ▸*],
+        apply is_homomorphism_cast_loop_space_succ_eq_in} end end
+    end
+  | (k, fin.mk 3 H) :=
+    begin
+      apply homomorphism.mk (cc_to_fn (LES_of_homotopy_groups3 f) (k + 1, 3)),
+      exact abstract begin rewrite [LES_of_homotopy_groups_fun3_3],
+      refine @is_homomorphism_compose _ _ _ _ _ _ (π→*[2 * (k + 1) + 1] f) tinverse _ _,
+      { apply group_homotopy_group (2 * (k+1))},
+      { apply phomotopy_group_functor_mul},
+      { apply is_homomorphism_inverse} end end
+    end
+  | (k, fin.mk 4 H) :=
+    begin
+      apply homomorphism.mk (cc_to_fn (LES_of_homotopy_groups3 f) (k + 1, 4)),
+      exact abstract begin rewrite [LES_of_homotopy_groups_fun3_4],
+      refine @is_homomorphism_compose _ _ _ _ _ _ (π→*[2 * (k + 1) + 1] (ppoint f)) tinverse _ _,
+      { apply group_homotopy_group (2 * (k+1))},
+      { apply phomotopy_group_functor_mul},
+      { apply is_homomorphism_inverse} end end
+    end
+  | (k, fin.mk 5 H) :=
+    begin
+      apply homomorphism.mk (cc_to_fn (LES_of_homotopy_groups3 f) (k + 1, 5)),
+      exact abstract begin rewrite [LES_of_homotopy_groups_fun3_5],
+      refine @is_homomorphism_compose _ _ _ _ _ _
+               (π→*[2 * (k + 1) + 1] (boundary_map f) ∘ tinverse) _ _ _,
+      { refine @is_homomorphism_compose _ _ _ _ _ _
+                 (π→*[2 * (k + 1) + 1] (boundary_map f)) tinverse _ _,
+        { apply group_homotopy_group (2 * (k+1))},
+        { apply phomotopy_group_functor_mul},
+        { apply is_homomorphism_inverse}},
+      { rewrite [▸*, -ap_compose', ▸*],
+        apply is_homomorphism_cast_loop_space_succ_eq_in} end end
+    end
+  | (k, fin.mk (l+6) H) := begin exfalso, apply lt_le_antisymm H, apply le_add_left end
+
+  --TODO: the maps 3, 4 and 5 are anti-homomorphisms.
+
 end chain_complex
diff --git a/homotopy/chain_complex.hlean b/homotopy/chain_complex.hlean
index ccd165d..827f775 100644
--- a/homotopy/chain_complex.hlean
+++ b/homotopy/chain_complex.hlean
@@ -5,10 +5,10 @@ Authors: Floris van Doorn
 
 -/
 
-import types.int types.pointed2 types.trunc
-
-open eq pointed int unit is_equiv equiv is_trunc trunc equiv.ops
+import types.int types.pointed2 types.trunc algebra.hott ..group_theory.basic .fin
 
+open eq pointed int unit is_equiv equiv is_trunc trunc equiv.ops function algebra group sigma.ops
+     sum prod nat bool fin
 namespace eq
   definition transport_eq_Fl_idp_left {A B : Type} {a : A} {b : B} (f : A → B) (q : f a = b)
     : transport_eq_Fl idp q = !idp_con⁻¹ :=
@@ -21,89 +21,131 @@ namespace eq
 
 end eq open eq
 
+structure succ_str : Type :=
+  (carrier : Type)
+  (succ : carrier → carrier)
+
+attribute succ_str.carrier [coercion]
+
+definition succ_str.S {X : succ_str} : X → X := succ_str.succ X
+
+open succ_str
+
+definition snat [reducible] [constructor] : succ_str := succ_str.mk ℕ nat.succ
+definition snat' [reducible] [constructor] : succ_str := succ_str.mk ℕ nat.pred
+definition sint [reducible] [constructor] : succ_str := succ_str.mk ℤ int.succ
+definition sint' [reducible] [constructor] : succ_str := succ_str.mk ℤ int.pred
+
+notation `+ℕ` := snat
+notation `-ℕ` := snat'
+notation `+ℤ` := sint
+notation `-ℤ` := sint'
+
+definition stratified_type [reducible] (N : succ_str) (n : ℕ) : Type₀ := N × fin (succ n)
+
+-- definition stratified_succ' {N : succ_str}  : Π{n : ℕ}, N → ifin n → stratified_type N n
+-- | (succ k) n (fz k) := (S n, ifin.max k)
+-- | (succ k) n (fs x) := (n, ifin.incl x)
+
+-- definition stratified_succ {N : succ_str} {n : ℕ} (x : stratified_type N n) : stratified_type N n :=
+-- stratified_succ' (pr1 x) (pr2 x)
+
+definition stratified_succ {N : succ_str} {n : ℕ} (x : stratified_type N n)
+  : stratified_type N n :=
+(if val (pr2 x) = n then S (pr1 x) else pr1 x, my_succ (pr2 x))
+
+definition stratified [reducible] [constructor] (N : succ_str) (n : ℕ) : succ_str :=
+succ_str.mk (stratified_type N n) stratified_succ
+
+--example (n : ℕ) : flatten (n, (2 : ifin (nat.succ (nat.succ 4)))) = 6*n+2 := proof rfl qed
+
+notation `+3ℕ` := stratified +ℕ 2
+notation `-3ℕ` := stratified -ℕ 2
+notation `+3ℤ` := stratified +ℤ 2
+notation `-3ℤ` := stratified -ℤ 2
+notation `+6ℕ` := stratified +ℕ 5
+notation `-6ℕ` := stratified -ℕ 5
+notation `+6ℤ` := stratified +ℤ 5
+notation `-6ℤ` := stratified -ℤ 5
+
+-- definition triple_type (N : succ_str) : Type₀ := N ⊎ N ⊎ N
+-- definition triple_succ {N : succ_str} : triple_type N → triple_type N
+-- | (inl n)       := inr (inl n)
+-- | (inr (inl n)) := inr (inr n)
+-- | (inr (inr n)) := inl (S n)
+
+-- definition triple [reducible] [constructor] (N : succ_str) : succ_str :=
+-- succ_str.mk (triple_type N) triple_succ
+
+-- notation `+3ℕ` := triple +ℕ
+-- notation `-3ℕ` := triple -ℕ
+-- notation `+3ℤ` := triple +ℤ
+-- notation `-3ℤ` := triple -ℤ
+
 namespace chain_complex
 
   -- are chain complexes with the "set"-requirement removed interesting?
-  structure type_chain_complex : Type :=
-    (car : ℤ → Type*)
-    (fn : Π(n : ℤ), car (n + 1) →* car n)
-    (is_chain_complex : Π{n : ℤ} (x : car ((n + 1) + 1)), fn n (fn (n+1) x) = pt)
+  structure type_chain_complex (N : succ_str) : Type :=
+    (car : N → Type*)
+    (fn : Π(n : N), car (S n) →* car n)
+    (is_chain_complex : Π(n : N) (x : car (S (S n))), fn n (fn (S n) x) = pt)
 
-  structure left_type_chain_complex : Type := -- chain complex on the naturals with maps going down
-    (car : ℕ → Type*)
-    (fn : Π(n : ℕ), car (n + 1) →* car n)
-    (is_chain_complex : Π{n : ℕ} (x : car ((n + 1) + 1)), fn n (fn (n+1) x) = pt)
+  section
+  variables {N : succ_str} (X : type_chain_complex N) (n : N)
 
-  structure right_type_chain_complex : Type := -- chain complex on the naturals with maps going up
-    (car : ℕ → Type*)
-    (fn : Π(n : ℕ), car n →* car (n + 1))
-    (is_chain_complex : Π{n : ℕ} (x : car n), fn (n+1) (fn n x) = pt)
-
-  definition  tcc_to_car [unfold 1] [coercion] := @type_chain_complex.car
-  definition  tcc_to_fn  [unfold 1]            := @type_chain_complex.fn
-  definition  tcc_is_chain_complex  [unfold 1] := @type_chain_complex.is_chain_complex
-  definition ltcc_to_car [unfold 1] [coercion] := @left_type_chain_complex.car
-  definition ltcc_to_fn  [unfold 1]            := @left_type_chain_complex.fn
-  definition ltcc_is_chain_complex  [unfold 1] := @left_type_chain_complex.is_chain_complex
-  definition rtcc_to_car [unfold 1] [coercion] := @right_type_chain_complex.car
-  definition rtcc_to_fn  [unfold 1]            := @right_type_chain_complex.fn
-  definition rtcc_is_chain_complex  [unfold 1] := @right_type_chain_complex.is_chain_complex
+  definition tcc_to_car [unfold 2] [coercion] := @type_chain_complex.car
+  definition tcc_to_fn  [unfold 2] : X (S n) →* X n := type_chain_complex.fn X n
+  definition tcc_is_chain_complex  [unfold 2]
+    : Π(x : X (S (S n))), tcc_to_fn X n (tcc_to_fn X (S n) x) = pt :=
+  type_chain_complex.is_chain_complex X n
 
   -- important: these notions are shifted by one! (this is to avoid transports)
-  definition is_exact_at_t [reducible] (X : type_chain_complex) (n : ℤ) : Type :=
-  Π(x : X (n + 1)), tcc_to_fn X n x = pt → fiber (tcc_to_fn X (n+1)) x
-  definition is_exact_at_lt [reducible] (X : left_type_chain_complex) (n : ℕ) : Type :=
-  Π(x : X (n + 1)), ltcc_to_fn X n x = pt → fiber (ltcc_to_fn X (n+1)) x
-  definition is_exact_at_rt [reducible] (X : right_type_chain_complex) (n : ℕ) : Type :=
-  Π(x : X (n + 1)), rtcc_to_fn X (n+1) x = pt → fiber (rtcc_to_fn X n) x
+  definition is_exact_at_t [reducible] /- X n -/ : Type :=
+  Π(x : X (S n)), tcc_to_fn X n x = pt → fiber (tcc_to_fn X (S n)) x
 
-  definition is_exact_t   [reducible] (X : type_chain_complex) : Type :=
-  Π(n : ℤ), is_exact_at_t X n
-  definition is_exact_lt [reducible] (X : left_type_chain_complex) : Type :=
-  Π(n : ℕ), is_exact_at_lt X n
-  definition is_exact_rt [reducible] (X : right_type_chain_complex) : Type :=
-  Π(n : ℕ), is_exact_at_rt X n
+  definition is_exact_t [reducible] /- X -/ : Type :=
+  Π(n : N), is_exact_at_t X n
 
-  definition type_chain_complex_from_left (X : left_type_chain_complex) : type_chain_complex :=
-  type_chain_complex.mk (int.rec X (λn, punit))
-    begin
-      intro n, fconstructor,
-      { induction n with n n,
-        { exact @ltcc_to_fn X n},
-        { esimp, intro x, exact star}},
-      { induction n with n n,
-        { apply respect_pt},
-        { reflexivity}}
-    end
-    begin
-      intro n, induction n with n n,
-      { exact ltcc_is_chain_complex X},
-      { esimp, intro x, reflexivity}
-    end
+  -- definition type_chain_complex_from_left (X : type_chain_complex) : type_chain_complex :=
+  -- type_chain_complex.mk (int.rec X (λn, punit))
+  --   begin
+  --     intro n, fconstructor,
+  --     { induction n with n n,
+  --       { exact @ltcc_to_fn X n},
+  --       { esimp, intro x, exact star}},
+  --     { induction n with n n,
+  --       { apply respect_pt},
+  --       { reflexivity}}
+  --   end
+  --   begin
+  --     intro n, induction n with n n,
+  --     { exact ltcc_is_chain_complex X},
+  --     { esimp, intro x, reflexivity}
+  --   end
 
-  definition is_exact_t_from_left {X : left_type_chain_complex} {n : ℕ} (H : is_exact_at_lt X n)
-    : is_exact_at_t (type_chain_complex_from_left X) n :=
-  H
+  -- definition is_exact_t_from_left {X : type_chain_complex} {n : ℕ} (H : is_exact_at_lt X n)
+  --   : is_exact_at_t (type_chain_complex_from_left X) n :=
+  -- H
 
-  definition transfer_left_type_chain_complex [constructor] (X : left_type_chain_complex)
-    {Y : ℕ → Type*} (g : Π{n : ℕ}, Y (n + 1) →* Y n) (e : Π{n}, X n ≃* Y n)
-    (p : Π{n} (x : X (n + 1)), e (ltcc_to_fn X n x) = g (e x)) : left_type_chain_complex :=
-  left_type_chain_complex.mk Y @g
-    begin
+  definition transfer_type_chain_complex [constructor]
+    {Y : N → Type*} (g : Π{n : N}, Y (S n) →* Y n) (e : Π{n}, X n ≃* Y n)
+    (p : Π{n} (x : X (S n)), e (tcc_to_fn X n x) = g (e x)) : type_chain_complex N :=
+  type_chain_complex.mk Y @g
+    abstract begin
       intro n, apply equiv_rect (equiv_of_pequiv e), intro x,
       refine ap g (p x)⁻¹ ⬝ _,
       refine (p _)⁻¹ ⬝ _,
-      refine ap e (ltcc_is_chain_complex X _) ⬝ _,
+      refine ap e (tcc_is_chain_complex X n _) ⬝ _,
       apply respect_pt
-    end
+    end end
 
-  definition is_exact_at_lt_transfer {X : left_type_chain_complex} {Y : ℕ → Type*}
-    {g : Π{n : ℕ}, Y (n + 1) →* Y n} (e : Π{n}, X n ≃* Y n)
-    (p : Π{n} (x : X (n + 1)), e (ltcc_to_fn X n x) = g (e x)) {n : ℕ}
-    (H : is_exact_at_lt X n) : is_exact_at_lt (transfer_left_type_chain_complex X @g @e @p) n :=
+  theorem is_exact_at_t_transfer {X : type_chain_complex N} {Y : N → Type*}
+    {g : Π{n : N}, Y (S n) →* Y n} (e : Π{n}, X n ≃* Y n)
+    (p : Π{n} (x : X (S n)), e (tcc_to_fn X n x) = g (e x)) {n : N}
+    (H : is_exact_at_t X n) : is_exact_at_t (transfer_type_chain_complex X @g @e @p) n :=
   begin
     intro y q, esimp at *,
-    assert H2 : ltcc_to_fn X n (e⁻¹ᵉ* y) = pt,
+    assert H2 : tcc_to_fn X n (e⁻¹ᵉ* y) = pt,
     { refine (inv_commute (λn, equiv_of_pequiv e) _ _ @p _)⁻¹ᵖ ⬝ _,
       refine ap _ q ⬝ _,
       exact respect_pt e⁻¹ᵉ*},
@@ -114,97 +156,142 @@ namespace chain_complex
     apply right_inv
   end
 
-  definition trunc_left_type_chain_complex [constructor] (X : left_type_chain_complex)
-    (k : trunc_index) : left_type_chain_complex :=
-  left_type_chain_complex.mk
-    (λn, ptrunc k (X n))
-    (λn, ptrunc_functor k (ltcc_to_fn X n))
+  -- move to init.equiv. This is inv_commute for A ≡ unit
+  definition inv_commute1' {B C : Type} (f : B → C) [is_equiv f] (h : B → B) (h' : C → C)
+    (p : Π(b : B), f (h b) = h' (f b)) (c : C) : f⁻¹ (h' c) = h (f⁻¹ c) :=
+  eq_of_fn_eq_fn' f (right_inv f (h' c) ⬝ ap h' (right_inv f c)⁻¹ ⬝ (p (f⁻¹ c))⁻¹)
+
+  definition inv_commute1 {B C : Type} (f : B ≃ C) (h : B → B) (h' : C → C)
+    (p : Π(b : B), f (h b) =   h' (f b)) (c : C) : f⁻¹ (h' c) = h (f⁻¹ c) :=
+  inv_commute1' (to_fun f) h h' p c
+
+  definition fn_cast_eq_cast_fn {A : Type} {P Q : A → Type} {x y : A} (p : x = y)
+    (f : Πx, P x → Q x) (z : P x) : f y (cast (ap P p) z) = cast (ap Q p) (f x z) :=
+  by induction p; reflexivity
+
+  definition cast_cast_inv {A : Type} {P : A → Type} {x y : A} (p : x = y) (z : P y) :
+    cast (ap P p) (cast (ap P p⁻¹) z) = z :=
+  by induction p; reflexivity
+
+  definition cast_inv_cast {A : Type} {P : A → Type} {x y : A} (p : x = y) (z : P x) :
+    cast (ap P p⁻¹) (cast (ap P p) z) = z :=
+  by induction p; reflexivity
+
+  -- more general transfer, where the base type can also change by an equivalence.
+  definition transfer_type_chain_complex2 [constructor] {M : succ_str} {Y : M → Type*}
+    (f : M ≃ N) (c : Π(m : M), S (f m) = f (S m))
+    (g : Π{m : M}, Y (S m) →* Y m) (e : Π{m}, X (f m) ≃* Y m)
+    (p : Π{m} (x : X (S (f m))), e (tcc_to_fn X (f m) x) = g (e (cast (ap (λx, X x) (c m)) x)))
+    : type_chain_complex M :=
+  type_chain_complex.mk Y @g
     begin
-      intro n x, esimp at *,
-      refine trunc.rec _ x, -- why doesn't induction work here?
-      clear x, intro x, esimp,
-      exact ap tr (ltcc_is_chain_complex X x)
-    end
-
-  /- actual (set) chain complexes -/
-
-  structure chain_complex : Type :=
-    (car : ℤ → Set*)
-    (fn : Π(n : ℤ), car (n + 1) →* car n)
-    (is_chain_complex : Π{n : ℤ} (x : car ((n + 1) + 1)), fn n (fn (n+1) x) = pt)
-
-  structure left_chain_complex : Type := -- chain complex on the naturals with maps going down
-    (car : ℕ → Set*)
-    (fn : Π(n : ℕ), car (n + 1) →* car n)
-    (is_chain_complex : Π{n : ℕ} (x : car ((n + 1) + 1)), fn n (fn (n+1) x) = pt)
-
-  structure right_chain_complex : Type := -- chain complex on the naturals with maps going up
-    (car : ℕ → Set*)
-    (fn : Π(n : ℕ), car n →* car (n + 1))
-    (is_chain_complex : Π{n : ℕ} (x : car n), fn (n+1) (fn n x) = pt)
-
-  definition  cc_to_car [unfold 1] [coercion] := @chain_complex.car
-  definition  cc_to_fn  [unfold 1]            := @chain_complex.fn
-  definition  cc_is_chain_complex  [unfold 1] := @chain_complex.is_chain_complex
-  definition lcc_to_car [unfold 1] [coercion] := @left_chain_complex.car
-  definition lcc_to_fn  [unfold 1]            := @left_chain_complex.fn
-  definition lcc_is_chain_complex  [unfold 1] := @left_chain_complex.is_chain_complex
-  definition rcc_to_car [unfold 1] [coercion] := @right_chain_complex.car
-  definition rcc_to_fn  [unfold 1]            := @right_chain_complex.fn
-  definition rcc_is_chain_complex  [unfold 1] := @right_chain_complex.is_chain_complex
-
-  -- important: these notions are shifted by one! (this is to avoid transports)
-  definition is_exact_at [reducible] (X : chain_complex) (n : ℤ) : Type :=
-  Π(x : X (n + 1)), cc_to_fn X n x = pt → image (cc_to_fn X (n+1)) x
-  definition is_exact_at_l [reducible] (X : left_chain_complex) (n : ℕ) : Type :=
-  Π(x : X (n + 1)), lcc_to_fn X n x = pt → image (lcc_to_fn X (n+1)) x
-  definition is_exact_at_r [reducible] (X : right_chain_complex) (n : ℕ) : Type :=
-  Π(x : X (n + 1)), rcc_to_fn X (n+1) x = pt → image (rcc_to_fn X n) x
-
-  definition is_exact   [reducible] (X : chain_complex) : Type := Π(n : ℤ), is_exact_at X n
-  definition is_exact_l [reducible] (X : left_chain_complex) : Type := Π(n : ℕ), is_exact_at_l X n
-  definition is_exact_r [reducible] (X : right_chain_complex) : Type := Π(n : ℕ), is_exact_at_r X n
-
-  definition chain_complex_from_left (X : left_chain_complex) : chain_complex :=
-  chain_complex.mk (int.rec X (λn, punit))
-    begin
-      intro n, fconstructor,
-      { induction n with n n,
-        { exact @lcc_to_fn X n},
-        { esimp, intro x, exact star}},
-      { induction n with n n,
-        { apply respect_pt},
-        { reflexivity}}
-    end
-    begin
-      intro n, induction n with n n,
-      { exact lcc_is_chain_complex X},
-      { esimp, intro x, reflexivity}
-    end
-
-  definition is_exact_from_left {X : left_chain_complex} {n : ℕ} (H : is_exact_at_l X n)
-    : is_exact_at (chain_complex_from_left X) n :=
-  H
-
-  definition transfer_left_chain_complex [constructor] (X : left_chain_complex) {Y : ℕ → Set*}
-    (g : Π{n : ℕ}, Y (n + 1) →* Y n) (e : Π{n}, X n ≃* Y n)
-    (p : Π{n} (x : X (n + 1)), e (lcc_to_fn X n x) = g (e x)) : left_chain_complex :=
-  left_chain_complex.mk Y @g
-    begin
-      intro n, apply equiv_rect (equiv_of_pequiv e), intro x,
-      refine ap g (p x)⁻¹ ⬝ _,
+      intro m,
+      apply equiv_rect (equiv_of_pequiv e),
+      apply equiv_rect (equiv_of_eq (ap (λx, X x) (c (S m)))), esimp,
+      apply equiv_rect (equiv_of_eq (ap (λx, X (S x)) (c m))), esimp,
+      intro x, refine ap g (p _)⁻¹ ⬝ _,
+      refine ap g (ap e (fn_cast_eq_cast_fn (c m) (tcc_to_fn X) x)) ⬝ _,
       refine (p _)⁻¹ ⬝ _,
-      refine ap e (lcc_is_chain_complex X _) ⬝ _,
+      refine ap e (tcc_is_chain_complex X (f m) _) ⬝ _,
       apply respect_pt
     end
 
-  definition transfer_is_exact_at_l (X : left_chain_complex) {Y : ℕ → Set*}
-    (g : Π{n : ℕ}, Y (n + 1) →* Y n) (e : Π{n}, X n ≃* Y n)
-    (p : Π{n} (x : X (n + 1)), e (lcc_to_fn X n x) = g (e x))
-    {n : ℕ} (H : is_exact_at_l X n) : is_exact_at_l (transfer_left_chain_complex X @g @e @p) n :=
+  definition is_exact_at_transfer2 {X : type_chain_complex N} {M : succ_str} {Y : M → Type*}
+    (f : M ≃ N) (c : Π(m : M), S (f m) = f (S m))
+    (g : Π{m : M}, Y (S m) →* Y m) (e : Π{m}, X (f m) ≃* Y m)
+    (p : Π{m} (x : X (S (f m))), e (tcc_to_fn X (f m) x) = g (e (cast (ap (λx, X x) (c m)) x)))
+    {m : M} (H : is_exact_at_t X (f m))
+    : is_exact_at_t (transfer_type_chain_complex2 X f c @g @e @p) m :=
   begin
     intro y q, esimp at *,
-    assert H2 : lcc_to_fn X n (e⁻¹ᵉ* y) = pt,
+    assert H2 : tcc_to_fn X (f m) ((equiv_of_eq (ap (λx, X x) (c m)))⁻¹ᵉ (e⁻¹ y)) = pt,
+    { refine _ ⬝ ap e⁻¹ᵉ* q ⬝ (respect_pt (e⁻¹ᵉ*)), apply eq_inv_of_eq, clear q, revert y,
+      refine inv_homotopy_of_homotopy (pequiv.to_equiv e) _,
+      apply inv_homotopy_of_homotopy, apply p},
+    induction (H _ H2) with x r,
+    refine fiber.mk (e (cast (ap (λx, X x) (c (S m))) (cast (ap (λx, X (S x)) (c m)) x))) _,
+    refine (p _)⁻¹ ⬝ _,
+    refine ap e (fn_cast_eq_cast_fn (c m) (tcc_to_fn X) x) ⬝ _,
+    refine ap (λx, e (cast _ x)) r ⬝ _,
+    esimp [equiv.symm], rewrite [-ap_inv],
+    refine ap e !cast_cast_inv ⬝ _,
+    apply right_inv
+  end
+
+  -- definition trunc_type_chain_complex [constructor] (X : type_chain_complex N)
+  --   (k : trunc_index) : type_chain_complex N :=
+  -- type_chain_complex.mk
+  --   (λn, ptrunc k (X n))
+  --   (λn, ptrunc_functor k (tcc_to_fn X n))
+  --   begin
+  --     intro n x, esimp at *,
+  --     refine trunc.rec _ x, -- why doesn't induction work here?
+  --     clear x, intro x, esimp,
+  --     exact ap tr (tcc_is_chain_complex X n x)
+  --   end
+  end
+
+  /- actual (set) chain complexes -/
+  structure chain_complex (N : succ_str) : Type :=
+    (car : N → Set*)
+    (fn : Π(n : N), car (S n) →* car n)
+    (is_chain_complex : Π(n : N) (x : car (S (S n))), fn n (fn (S n) x) = pt)
+
+  section
+  variables {N : succ_str} (X : chain_complex N) (n : N)
+
+  definition cc_to_car [unfold 2] [coercion] := @chain_complex.car
+  definition cc_to_fn  [unfold 2] : X (S n) →* X n := @chain_complex.fn N X n
+  definition cc_is_chain_complex  [unfold 2]
+    : Π(x : X (S (S n))), cc_to_fn X n (cc_to_fn X (S n) x) = pt :=
+  @chain_complex.is_chain_complex N X n
+
+  -- important: these notions are shifted by one! (this is to avoid transports)
+  definition is_exact_at [reducible] /- X n -/ : Type :=
+  Π(x : X (S n)), cc_to_fn X n x = pt → image (cc_to_fn X (S n)) x
+
+  definition is_exact [reducible] /- X -/ : Type := Π(n : N), is_exact_at X n
+
+  -- definition chain_complex_from_left (X : chain_complex) : chain_complex :=
+  -- chain_complex.mk (int.rec X (λn, punit))
+  --   begin
+  --     intro n, fconstructor,
+  --     { induction n with n n,
+  --       { exact @lcc_to_fn X n},
+  --       { esimp, intro x, exact star}},
+  --     { induction n with n n,
+  --       { apply respect_pt},
+  --       { reflexivity}}
+  --   end
+  --   begin
+  --     intro n, induction n with n n,
+  --     { exact lcc_is_chain_complex X},
+  --     { esimp, intro x, reflexivity}
+  --   end
+
+  -- definition is_exact_from_left {X : chain_complex} {n : ℕ} (H : is_exact_at_l X n)
+  --   : is_exact_at (chain_complex_from_left X) n :=
+  -- H
+
+  definition transfer_chain_complex [constructor] {Y : N → Set*}
+    (g : Π{n : N}, Y (S n) →* Y n) (e : Π{n}, X n ≃* Y n)
+    (p : Π{n} (x : X (S n)), e (cc_to_fn X n x) = g (e x)) : chain_complex N :=
+  chain_complex.mk Y @g
+    abstract begin
+      intro n, apply equiv_rect (equiv_of_pequiv e), intro x,
+      refine ap g (p x)⁻¹ ⬝ _,
+      refine (p _)⁻¹ ⬝ _,
+      refine ap e (cc_is_chain_complex X n _) ⬝ _,
+      apply respect_pt
+    end end
+
+  theorem is_exact_at_transfer {X : chain_complex N} {Y : N → Set*}
+    (g : Π{n : N}, Y (S n) →* Y n) (e : Π{n}, X n ≃* Y n)
+    (p : Π{n} (x : X (S n)), e (cc_to_fn X n x) = g (e x))
+    {n : N} (H : is_exact_at X n) : is_exact_at (transfer_chain_complex X @g @e @p) n :=
+  begin
+    intro y q, esimp at *,
+    assert H2 : cc_to_fn X n (e⁻¹ᵉ* y) = pt,
     { refine (inv_commute (λn, equiv_of_pequiv e) _ _ @p _)⁻¹ᵖ ⬝ _,
       refine ap _ q ⬝ _,
       exact respect_pt e⁻¹ᵉ*},
@@ -216,20 +303,20 @@ namespace chain_complex
     apply right_inv
   end
 
-  definition trunc_left_chain_complex [constructor] (X : left_type_chain_complex)
-    : left_chain_complex :=
-  left_chain_complex.mk
+  definition trunc_chain_complex [constructor] (X : type_chain_complex N)
+    : chain_complex N :=
+  chain_complex.mk
     (λn, ptrunc 0 (X n))
-    (λn, ptrunc_functor 0 (ltcc_to_fn X n))
+    (λn, ptrunc_functor 0 (tcc_to_fn X n))
     begin
       intro n x, esimp at *,
       refine @trunc.rec _ _ _ (λH, !is_trunc_eq) _ x,
       clear x, intro x, esimp,
-      exact ap tr (ltcc_is_chain_complex X x)
+      exact ap tr (tcc_is_chain_complex X n x)
     end
 
-  definition is_exact_at_l_trunc (X : left_type_chain_complex) {n : ℕ}
-    (H : is_exact_at_lt X n) : is_exact_at_l (trunc_left_chain_complex X) n :=
+  definition is_exact_at_trunc (X : type_chain_complex N) {n : N}
+    (H : is_exact_at_t X n) : is_exact_at (trunc_chain_complex X) n :=
   begin
     intro x p, esimp at *,
     induction x with x, esimp at *,
@@ -240,4 +327,199 @@ namespace chain_complex
     esimp, exact ap tr r
   end
 
+  definition transfer_chain_complex2' [constructor] {M : succ_str} {Y : M → Set*}
+    (f : N ≃ M) (c : Π(n : N), f (S n) = S (f n))
+    (g : Π{m : M}, Y (S m) →* Y m) (e : Π{n}, X n ≃* Y (f n))
+    (p : Π{n} (x : X (S n)), e (cc_to_fn X n x) = g (c n ▸ e x)) : chain_complex M :=
+  chain_complex.mk Y @g
+    begin
+      refine equiv_rect f _ _, intro n,
+      assert H : Π (x : Y (f (S (S n)))), g (c n ▸ g (c (S n) ▸ x)) = pt,
+      { apply equiv_rect (equiv_of_pequiv e), intro x,
+        refine ap (λx, g (c n ▸ x)) (@p (S n) x)⁻¹ᵖ ⬝ _,
+        refine (p _)⁻¹ ⬝ _,
+        refine ap e (cc_is_chain_complex X n _) ⬝ _,
+        apply respect_pt},
+      refine pi.pi_functor _ _ H,
+      { intro x, exact (c (S n))⁻¹ ▸ (c n)⁻¹ ▸ x}, -- with implicit arguments, this is:
+      -- transport (λx, Y x) (c (S n))⁻¹ (transport (λx, Y (S x)) (c n)⁻¹ x)
+      { intro x, intro p, refine _ ⬝ p, rewrite [tr_inv_tr, fn_tr_eq_tr_fn (c n)⁻¹ @g, tr_inv_tr]}
+    end
+
+  definition is_exact_at_transfer2' {X : chain_complex N} {M : succ_str} {Y : M → Set*}
+    (f : N ≃ M) (c : Π(n : N), f (S n) = S (f n))
+    (g : Π{m : M}, Y (S m) →* Y m) (e : Π{n}, X n ≃* Y (f n))
+    (p : Π{n} (x : X (S n)), e (cc_to_fn X n x) = g (c n ▸ e x))
+    {n : N} (H : is_exact_at X n) : is_exact_at (transfer_chain_complex2' X f c @g @e @p) (f n) :=
+  begin
+    intro y q, esimp at *,
+    assert H2 : cc_to_fn X n (e⁻¹ᵉ* ((c n)⁻¹ ▸ y)) = pt,
+    { refine (inv_commute (λn, equiv_of_pequiv e) _ _ @p _)⁻¹ᵖ ⬝ _,
+      rewrite [tr_inv_tr, q],
+      exact respect_pt e⁻¹ᵉ*},
+    induction (H _ H2) with x,
+    induction x with x r,
+    refine image.mk (c n ▸ c (S n) ▸ e x) _,
+    rewrite [fn_tr_eq_tr_fn (c n) @g],
+    refine ap (λx, c n ▸ x) (p x)⁻¹ ⬝ _,
+    refine ap (λx, c n ▸ e x) r ⬝ _,
+    refine ap (λx, c n ▸ x) !right_inv ⬝ _,
+    apply tr_inv_tr,
+  end
+
+  -- structure group_chain_complex : Type :=
+  --   (car : N → Group)
+  --   (fn : Π(n : N), car (S n) →g car n)
+  --   (is_chain_complex : Π{n : N} (x : car ((S n) + 1)), fn n (fn (S n) x) = 1)
+
+  -- structure group_chain_complex : Type := -- chain complex on the naturals with maps going down
+  --   (car : N → Group)
+  --   (fn : Π(n : N), car (S n) →g car n)
+  --   (is_chain_complex : Π{n : N} (x : car ((S n) + 1)), fn n (fn (S n) x) = 1)
+
+  -- structure right_group_chain_complex : Type := -- chain complex on the naturals with maps going up
+  --   (car : N → Group)
+  --   (fn : Π(n : N), car n →g car (S n))
+  --   (is_chain_complex : Π{n : N} (x : car n), fn (S n) (fn n x) = 1)
+
+  -- definition  gcc_to_car [unfold 1] [coercion] := @group_chain_complex.car
+  -- definition  gcc_to_fn  [unfold 1]            := @group_chain_complex.fn
+  -- definition  gcc_is_chain_complex  [unfold 1] := @group_chain_complex.is_chain_complex
+  -- definition lgcc_to_car [unfold 1] [coercion] := @left_group_chain_complex.car
+  -- definition lgcc_to_fn  [unfold 1]            := @left_group_chain_complex.fn
+  -- definition lgcc_is_chain_complex  [unfold 1] := @left_group_chain_complex.is_chain_complex
+  -- definition rgcc_to_car [unfold 1] [coercion] := @right_group_chain_complex.car
+  -- definition rgcc_to_fn  [unfold 1]            := @right_group_chain_complex.fn
+  -- definition rgcc_is_chain_complex  [unfold 1] := @right_group_chain_complex.is_chain_complex
+
+  -- -- important: these notions are shifted by one! (this is to avoid transports)
+  -- definition is_exact_at_g [reducible] (X : group_chain_complex) (n : N) : Type :=
+  -- Π(x : X (S n)), gcc_to_fn X n x = 1 → image (gcc_to_fn X (S n)) x
+  -- definition is_exact_at_lg [reducible] (X : left_group_chain_complex) (n : N) : Type :=
+  -- Π(x : X (S n)), lgcc_to_fn X n x = 1 → image (lgcc_to_fn X (S n)) x
+  -- definition is_exact_at_rg [reducible] (X : right_group_chain_complex) (n : N) : Type :=
+  -- Π(x : X (S n)), rgcc_to_fn X (S n) x = 1 → image (rgcc_to_fn X n) x
+
+  -- definition is_exact_g   [reducible] (X : group_chain_complex) : Type :=
+  -- Π(n : N), is_exact_at_g X n
+  -- definition is_exact_lg [reducible] (X : left_group_chain_complex) : Type :=
+  -- Π(n : N), is_exact_at_lg X n
+  -- definition is_exact_rg [reducible] (X : right_group_chain_complex) : Type :=
+  -- Π(n : N), is_exact_at_rg X n
+
+  -- definition group_chain_complex_from_left (X : left_group_chain_complex) : group_chain_complex :=
+  -- group_chain_complex.mk (int.rec X (λn, G0))
+  --   begin
+  --     intro n, fconstructor,
+  --     { induction n with n n,
+  --       { exact @lgcc_to_fn X n},
+  --       { esimp, intro x, exact star}},
+  --     { induction n with n n,
+  --       { apply respect_mul},
+  --       { intro g h, reflexivity}}
+  --   end
+  --   begin
+  --     intro n, induction n with n n,
+  --     { exact lgcc_is_chain_complex X},
+  --     { esimp, intro x, reflexivity}
+  --   end
+
+  -- definition is_exact_g_from_left {X : left_group_chain_complex} {n : N} (H : is_exact_at_lg X n)
+  --   : is_exact_at_g (group_chain_complex_from_left X) n :=
+  -- H
+
+  -- definition transfer_left_group_chain_complex [constructor] (X : left_group_chain_complex)
+  --   {Y : N → Group} (g : Π{n : N}, Y (S n) →g Y n) (e : Π{n}, X n ≃* Y n)
+  --   (p : Π{n} (x : X (S n)), e (lgcc_to_fn X n x) = g (e x)) : left_group_chain_complex :=
+  -- left_group_chain_complex.mk Y @g
+  --   begin
+  --     intro n, apply equiv_rect (pequiv_of_equiv e), intro x,
+  --     refine ap g (p x)⁻¹ ⬝ _,
+  --     refine (p _)⁻¹ ⬝ _,
+  --     refine ap e (lgcc_is_chain_complex X _) ⬝ _,
+  --     exact respect_pt
+  --   end
+
+  -- definition is_exact_at_t_transfer {X : left_group_chain_complex} {Y : N → Type*}
+  --   {g : Π{n : N}, Y (S n) →* Y n} (e : Π{n}, X n ≃* Y n)
+  --   (p : Π{n} (x : X (S n)), e (lgcc_to_fn X n x) = g (e x)) {n : N}
+  --   (H : is_exact_at_lg X n) : is_exact_at_lg (transfer_left_group_chain_complex X @g @e @p) n :=
+  -- begin
+  --   intro y q, esimp at *,
+  --   assert H2 : lgcc_to_fn X n (e⁻¹ᵉ* y) = pt,
+  --   { refine (inv_commute (λn, equiv_of_pequiv e) _ _ @p _)⁻¹ᵖ ⬝ _,
+  --     refine ap _ q ⬝ _,
+  --     exact respect_pt e⁻¹ᵉ*},
+  --   cases (H _ H2) with x r,
+  --   refine image.mk (e x) _,
+  --   refine (p x)⁻¹ ⬝ _,
+  --   refine ap e r ⬝ _,
+  --   apply right_inv
+  -- end
+
+  -- TODO: move
+  definition is_trunc_ptrunctype [instance] {n : trunc_index} (X : ptrunctype n)
+    : is_trunc n (ptrunctype.to_pType X) :=
+  trunctype.struct X
+
+  /- a group where the point in the pointed corresponds with 1 in the group -/
+  structure pgroup [class] (X : Type*) extends semigroup X, has_inv X :=
+    (pt_mul : Πa, mul pt a = a)
+    (mul_pt : Πa, mul a pt = a)
+    (mul_left_inv_pt : Πa, mul (inv a) a = pt)
+
+  definition group_of_pgroup [reducible] [instance] (X : Type*) [H : pgroup X]
+    : group X :=
+  ⦃group, H,
+          one := pt,
+          one_mul := pgroup.pt_mul ,
+          mul_one := pgroup.mul_pt,
+          mul_left_inv := pgroup.mul_left_inv_pt⦄
+
+  definition pgroup_of_group (X : Type*) [H : group X] (p : one = pt :> X) : pgroup X :=
+  begin
+    cases X with X x, esimp at *, induction p,
+    exact ⦃pgroup, H,
+            pt_mul := one_mul,
+            mul_pt := mul_one,
+            mul_left_inv_pt := mul.left_inv⦄
+
+  end
+
+  definition is_embedding_of_trivial (X : chain_complex N) {n : N}
+    (H : is_exact_at X n) [HX : is_prop (X (S (S n)))]
+    [pgroup (X n)] [pgroup (X (S n))] [is_homomorphism (cc_to_fn X n)]
+      : is_embedding (cc_to_fn X n) :=
+  begin
+    apply is_embedding_homomorphism,
+    intro g p,
+    induction H g p with v,
+    induction v with x q,
+    assert r : pt = x, exact @is_prop.elim _ HX _ _,
+    induction r,
+    refine q⁻¹ ⬝ _,
+    apply respect_pt
+  end
+
+  definition is_surjective_of_trivial (X : chain_complex N) {n : N}
+    (H : is_exact_at X n) [HX : is_prop (X n)] : is_surjective (cc_to_fn X (S n)) :=
+  begin
+    intro g,
+    refine trunc.elim _ (H g (@is_prop.elim _ HX _ _)),
+    apply tr
+  end
+
+  definition is_equiv_of_trivial (X : chain_complex N) {n : N}
+    (H1 : is_exact_at X n) (H2 : is_exact_at X (S n))
+    [HX1 : is_prop (X n)] [HX2 : is_prop (X (S (S (S n))))]
+    [pgroup (X (S n))] [pgroup (X (S (S n)))] [is_homomorphism (cc_to_fn X (S n))]
+    : is_equiv (cc_to_fn X (S n)) :=
+  begin
+    apply is_equiv_of_is_surjective_of_is_embedding,
+    { apply is_embedding_of_trivial X, apply H2},
+    { apply is_surjective_of_trivial X, apply H1},
+  end
+
+  end
+
 end chain_complex
diff --git a/homotopy/fin.hlean b/homotopy/fin.hlean
new file mode 100644
index 0000000..990e01d
--- /dev/null
+++ b/homotopy/fin.hlean
@@ -0,0 +1,59 @@
+/-
+Copyright (c) 2016 Floris van Doorn. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Floris van Doorn
+
+Finite ordinal types.
+-/
+
+import types.fin
+
+open eq nat fin algebra
+
+inductive is_succ [class] : ℕ → Type :=
+| mk : Πn, is_succ (succ n)
+
+attribute is_succ.mk [instance]
+
+definition is_succ_add_right [instance] (n m : ℕ) [H : is_succ m] : is_succ (n+m) :=
+by induction H with m; constructor
+
+definition is_succ_add_left (n m : ℕ) [H : is_succ n] : is_succ (n+m) :=
+by induction H with n; cases m with m: constructor
+
+definition is_succ_bit0 [instance] (n : ℕ) [H : is_succ n] : is_succ (bit0 n) :=
+by induction H with n; constructor
+
+
+namespace fin
+
+  definition my_succ {n : ℕ} (x : fin n) : fin n :=
+  begin
+    cases n with n,
+    { exfalso, apply not_lt_zero _ (is_lt x)},
+    { exact
+      if H : val x = n
+        then fin.mk 0 !zero_lt_succ
+        else fin.mk (nat.succ (val x)) (succ_lt_succ (lt_of_le_of_ne (le_of_lt_succ (is_lt x)) H))}
+  end
+
+  protected definition add {n : ℕ} (x y : fin n) : fin n :=
+  iterate my_succ (val y) x
+
+  definition has_zero_fin [instance] (n : ℕ) [H : is_succ n] : has_zero (fin n) :=
+  by induction H with n; exact has_zero.mk (fin.zero n)
+
+  definition has_one_fin [instance] (n : ℕ) [H : is_succ n] : has_one (fin n) :=
+  by induction H with n; exact has_one.mk (my_succ (fin.zero n))
+
+  definition has_add_fin [instance] (n : ℕ) : has_add (fin n) :=
+  has_add.mk fin.add
+
+  -- definition my_succ_eq_zero {n : ℕ} (x : fin (nat.succ n)) (p : val x = n) : my_succ x = 0 :=
+  -- if H : val x = n
+  --   then fin.mk 0 !zero_lt_succ
+  --   else fin.mk (nat.succ (val x)) (succ_lt_succ (lt_of_le_of_ne (le_of_lt_succ (is_lt x)) H))
+
+
+
+end fin
diff --git a/homotopy/homotopy_groups.hlean b/homotopy/homotopy_groups.hlean
new file mode 100644
index 0000000..1bc2904
--- /dev/null
+++ b/homotopy/homotopy_groups.hlean
@@ -0,0 +1,97 @@
+/-
+Copyright (c) 2016 Floris van Doorn. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Floris van Doorn
+
+-/
+
+-- to be moved to algebra/homotopy_group in the Lean library
+
+import group_theory.basic algebra.homotopy_group
+
+open eq algebra pointed group trunc is_trunc nat algebra equiv equiv.ops is_equiv
+
+namespace my
+
+  section
+  variables {A B C : Type*}
+  definition apn_compose (n : ℕ) (g : B →* C) (f : A →* B) : apn n (g ∘* f) ~* apn n g ∘* apn n f :=
+  begin
+    induction n with n IH,
+    { reflexivity},
+    { refine ap1_phomotopy IH ⬝* _, apply ap1_compose}
+  end
+
+  theorem ap1_con (f : A →* B) (p q : Ω A) : ap1 f (p ⬝ q) = ap1 f p ⬝ ap1 f q :=
+  begin
+    rewrite [▸*, ap_con, +con.assoc, con_inv_cancel_left]
+  end
+
+  definition apn_con {n : ℕ} (f : A →* B) (p q : Ω[n + 1] A)
+    : apn (n+1) f (p ⬝ q) = apn (n+1) f p ⬝ apn (n+1) f q :=
+  ap1_con (apn n f) p q
+
+  definition tr_mul {n : ℕ} (p q : Ω[n + 1] A) : @mul (πg[n+1] A) _ (tr p ) (tr q) = tr (p ⬝ q) :=
+  by reflexivity
+  end
+
+  section
+
+    parameters {A B : Type} (f : A ≃ B) [group A]
+
+    definition group_equiv_mul (b b' : B) : B := f (f⁻¹ᶠ b * f⁻¹ᶠ b')
+
+    definition group_equiv_one : B := f one
+
+    definition group_equiv_inv (b : B) : B := f (f⁻¹ᶠ b)⁻¹
+
+    local infix * := my.group_equiv_mul f
+    local postfix ^ := my.group_equiv_inv f
+    local notation 1 := my.group_equiv_one f
+
+    theorem group_equiv_mul_assoc (b₁ b₂ b₃ : B) : (b₁ * b₂) * b₃ = b₁ * (b₂ * b₃) :=
+    by rewrite [↑group_equiv_mul, +left_inv f, mul.assoc]
+
+    theorem group_equiv_one_mul (b : B) : 1 * b = b :=
+    by rewrite [↑group_equiv_mul, ↑group_equiv_one, left_inv f, one_mul, right_inv f]
+
+    theorem group_equiv_mul_one (b : B) : b * 1 = b :=
+    by rewrite [↑group_equiv_mul, ↑group_equiv_one, left_inv f, mul_one, right_inv f]
+
+    theorem group_equiv_mul_left_inv (b : B) : b^ * b = 1 :=
+    by rewrite [↑group_equiv_mul, ↑group_equiv_one, ↑group_equiv_inv,
+                +left_inv f, mul.left_inv]
+
+    definition group_equiv_closed : group B :=
+    ⦃group,
+      mul          := group_equiv_mul,
+      mul_assoc    := group_equiv_mul_assoc,
+      one          := group_equiv_one,
+      one_mul      := group_equiv_one_mul,
+      mul_one      := group_equiv_mul_one,
+      inv          := group_equiv_inv,
+      mul_left_inv := group_equiv_mul_left_inv,
+    is_set_carrier := is_trunc_equiv_closed 0 f⦄
+
+  end
+
+end my open my
+
+namespace eq
+
+  local attribute mul [unfold 2]
+  definition homotopy_group_homomorphism [constructor] (n : ℕ) {A B : Type*} (f : A →* B)
+    : πg[n+1] A →g πg[n+1] B :=
+  begin
+    fconstructor,
+    { exact phomotopy_group_functor (n+1) f},
+    { intro g,
+      refine @trunc.rec _ _ _ (λx, !is_trunc_eq) _, intro h,
+      refine @trunc.rec _ _ _ (λx, !is_trunc_eq) _ g, clear g, intro g,
+      rewrite [tr_mul, ▸*],
+      apply ap tr, apply apn_con}
+  end
+
+  notation `π→g[`:95  n:0 ` +1] `:0 f:95 := homotopy_group_homomorphism n f
+
+end eq
diff --git a/homotopy/sec83.hlean b/homotopy/sec83.hlean
index d0ebeaf..8c5a634 100644
--- a/homotopy/sec83.hlean
+++ b/homotopy/sec83.hlean
@@ -2,48 +2,43 @@
 
 import types.trunc types.pointed homotopy.connectedness homotopy.sphere homotopy.circle algebra.group algebra.homotopy_group
 
-open eq is_trunc is_equiv nat equiv trunc function circle algebra pointed is_trunc.trunc_index homotopy
+open eq is_trunc is_equiv nat equiv trunc function circle algebra pointed trunc_index homotopy
 
-notation `Floris` := sorry
 
 -- Lemma 8.3.1
 
-definition homotopy_group_of_is_trunc (A : Type*) (n : ℕ) (p : is_trunc n A) : ∀(k : ℕ), πG[n+k+1] A = G0 :=
+theorem trivial_homotopy_group_of_is_trunc (A : Type*) (n k : ℕ) [is_trunc n A] (H : n ≤ k)
+  : is_contr (πg[k+1] A) :=
 begin
-  intro k,
-  apply @trivial_group_of_is_contr,
   apply is_trunc_trunc_of_is_trunc,
   apply is_contr_loop_of_is_trunc,
-  apply @is_trunc_of_leq A n _,
-  induction k with k IHk,
-  {
-    apply is_trunc.trunc_index.le.refl
-  },
-  {
-    induction n with n IHn,
-    {
-      constructor
-    },
-    {
-      exact Floris
-    }
-  }
+  apply @is_trunc_of_le A n _,
+  exact of_nat_le_of_nat H
 end
 
 -- Lemma 8.3.2
-definition trunc_trunc (n k : ℕ₋₂) (p : k ≤ n) (A : Type)
-  : trunc k (trunc n A) ≃ trunc k A :=
-sorry
-
-definition zero_trunc_of_iterated_loop_space (k : ℕ) (A : Type*)
-  : trunc 0 (Ω[k] A) ≃ Ω[k](pointed.MK (trunc k A) (tr pt)) := 
-sorry
-
-
-definition homotopy_group_of_is_conn (A : Type*) (n : ℕ) (p : is_conn n A) : ∀(k : ℕ), (k ≤ n) → is_contr(π[k] A) :=
+theorem trivial_homotopy_group_of_is_conn (A : Type*) {k n : ℕ} (H : k ≤ n) [is_conn n A]
+  : is_contr (π[k] A) :=
 begin
-  intros k H,
-  exact Floris
+    have H2 : of_nat k ≤ of_nat n, from of_nat_le_of_nat H,
+    have H3 : is_contr (ptrunc k A),
+    begin
+      fapply is_contr_equiv_closed,
+      { apply trunc_trunc_equiv_left _ k n H2}
+    end,
+    have H4 : is_contr (Ω[k](ptrunc k A)),
+      from !is_trunc_loop_of_is_trunc,
+    apply is_trunc_equiv_closed_rev,
+    { apply equiv_of_pequiv (phomotopy_group_pequiv_loop_ptrunc k A)}
 end
 
 -- Corollary 8.3.3
+open sphere.ops sphere_index
+theorem homotopy_group_sphere_le (n k : ℕ) (H : k < n) : is_contr (π[k] (S. n)) :=
+begin
+  cases n with n,
+  { exfalso, apply not_lt_zero, exact H},
+  { have H2 : k ≤ n, from le_of_lt_succ H,
+    apply @(trivial_homotopy_group_of_is_conn _ H2),
+    rewrite [-trunc_index.of_sphere_index_of_nat, -trunc_index.succ_sub_one], apply is_conn_sphere}
+end
diff --git a/homotopy/sec86.hlean b/homotopy/sec86.hlean
new file mode 100644
index 0000000..56fa15f
--- /dev/null
+++ b/homotopy/sec86.hlean
@@ -0,0 +1,45 @@
+
+
+import  homotopy.wedge types.pi
+
+open eq homotopy is_trunc pointed susp nat pi equiv equiv.ops is_equiv trunc
+
+section freudenthal
+
+parameters {A : Type*} (n : ℕ) [is_conn n A]
+
+--set_option pp.notation false
+
+protected definition my_wedge_extension.ext : Π {A : Type*} {B : Type*} (n m : ℕ) [cA : is_conn n (carrier A)] [cB : is_conn m (carrier B)]
+(P : carrier A → carrier B → (m+n)-Type) (f : Π (a : carrier A), trunctype.carrier (P a (Point B)))
+(g : Π (b : carrier B), trunctype.carrier (P (Point A) b)),
+  f (Point A) = g (Point B) → (Π (a : carrier A) (b : carrier B), trunctype.carrier (P a b)) :=
+sorry
+
+definition code_fun (a : A) (q : north = north :> susp A)
+  : trunc (n * 2) (fiber (pmap.to_fun (loop_susp_unit A)) q) → trunc (n * 2) (fiber merid (q ⬝ merid a)) :=
+begin
+  intro x, induction x with x,
+  esimp at *, cases x with a' p,
+--  apply my_wedge_extension.ext n n,
+  exact sorry
+end
+
+definition code (y : susp A) :  north = y → Type :=
+susp.rec_on y
+  (λp, trunc (2*n) (fiber (loop_susp_unit A) p))
+  (λq, trunc (2*n) (fiber merid q))
+  begin
+    intros,
+    apply arrow_pathover_constant_right,
+    intro q, rewrite [transport_eq_r],
+    apply ua,
+    exact sorry
+  end
+
+definition freudenthal_suspension  : is_conn_map (n*2) (loop_susp_unit A) :=
+sorry
+
+
+
+end freudenthal