Finish construction of the LES of homotopy groups without signs

The maps on every level are just the functorial action of the homotopy groups (possibly composed by a cast), but there are no compositions with path inversion.
There are also some updates in various files after changes in the HoTT library.

homotopy/LES.hlean

@@ -0,0 +1,389 @@
+import .LES_of_homotopy_groups
+open eq pointed is_trunc trunc_index trunc group is_equiv equiv algebra prod fin fiber nat
+     succ_str chain_complex
+
+/--------------
+    PART 3'
+ --------------/
+
+namespace chain_complex'
+
+  section
+  universe variable u
+  parameters {X Y : pType.{u}} (f : X →* Y)
+
+  definition homotopy_groups2 [reducible] : +3ℕ → Type*
+  | (n, fin.mk 0 H) := Ω[n] Y
+  | (n, fin.mk 1 H) := Ω[n] X
+  | (n, fin.mk k H) := Ω[n] (pfiber f)
+
+  definition homotopy_groups2_add1 (n : ℕ) : Π(x : fin (succ 2)),
+    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 (k+3) H) := begin exfalso, apply lt_le_antisymm H, apply le_add_left end
+
+  definition homotopy_groups_fun2 : Π(n : +3ℕ), homotopy_groups2 (S n) →* homotopy_groups2 n
+  | (n, fin.mk 0 H) := proof Ω→[n] f qed
+  | (n, fin.mk 1 H) := proof Ω→[n] (ppoint f) qed
+  | (n, fin.mk 2 H) :=
+    proof Ω→[n] (boundary_map f) ∘* pcast (loop_space_succ_eq_in Y n) qed
+  | (n, fin.mk (k+3) H) := begin exfalso, apply lt_le_antisymm H, apply le_add_left end
+
+  definition homotopy_groups_fun2_add1_0 (n : ℕ) (H : 0 < succ 2)
+    : homotopy_groups_fun2 (n+1, fin.mk 0 H) ~*
+      cast proof idp qed ap1 (homotopy_groups_fun2 (n, fin.mk 0 H)) :=
+  by reflexivity
+
+  definition homotopy_groups_fun2_add1_1 (n : ℕ) (H : 1 < succ 2)
+    : homotopy_groups_fun2 (n+1, fin.mk 1 H) ~*
+      cast proof idp qed ap1 (homotopy_groups_fun2 (n, fin.mk 1 H)) :=
+  by reflexivity
+
+  definition homotopy_groups_fun2_add1_2 (n : ℕ) (H : 2 < succ 2)
+    : homotopy_groups_fun2 (n+1, fin.mk 2 H) ~*
+      cast proof idp qed ap1 (homotopy_groups_fun2 (n, fin.mk 2 H)) :=
+  begin
+    esimp,
+    refine _ ⬝* !ap1_compose⁻¹*,
+    exact pwhisker_left _ !pcast_ap_loop_space,
+  end
+exit
+  definition nat_of_str_3S [unfold 2] [reducible]
+    : Π(x : stratified +ℕ 2), nat_of_str x + 1 = nat_of_str (@S (stratified +ℕ 2) 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 (k+3) H) := begin exfalso, apply lt_le_antisymm H, apply le_add_left end
+
+  definition homotopy_groups2_pequiv : Π(x : +3ℕ),
+    homotopy_groups (nat_of_str x) ≃* homotopy_groups2 x
+  |  (0,    (fin.mk 0 H))     := by reflexivity
+  |  (0,    (fin.mk 1 H))     := by reflexivity
+  |  (0,    (fin.mk 2 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_pequiv_loop,
+      rexact homotopy_groups2_pequiv (n, fin.mk 0 H)
+    end
+  | ((n+1), (fin.mk 1 H))     :=
+    begin
+      apply loop_pequiv_loop,
+      rexact homotopy_groups2_pequiv (n, fin.mk 1 H)
+    end
+  | ((n+1), (fin.mk 2 H))     :=
+    begin
+      apply loop_pequiv_loop,
+      rexact homotopy_groups2_pequiv (n, fin.mk 2 H)
+    end
+  | (n,     (fin.mk (k+3) H)) := begin exfalso, apply lt_le_antisymm H, apply le_add_left end
+--  | (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 (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_pequiv_loop x) !loopn_pequiv_loopn_rfl)⁻¹ _,
+          refine cast (ap (λx, _ ~* x) !loopn_pequiv_loopn_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_0 :
+    Π(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'

homotopy/LES2.hlean

@@ -0,0 +1,801 @@
+/-
+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
+
+We define the fiber sequence of a pointed map f : X →* Y. We mostly follow the proof in section 8.4
+of the book.
+
+PART 1:
+We define a sequence fiber_sequence as in Definition 8.4.3.
+It has types X(n) : Type*
+X(0)   := Y,
+X(1)   := X,
+X(n+1) := fiber (f(n))
+with functions f(n) : X(n+1) →* X(n)
+f(0)   := f
+f(n+1) := point (f(n)) [this is the first projection]
+We prove that this is an exact sequence.
+Then we prove Lemma 8.4.3, by showing that X(n+3) ≃* Ω(X(n)) and that this equivalence sends
+the pointed map f(n+3) to -Ω(f(n)), i.e. the composition of Ω(f(n)) with path inversion.
+Using this equivalence we get a boundary_map : Ω(Y) → pfiber f.
+
+PART 2:
+Now we can define a new fiber sequence X'(n) : Type*, and here we slightly diverge from the book.
+We define it as
+X'(0)   := Y,
+X'(1)   := X,
+X'(2)   := fiber f
+X'(n+3) := Ω(X'(n))
+with maps f'(n) : X'(n+1) →* X'(n)
+f'(0) := f
+f'(1) := point f
+f'(2) := boundary_map
+f'(n+3) := Ω(f'(n))
+
+This sequence is not equivalent to the previous sequence. The difference is in the signs.
+The sequence f has negative signs (i.e. is composed with the inverse maps) for n ≡ 3, 4, 5 mod 6.
+This sign information is captured by e : X'(n) ≃* X'(n) such that
+e(k)   := 1               for k = 0,1,2,3
+e(k+3) := Ω(e(k)) ∘ (-)⁻¹ for k > 0
+
+Now the sequence (X', f' ∘ e) is equivalent to (X, f), Hence (X', f' ∘ e) is an exact sequence.
+We then prove that (X', f') is an exact sequence by using that there are other equivalences
+eₗ and eᵣ such that
+f' = eᵣ ∘ f' ∘ e
+f' ∘ eₗ = e ∘ f'.
+(this fact is type_chain_complex_cancel_aut and is_exact_at_t_cancel_aut in the file chain_complex)
+eₗ and eᵣ are almost the same as e, except that the places where the inverse is taken is
+slightly shifted:
+eᵣ = (-)⁻¹ for n ≡ 3, 4, 5 mod 6                       and eᵣ = 1 otherwise
+e  = (-)⁻¹ for n ≡ 4, 5, 6 mod 6 (except for n = 0)    and e  = 1 otherwise
+eₗ = (-)⁻¹ for n ≡ 5, 6, 7 mod 6 (except for n = 0, 1) and eₗ = 1 otherwise
+
+PART 3:
+We change the type over which the sequence of types and maps are indexed from ℕ to ℕ × 3
+(where 3 is the finite type with 3 elements). The reason is that we have that X'(3n) = Ωⁿ(Y), but
+this equality is not definitionally true. Hence we cannot even state whether f'(3n) = Ωⁿ(f) without
+using transports. This gets ugly. However, if we use as index type ℕ × 3, we can do this. We can
+define
+Y : ℕ × 3 → Type* as
+Y(n, 0) := Ωⁿ(Y)
+Y(n, 1) := Ωⁿ(X)
+Y(n, 2) := Ωⁿ(fiber f)
+with maps g(n) : Y(S n) →* Y(n) (where the successor is defined in the obvious way)
+g(n, 0) := Ωⁿ(f)
+g(n, 1) := Ωⁿ(point f)
+g(n, 2) := Ωⁿ(boundary_map) ∘ cast
+
+Here "cast" is the transport over the equality Ωⁿ⁺¹(Y) = Ωⁿ(Ω(Y)). We show that the sequence
+(ℕ, X', f') is equivalent to (ℕ × 3, Y, g).
+
+PART 4:
+We get the long exact sequence of homotopy groups by taking the set-truncation of (Y, g).
+-/
+
+import .chain_complex algebra.homotopy_group
+
+open eq pointed sigma fiber equiv is_equiv sigma.ops is_trunc nat trunc algebra function sum
+
+section MOVE
+  -- TODO: MOVE
+  open group chain_complex
+  definition pinverse_pinverse (A : Type*) : pinverse ∘* pinverse ~* pid (Ω A) :=
+  begin
+    fapply phomotopy.mk,
+    { apply inv_inv},
+    { reflexivity}
+  end
+
+  definition to_pmap_pequiv_of_pmap {A B : Type*} (f : A →* B) (H : is_equiv f)
+    : pequiv.to_pmap (pequiv_of_pmap f H) = f :=
+  by cases f; reflexivity
+
+  definition to_pmap_pequiv_trans {A B C : Type*} (f : A ≃* B) (g : B ≃* C)
+    : pequiv.to_pmap (f ⬝e* g) = g ∘* f :=
+  !to_pmap_pequiv_of_pmap
+
+  definition pequiv_pinverse (A : Type*) : Ω A ≃* Ω A :=
+  pequiv_of_pmap pinverse !is_equiv_eq_inverse
+
+  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
+
+end MOVE
+
+/--------------
+    PART 1
+ --------------/
+
+namespace chain_complex
+
+  definition fiber_sequence_helper [constructor] (v : Σ(X Y : Type*), X →* Y)
+    : Σ(Z X : Type*), Z →* X :=
+  ⟨pfiber v.2.2, v.1, ppoint v.2.2⟩
+
+  definition fiber_sequence_helpern (v : Σ(X Y : Type*), X →* Y) (n : ℕ)
+    : Σ(Z X : Type*), Z →* X :=
+  iterate fiber_sequence_helper n v
+
+  section
+  universe variable u
+  parameters {X Y : pType.{u}} (f : X →* Y)
+  include f
+
+  definition fiber_sequence_carrier (n : ℕ) : Type* :=
+  (fiber_sequence_helpern ⟨X, Y, f⟩ n).2.1
+
+  definition fiber_sequence_fun (n : ℕ)
+    : fiber_sequence_carrier (n + 1) →* fiber_sequence_carrier n :=
+  (fiber_sequence_helpern ⟨X, Y, f⟩ n).2.2
+
+  /- Definition 8.4.3 -/
+  definition fiber_sequence : type_chain_complex.{0 u} +ℕ :=
+  begin
+    fconstructor,
+    { exact fiber_sequence_carrier},
+    { exact fiber_sequence_fun},
+    { intro n x, cases n with n,
+      { exact point_eq x},
+      { exact point_eq x}}
+  end
+
+  definition is_exact_fiber_sequence : is_exact_t fiber_sequence :=
+  λn x p, fiber.mk (fiber.mk x p) rfl
+
+  /- (generalization of) Lemma 8.4.4(i)(ii) -/
+  definition fiber_sequence_carrier_equiv (n : ℕ)
+    : fiber_sequence_carrier (n+3) ≃ Ω(fiber_sequence_carrier n) :=
+  calc
+    fiber_sequence_carrier (n+3) ≃ fiber (fiber_sequence_fun (n+1)) pt : erfl
+    ... ≃ Σ(x : fiber_sequence_carrier _), fiber_sequence_fun (n+1) x = pt
+      : fiber.sigma_char
+    ... ≃ Σ(x : fiber (fiber_sequence_fun n) pt), fiber_sequence_fun _ x = pt
+      : erfl
+    ... ≃ Σ(v : Σ(x : fiber_sequence_carrier _), fiber_sequence_fun _ x = pt),
+            fiber_sequence_fun _ (fiber.mk v.1 v.2) = pt
+      : by exact sigma_equiv_sigma !fiber.sigma_char (λa, erfl)
+    ... ≃ Σ(v : Σ(x : fiber_sequence_carrier _), fiber_sequence_fun _ x = pt),
+            v.1 = pt
+      : erfl
+    ... ≃ Σ(v : Σ(x : fiber_sequence_carrier _), x = pt),
+            fiber_sequence_fun _ v.1 = pt
+      : sigma_assoc_comm_equiv
+    ... ≃ fiber_sequence_fun _ !center.1 = pt
+      : @(sigma_equiv_of_is_contr_left _) !is_contr_sigma_eq'
+    ... ≃ fiber_sequence_fun _ pt = pt
+      : erfl
+    ... ≃ pt = pt
+      : by exact !equiv_eq_closed_left !respect_pt
+    ... ≃ Ω(fiber_sequence_carrier n) : erfl
+
+  /- computation rule -/
+  definition fiber_sequence_carrier_equiv_eq (n : ℕ)
+    (x : fiber_sequence_carrier (n+1)) (p : fiber_sequence_fun n x = pt)
+    (q : fiber_sequence_fun (n+1) (fiber.mk x p) = pt)
+    : fiber_sequence_carrier_equiv n (fiber.mk (fiber.mk x p) q)
+      = !respect_pt⁻¹ ⬝ ap (fiber_sequence_fun n) q⁻¹ ⬝ p :=
+  begin
+    refine _ ⬝ !con.assoc⁻¹,
+    apply whisker_left,
+    refine transport_eq_Fl _ _ ⬝ _,
+    apply whisker_right,
+    refine inverse2 !ap_inv ⬝ !inv_inv ⬝ _,
+    refine ap_compose (fiber_sequence_fun n) pr₁ _ ⬝
+           ap02 (fiber_sequence_fun n) !ap_pr1_center_eq_sigma_eq',
+  end
+
+  definition fiber_sequence_carrier_equiv_inv_eq (n : ℕ)
+    (p : Ω(fiber_sequence_carrier n)) : (fiber_sequence_carrier_equiv n)⁻¹ᵉ p =
+      fiber.mk (fiber.mk pt (respect_pt (fiber_sequence_fun n) ⬝ p)) idp :=
+  begin
+    apply inv_eq_of_eq,
+    refine _ ⬝ !fiber_sequence_carrier_equiv_eq⁻¹, esimp,
+    exact !inv_con_cancel_left⁻¹
+  end
+
+  definition fiber_sequence_carrier_pequiv (n : ℕ)
+    : fiber_sequence_carrier (n+3) ≃* Ω(fiber_sequence_carrier n) :=
+  pequiv_of_equiv (fiber_sequence_carrier_equiv n)
+    begin
+      esimp,
+      apply con.left_inv
+    end
+
+  definition fiber_sequence_carrier_pequiv_eq (n : ℕ)
+    (x : fiber_sequence_carrier (n+1)) (p : fiber_sequence_fun n x = pt)
+    (q : fiber_sequence_fun (n+1) (fiber.mk x p) = pt)
+    : fiber_sequence_carrier_pequiv n (fiber.mk (fiber.mk x p) q)
+      = !respect_pt⁻¹ ⬝ ap (fiber_sequence_fun n) q⁻¹ ⬝ p :=
+  fiber_sequence_carrier_equiv_eq n x p q
+
+  definition fiber_sequence_carrier_pequiv_inv_eq (n : ℕ)
+    (p : Ω(fiber_sequence_carrier n)) : (fiber_sequence_carrier_pequiv n)⁻¹ᵉ* p =
+      fiber.mk (fiber.mk pt (respect_pt (fiber_sequence_fun n) ⬝ p)) idp :=
+  by rexact fiber_sequence_carrier_equiv_inv_eq n p
+
+  /- Lemma 8.4.4(iii) -/
+  definition fiber_sequence_fun_eq_helper (n : ℕ)
+    (p : Ω(fiber_sequence_carrier (n + 1))) :
+    fiber_sequence_carrier_pequiv n
+      (fiber_sequence_fun (n + 3)
+        ((fiber_sequence_carrier_pequiv (n + 1))⁻¹ᵉ* p)) =
+          ap1 (fiber_sequence_fun n) p⁻¹ :=
+  begin
+    refine ap (λx, fiber_sequence_carrier_pequiv n (fiber_sequence_fun (n + 3) x))
+              (fiber_sequence_carrier_pequiv_inv_eq (n+1) p) ⬝ _,
+    /- the following three lines are rewriting some reflexivities: -/
+    -- replace (n + 3) with (n + 2 + 1),
+    -- refine ap (fiber_sequence_carrier_pequiv n)
+    --           (fiber_sequence_fun_eq1 (n+2) _ idp) ⬝ _,
+    refine fiber_sequence_carrier_pequiv_eq n pt (respect_pt (fiber_sequence_fun n)) _ ⬝ _,
+    esimp,
+    apply whisker_right,
+    apply whisker_left,
+    apply ap02, apply inverse2, apply idp_con,
+  end
+
+  theorem fiber_sequence_carrier_pequiv_eq_point_eq_idp (n : ℕ) :
+    fiber_sequence_carrier_pequiv_eq n
+      (Point (fiber_sequence_carrier (n+1)))
+      (respect_pt (fiber_sequence_fun n))
+      (respect_pt (fiber_sequence_fun (n + 1))) = idp :=
+  begin
+    apply con_inv_eq_idp,
+    refine ap (λx, whisker_left _ (_ ⬝ x)) _ ⬝ _,
+    { reflexivity},
+    { reflexivity},
+    refine ap (whisker_left _)
+              (transport_eq_Fl_idp_left (fiber_sequence_fun n)
+                                        (respect_pt (fiber_sequence_fun n))) ⬝ _,
+    apply whisker_left_idp_con_eq_assoc
+  end
+
+  theorem fiber_sequence_fun_phomotopy_helper (n : ℕ) :
+    (fiber_sequence_carrier_pequiv n ∘*
+      fiber_sequence_fun (n + 3)) ∘*
+        (fiber_sequence_carrier_pequiv (n + 1))⁻¹ᵉ* ~*
+          ap1 (fiber_sequence_fun n) ∘* pinverse :=
+  begin
+    fapply phomotopy.mk,
+    { exact chain_complex.fiber_sequence_fun_eq_helper f n},
+    { esimp, rewrite [idp_con], refine _ ⬝ whisker_left _ !idp_con⁻¹,
+      apply whisker_right,
+      apply whisker_left,
+      exact chain_complex.fiber_sequence_carrier_pequiv_eq_point_eq_idp f n}
+  end
+
+  theorem fiber_sequence_fun_eq (n : ℕ) : Π(x : fiber_sequence_carrier (n + 4)),
+    fiber_sequence_carrier_pequiv n (fiber_sequence_fun (n + 3) x) =
+      ap1 (fiber_sequence_fun n) (fiber_sequence_carrier_pequiv (n + 1) x)⁻¹ :=
+  begin
+    apply homotopy_of_inv_homotopy_pre (fiber_sequence_carrier_pequiv (n + 1)),
+    apply fiber_sequence_fun_eq_helper n
+  end
+
+  theorem fiber_sequence_fun_phomotopy (n : ℕ) :
+    fiber_sequence_carrier_pequiv n ∘*
+      fiber_sequence_fun (n + 3) ~*
+          (ap1 (fiber_sequence_fun n) ∘* pinverse) ∘* fiber_sequence_carrier_pequiv (n + 1) :=
+  begin
+    apply phomotopy_of_pinv_right_phomotopy,
+    apply fiber_sequence_fun_phomotopy_helper
+  end
+
+  definition boundary_map : Ω Y →* pfiber f :=
+  fiber_sequence_fun 2 ∘* (fiber_sequence_carrier_pequiv 0)⁻¹ᵉ*
+
+/--------------
+    PART 2
+ --------------/
+
+  /- Now we are ready to define the long exact sequence of homotopy groups.
+     First we define its carrier -/
+  definition loop_spaces : ℕ → Type*
+  | 0     := Y
+  | 1     := X
+  | 2     := pfiber f
+  | (k+3) := Ω (loop_spaces k)
+
+  /- The maps between the homotopy groups -/
+  definition loop_spaces_fun
+    : Π(n : ℕ), loop_spaces (n+1) →* loop_spaces n
+  | 0     := proof f qed
+  | 1     := proof ppoint f qed
+  | 2     := proof boundary_map qed
+  | (k+3) := proof ap1 (loop_spaces_fun k) qed
+
+  definition loop_spaces_fun_add3 [unfold_full] (n : ℕ) :
+    loop_spaces_fun (n + 3) = ap1 (loop_spaces_fun n) :=
+  proof idp qed
+
+  definition fiber_sequence_pequiv_loop_spaces :
+    Πn, fiber_sequence_carrier n ≃* loop_spaces n
+  | 0     := by reflexivity
+  | 1     := by reflexivity
+  | 2     := by reflexivity
+  | (k+3) :=
+    begin
+      refine fiber_sequence_carrier_pequiv k ⬝e* _,
+      apply loop_pequiv_loop,
+      exact fiber_sequence_pequiv_loop_spaces k
+    end
+
+  definition fiber_sequence_pequiv_loop_spaces_add3 (n : ℕ)
+    : fiber_sequence_pequiv_loop_spaces (n + 3) =
+      ap1 (fiber_sequence_pequiv_loop_spaces n) ∘* fiber_sequence_carrier_pequiv n :=
+  by reflexivity
+
+  definition fiber_sequence_pequiv_loop_spaces_3_phomotopy
+    : fiber_sequence_pequiv_loop_spaces 3 ~* proof fiber_sequence_carrier_pequiv nat.zero qed :=
+  begin
+    refine pwhisker_right _ ap1_id ⬝* _,
+    apply pid_comp
+  end
+
+  definition pid_or_pinverse : Π(n : ℕ), loop_spaces n ≃* loop_spaces n
+  | 0     := pequiv.rfl
+  | 1     := pequiv.rfl
+  | 2     := pequiv.rfl
+  | 3     := pequiv.rfl
+  | (k+4) := !pequiv_pinverse ⬝e* loop_pequiv_loop (pid_or_pinverse (k+1))
+
+  definition pid_or_pinverse_add4 (n : ℕ)
+    : pid_or_pinverse (n + 4) = !pequiv_pinverse ⬝e* loop_pequiv_loop (pid_or_pinverse (n + 1)) :=
+  by reflexivity
+
+  definition pid_or_pinverse_add4_rev : Π(n : ℕ),
+    pid_or_pinverse (n + 4) ~* pinverse ∘* Ω→(pid_or_pinverse (n + 1))
+  | 0     := begin rewrite [pid_or_pinverse_add4, + to_pmap_pequiv_trans],
+                   replace pid_or_pinverse (0 + 1) with pequiv.refl X,
+                   rewrite [loop_pequiv_loop_rfl, ▸*], refine !pid_comp ⬝* _,
+                   exact !comp_pid⁻¹* ⬝* pwhisker_left _ !ap1_id⁻¹* end
+  | 1     := begin rewrite [pid_or_pinverse_add4, + to_pmap_pequiv_trans],
+                   replace pid_or_pinverse (1 + 1) with pequiv.refl (pfiber f),
+                   rewrite [loop_pequiv_loop_rfl, ▸*], refine !pid_comp ⬝* _,
+                   exact !comp_pid⁻¹* ⬝* pwhisker_left _ !ap1_id⁻¹* end
+  | 2     := begin rewrite [pid_or_pinverse_add4, + to_pmap_pequiv_trans],
+                   replace pid_or_pinverse (2 + 1) with pequiv.refl (Ω Y),
+                   rewrite [loop_pequiv_loop_rfl, ▸*], refine !pid_comp ⬝* _,
+                   exact !comp_pid⁻¹* ⬝* pwhisker_left _ !ap1_id⁻¹* end
+  | (k+3) :=
+    begin
+      replace (k + 3 + 1) with (k + 4),
+      rewrite [+ pid_or_pinverse_add4, + to_pmap_pequiv_trans],
+      refine _ ⬝* pwhisker_left _ !ap1_compose⁻¹*,
+      refine _ ⬝* !passoc,
+      apply pconcat2,
+      { refine ap1_phomotopy (pid_or_pinverse_add4_rev k) ⬝* _,
+        refine !ap1_compose ⬝* _, apply pwhisker_right, apply ap1_pinverse},
+      { refine !ap1_pinverse⁻¹*}
+    end
+
+  theorem fiber_sequence_phomotopy_loop_spaces : Π(n : ℕ),
+    fiber_sequence_pequiv_loop_spaces n ∘* fiber_sequence_fun n ~*
+      (loop_spaces_fun n ∘* pid_or_pinverse (n + 1)) ∘* fiber_sequence_pequiv_loop_spaces (n + 1)
+  | 0     := proof proof phomotopy.rfl qed ⬝* pwhisker_right _ !comp_pid⁻¹* qed
+  | 1     := by reflexivity
+  | 2     :=
+    begin
+      refine !pid_comp ⬝* _,
+      replace loop_spaces_fun 2 with boundary_map,
+      refine _ ⬝* pwhisker_left _ fiber_sequence_pequiv_loop_spaces_3_phomotopy⁻¹*,
+      apply phomotopy_of_pinv_right_phomotopy,
+      exact !pid_comp⁻¹*
+    end
+  | (k+3) :=
+    begin
+      replace (k + 3 + 1) with (k + 1 + 3),
+      rewrite [fiber_sequence_pequiv_loop_spaces_add3 k,
+               fiber_sequence_pequiv_loop_spaces_add3 (k+1)],
+      refine !passoc ⬝* _,
+      refine pwhisker_left _ (fiber_sequence_fun_phomotopy k) ⬝* _,
+      refine !passoc⁻¹* ⬝* _ ⬝* !passoc,
+      apply pwhisker_right,
+      replace (k + 1 + 3) with (k + 4),
+      xrewrite [loop_spaces_fun_add3, pid_or_pinverse_add4, to_pmap_pequiv_trans],
+      refine _ ⬝* !passoc⁻¹*,
+      refine _ ⬝* pwhisker_left _ !passoc⁻¹*,
+      refine _ ⬝* pwhisker_left _ (pwhisker_left _ !ap1_compose_pinverse),
+      refine !passoc⁻¹* ⬝* _ ⬝* !passoc ⬝* !passoc,
+      apply pwhisker_right,
+      refine !ap1_compose⁻¹* ⬝* _ ⬝* !ap1_compose ⬝* pwhisker_right _ !ap1_compose,
+      apply ap1_phomotopy,
+      exact fiber_sequence_phomotopy_loop_spaces k
+    end
+
+  definition pid_or_pinverse_right : Π(n : ℕ), loop_spaces n →* loop_spaces n
+  | 0     := !pid
+  | 1     := !pid
+  | 2     := !pid
+  | (k+3) := Ω→(pid_or_pinverse_right k) ∘* pinverse
+
+  definition pid_or_pinverse_left : Π(n : ℕ), loop_spaces n →* loop_spaces n
+  | 0     := pequiv.rfl
+  | 1     := pequiv.rfl
+  | 2     := pequiv.rfl
+  | 3     := pequiv.rfl
+  | 4     := pequiv.rfl
+  | (k+5) := Ω→(pid_or_pinverse_left (k+2)) ∘* pinverse
+
+  definition pid_or_pinverse_right_add3 (n : ℕ)
+    : pid_or_pinverse_right (n + 3) = Ω→(pid_or_pinverse_right n) ∘* pinverse :=
+  by reflexivity
+
+  definition pid_or_pinverse_left_add5 (n : ℕ)
+    : pid_or_pinverse_left (n + 5) = Ω→(pid_or_pinverse_left (n+2)) ∘* pinverse :=
+  by reflexivity
+
+  theorem pid_or_pinverse_commute_right : Π(n : ℕ),
+    loop_spaces_fun n ~* pid_or_pinverse_right n ∘* loop_spaces_fun n ∘* pid_or_pinverse (n + 1)
+  | 0     := proof !comp_pid⁻¹* ⬝* !pid_comp⁻¹* qed
+  | 1     := proof !comp_pid⁻¹* ⬝* !pid_comp⁻¹* qed
+  | 2     := proof !comp_pid⁻¹* ⬝* !pid_comp⁻¹* qed
+  | (k+3) :=
+    begin
+      replace (k + 3 + 1) with (k + 4),
+      rewrite [pid_or_pinverse_right_add3, loop_spaces_fun_add3],
+      refine _ ⬝* pwhisker_left _ (pwhisker_left _ !pid_or_pinverse_add4_rev⁻¹*),
+      refine ap1_phomotopy (pid_or_pinverse_commute_right k) ⬝* _,
+      refine !ap1_compose ⬝* _ ⬝* !passoc⁻¹*,
+      apply pwhisker_left,
+      refine !ap1_compose ⬝* _ ⬝* !passoc ⬝* !passoc,
+      apply pwhisker_right,
+      refine _ ⬝* pwhisker_right _ !ap1_compose_pinverse,
+      refine _ ⬝* !passoc⁻¹*,
+      refine !comp_pid⁻¹* ⬝* pwhisker_left _ _,
+      symmetry, apply pinverse_pinverse
+    end
+
+  theorem pid_or_pinverse_commute_left : Π(n : ℕ),
+    loop_spaces_fun n ∘* pid_or_pinverse_left (n + 1) ~* pid_or_pinverse n ∘* loop_spaces_fun n
+  | 0     := proof !comp_pid ⬝* !pid_comp⁻¹* qed
+  | 1     := proof !comp_pid ⬝* !pid_comp⁻¹* qed
+  | 2     := proof !comp_pid ⬝* !pid_comp⁻¹* qed
+  | 3     := proof !comp_pid ⬝* !pid_comp⁻¹* qed
+  | (k+4) :=
+    begin
+      replace (k + 4 + 1) with (k + 5),
+      rewrite [pid_or_pinverse_left_add5, pid_or_pinverse_add4, to_pmap_pequiv_trans],
+      replace (k + 4) with (k + 1 + 3),
+      rewrite [loop_spaces_fun_add3],
+      refine !passoc⁻¹* ⬝* _ ⬝* !passoc⁻¹*,
+      refine _ ⬝* pwhisker_left _ !ap1_compose_pinverse,
+      refine _ ⬝* !passoc,
+      apply pwhisker_right,
+      refine !ap1_compose⁻¹* ⬝* _ ⬝* !ap1_compose,
+      exact ap1_phomotopy (pid_or_pinverse_commute_left (k+1))
+    end
+
+  definition LES_of_loop_spaces' [constructor] : type_chain_complex +ℕ :=
+  transfer_type_chain_complex
+    fiber_sequence
+    (λn, loop_spaces_fun n ∘* pid_or_pinverse (n + 1))
+    fiber_sequence_pequiv_loop_spaces
+    fiber_sequence_phomotopy_loop_spaces
+
+  definition LES_of_loop_spaces [constructor] : type_chain_complex +ℕ :=
+  type_chain_complex_cancel_aut
+    LES_of_loop_spaces'
+    loop_spaces_fun
+    pid_or_pinverse
+    pid_or_pinverse_right
+    (λn x, idp)
+    pid_or_pinverse_commute_right
+
+  definition is_exact_LES_of_loop_spaces : is_exact_t LES_of_loop_spaces :=
+  begin
+    intro n,
+    refine is_exact_at_t_cancel_aut n pid_or_pinverse_left _ _ pid_or_pinverse_commute_left _,
+    apply is_exact_at_t_transfer,
+    apply is_exact_fiber_sequence
+  end
+
+  open prod succ_str fin
+
+  /--------------
+      PART 3
+   --------------/
+
+  definition loop_spaces2 [reducible] : +3ℕ → Type*
+  | (n, fin.mk 0 H) := Ω[n] Y
+  | (n, fin.mk 1 H) := Ω[n] X
+  | (n, fin.mk k H) := Ω[n] (pfiber f)
+
+  definition loop_spaces2_add1 (n : ℕ) : Π(x : fin (nat.succ 2)),
+    loop_spaces2 (n+1, x) = Ω (loop_spaces2 (n, x))
+  | (fin.mk 0 H) := by reflexivity
+  | (fin.mk 1 H) := by reflexivity
+  | (fin.mk 2 H) := by reflexivity
+  | (fin.mk (k+3) H) := begin exfalso, apply lt_le_antisymm H, apply le_add_left end
+
+  definition loop_spaces_fun2 : Π(n : +3ℕ), loop_spaces2 (S n) →* loop_spaces2 n
+  | (n, fin.mk 0 H) := proof Ω→[n] f qed
+  | (n, fin.mk 1 H) := proof Ω→[n] (ppoint f) qed
+  | (n, fin.mk 2 H) := proof Ω→[n] boundary_map ∘* pcast (loop_space_succ_eq_in Y n) qed
+  | (n, fin.mk (k+3) H) := begin exfalso, apply lt_le_antisymm H, apply le_add_left end
+
+  definition loop_spaces_fun2_add1_0 (n : ℕ) (H : 0 < succ 2)
+    : loop_spaces_fun2 (n+1, fin.mk 0 H) ~*
+      cast proof idp qed ap1 (loop_spaces_fun2 (n, fin.mk 0 H)) :=
+  by reflexivity
+
+  definition loop_spaces_fun2_add1_1 (n : ℕ) (H : 1 < succ 2)
+    : loop_spaces_fun2 (n+1, fin.mk 1 H) ~*
+      cast proof idp qed ap1 (loop_spaces_fun2 (n, fin.mk 1 H)) :=
+  by reflexivity
+
+  definition loop_spaces_fun2_add1_2 (n : ℕ) (H : 2 < succ 2)
+    : loop_spaces_fun2 (n+1, fin.mk 2 H) ~*
+      cast proof idp qed ap1 (loop_spaces_fun2 (n, fin.mk 2 H)) :=
+  begin
+    esimp,
+    refine _ ⬝* !ap1_compose⁻¹*,
+    apply pwhisker_left,
+    apply 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_3S [unfold 2] [reducible]
+    : Π(x : stratified +ℕ 2), nat_of_str x + 1 = nat_of_str (@S (stratified +ℕ 2) 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 (k+3) 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 3 times the same,
+    so maybe this can be simplified
+  -/
+  definition loop_spaces2_pequiv' : Π(n : ℕ) (x : fin (nat.succ 2)),
+    loop_spaces (nat_of_str (n, x)) ≃* loop_spaces2 (n, x)
+  |  0    (fin.mk 0 H)     := by reflexivity
+  |  0    (fin.mk 1 H)     := by reflexivity
+  |  0    (fin.mk 2 H)     := by reflexivity
+  | (n+1) (fin.mk 0 H)     :=
+    begin
+      apply loop_pequiv_loop,
+      rexact loop_spaces2_pequiv' n (fin.mk 0 H)
+    end
+  | (n+1) (fin.mk 1 H)     :=
+    begin
+      apply loop_pequiv_loop,
+      rexact loop_spaces2_pequiv' n (fin.mk 1 H)
+    end
+  | (n+1) (fin.mk 2 H)     :=
+    begin
+      apply loop_pequiv_loop,
+      rexact loop_spaces2_pequiv' n (fin.mk 2 H)
+    end
+  | n     (fin.mk (k+3) H) := begin exfalso, apply lt_le_antisymm H, apply le_add_left end
+
+  definition loop_spaces2_pequiv : Π(x : +3ℕ),
+    loop_spaces (nat_of_str x) ≃* loop_spaces2 x
+  | (n, x) := loop_spaces2_pequiv' n x
+
+  local attribute loop_pequiv_loop [reducible]
+  /- all cases where n>0 are basically the same -/
+  definition loop_spaces_fun2_phomotopy (x : +3ℕ) :
+    loop_spaces2_pequiv x ∘* loop_spaces_fun (nat_of_str x) ~*
+      (loop_spaces_fun2 x ∘* loop_spaces2_pequiv (S x))
+    ∘* pcast (ap (loop_spaces) (nat_of_str_3S 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 2,
+    { /-k=0-/
+      induction n with n IH,
+      { refine !pid_comp ⬝* _ ⬝* !comp_pid⁻¹* ⬝* !comp_pid⁻¹*,
+        reflexivity},
+      { refine _ ⬝* !comp_pid⁻¹*,
+        refine _ ⬝* pwhisker_right _ !loop_spaces_fun2_add1_0⁻¹*,
+        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 _ !loop_spaces_fun2_add1_1⁻¹*,
+        refine !ap1_compose⁻¹* ⬝* _ ⬝* !ap1_compose, apply ap1_phomotopy,
+        exact IH ⬝* !comp_pid}},
+    { /-k=2-/
+      induction n with n IH,
+      { refine !pid_comp ⬝* _ ⬝* !comp_pid⁻¹*,
+        refine !comp_pid⁻¹* ⬝* pconcat2 _ _,
+        { exact (comp_pid (chain_complex.boundary_map f))⁻¹*},
+        { refine cast (ap (λx, _ ~* x) !loop_pequiv_loop_rfl)⁻¹ _, reflexivity}},
+      { refine _ ⬝* !comp_pid⁻¹*,
+        refine _ ⬝* pwhisker_right _ !loop_spaces_fun2_add1_2⁻¹*,
+        refine !ap1_compose⁻¹* ⬝* _ ⬝* !ap1_compose, apply ap1_phomotopy,
+        exact IH ⬝* !comp_pid}},
+    { /-k=k'+3-/ exfalso, apply lt_le_antisymm H, apply le_add_left}
+  end
+
+  definition LES_of_loop_spaces2 [constructor] : type_chain_complex +3ℕ :=
+  transfer_type_chain_complex2
+    LES_of_loop_spaces
+    !fin_prod_nat_equiv_nat
+    nat_of_str_3S
+    @loop_spaces_fun2
+    @loop_spaces2_pequiv
+    begin
+      intro m x,
+      refine loop_spaces_fun2_phomotopy m x ⬝ _,
+      apply ap (loop_spaces_fun2 m), apply ap (loop_spaces2_pequiv (S m)),
+      esimp, exact ap010 cast !ap_compose⁻¹ x
+    end
+
+  definition is_exact_LES_of_loop_spaces2 : is_exact_t LES_of_loop_spaces2 :=
+  begin
+    intro n,
+    apply is_exact_at_transfer2,
+    apply is_exact_LES_of_loop_spaces
+  end
+
+  definition LES_of_homotopy_groups' [constructor] : chain_complex +3ℕ :=
+  trunc_chain_complex LES_of_loop_spaces2
+
+/--------------
+    PART 4
+ --------------/
+
+  definition homotopy_groups [reducible] : +3ℕ → Set*
+  | (n, fin.mk 0 H) := π*[n] Y
+  | (n, fin.mk 1 H) := π*[n] X
+  | (n, fin.mk k H) := π*[n] (pfiber f)
+
+  definition homotopy_groups_pequiv_loop_spaces2 [reducible]
+    : Π(n : +3ℕ), ptrunc 0 (loop_spaces2 n) ≃* homotopy_groups 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 (k+3) H) := begin exfalso, apply lt_le_antisymm H, apply le_add_left end
+
+  definition homotopy_groups_fun : Π(n : +3ℕ), homotopy_groups (S n) →* homotopy_groups n
+  | (n, fin.mk 0 H) := proof π→*[n] f qed
+  | (n, fin.mk 1 H) := proof π→*[n] (ppoint f) qed
+  | (n, fin.mk 2 H) :=
+    proof π→*[n] boundary_map ∘* pcast (ap (ptrunc 0) (loop_space_succ_eq_in Y n)) qed
+  | (n, fin.mk (k+3) H) := begin exfalso, apply lt_le_antisymm H, apply le_add_left end
+
+  definition homotopy_groups_fun_phomotopy_loop_spaces_fun2 [reducible]
+    : Π(n : +3ℕ), homotopy_groups_pequiv_loop_spaces2 n ∘* ptrunc_functor 0 (loop_spaces_fun2 n) ~*
+      homotopy_groups_fun n ∘* homotopy_groups_pequiv_loop_spaces2 (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 (k+3) H) := begin exfalso, apply lt_le_antisymm H, apply le_add_left end
+
+  definition LES_of_homotopy_groups [constructor] : chain_complex +3ℕ :=
+  transfer_chain_complex
+    LES_of_homotopy_groups'
+    homotopy_groups_fun
+    homotopy_groups_pequiv_loop_spaces2
+    homotopy_groups_fun_phomotopy_loop_spaces_fun2
+
+  definition is_exact_LES_of_homotopy_groups : is_exact LES_of_homotopy_groups :=
+  begin
+    intro n,
+    apply is_exact_at_transfer,
+    apply is_exact_at_trunc,
+    apply is_exact_LES_of_loop_spaces2
+  end
+
+  variable (n : ℕ)
+
+  /- the carrier of the fiber sequence is definitionally what we want (as pointed sets) -/
+  example : LES_of_homotopy_groups (str_of_nat 6)  = π*[2] Y          :> Set* := by reflexivity
+  example : LES_of_homotopy_groups (str_of_nat 7)  = π*[2] X          :> Set* := by reflexivity
+  example : LES_of_homotopy_groups (str_of_nat 8)  = π*[2] (pfiber f) :> Set* := by reflexivity
+  example : LES_of_homotopy_groups (str_of_nat 9)  = π*[3] Y          :> Set* := by reflexivity
+  example : LES_of_homotopy_groups (str_of_nat 10) = π*[3] X          :> Set* := by reflexivity
+  example : LES_of_homotopy_groups (str_of_nat 11) = π*[3] (pfiber f) :> Set* := by reflexivity
+
+  definition LES_of_homotopy_groups_0 : LES_of_homotopy_groups (n, 0) = π*[n] Y :=
+  by reflexivity
+  definition LES_of_homotopy_groups_1 : LES_of_homotopy_groups (n, 1) = π*[n] X :=
+  by reflexivity
+  definition LES_of_homotopy_groups_2 : LES_of_homotopy_groups (n, 2) = π*[n] (pfiber f) :=
+  by reflexivity
+
+  /- the functions of the fiber sequence is definitionally what we want (as pointed function).
+      -/
+
+  definition LES_of_homotopy_groups_fun_0 :
+    cc_to_fn LES_of_homotopy_groups (n, 0) = π→*[n] f :=
+  by reflexivity
+  definition LES_of_homotopy_groups_fun_1 :
+    cc_to_fn LES_of_homotopy_groups (n, 1) = π→*[n] (ppoint f) :=
+  by reflexivity
+  definition LES_of_homotopy_groups_fun_2 : cc_to_fn LES_of_homotopy_groups (n, 2) =
+    π→*[n] boundary_map ∘* pcast (ap (ptrunc 0) (loop_space_succ_eq_in Y n)) :=
+  by reflexivity
+
+  open group
+
+  definition group_LES_of_homotopy_groups_0
+    : Π(x : fin (succ 2)), group (LES_of_homotopy_groups (1, x))
+  | (fin.mk 0     H) := begin rexact group_homotopy_group 0 Y end
+  | (fin.mk 1     H) := begin rexact group_homotopy_group 0 X end
+  | (fin.mk 2     H) := begin rexact group_homotopy_group 0 (pfiber f) end
+  | (fin.mk (k+3) H) := begin exfalso, apply lt_le_antisymm H, apply le_add_left end
+
+  definition comm_group_LES_of_homotopy_groups (n : ℕ) : Π(x : fin (succ 2)),
+    comm_group (LES_of_homotopy_groups (n + 2, x))
+  | (fin.mk 0 H) := proof comm_group_homotopy_group n Y qed
+  | (fin.mk 1 H) := proof comm_group_homotopy_group n X qed
+  | (fin.mk 2 H) := proof comm_group_homotopy_group n (pfiber f) qed
+  | (fin.mk (k+3) H) := begin exfalso, apply lt_le_antisymm H, apply le_add_left end
+
+  definition CommGroup_LES_of_homotopy_groups (n : +3ℕ) : CommGroup.{u} :=
+  CommGroup.mk (LES_of_homotopy_groups (pr1 n + 2, pr2 n))
+               (comm_group_LES_of_homotopy_groups (pr1 n) (pr2 n))
+
+  definition homomorphism_LES_of_homotopy_groups_fun : Π(k : +3ℕ),
+    CommGroup_LES_of_homotopy_groups (S k) →g CommGroup_LES_of_homotopy_groups k
+  | (k, fin.mk 0 H) :=
+    proof homomorphism.mk (cc_to_fn LES_of_homotopy_groups (k + 2, 0))
+                          (phomotopy_group_functor_mul _ _) qed
+  | (k, fin.mk 1 H) :=
+    proof homomorphism.mk (cc_to_fn LES_of_homotopy_groups (k + 2, 1))
+                          (phomotopy_group_functor_mul _ _) qed
+  | (k, fin.mk 2 H) :=
+    begin
+      apply homomorphism.mk (cc_to_fn LES_of_homotopy_groups (k + 2, 2)),
+      exact abstract begin rewrite [LES_of_homotopy_groups_fun_2],
+      refine @is_homomorphism_compose _ _ _ _ _ _ (π→*[k + 2] boundary_map) _ _ _,
+      { apply group_homotopy_group (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 (l+3) H) := begin exfalso, apply lt_le_antisymm H, apply le_add_left end
+
+  end
+end chain_complex

homotopy/LES_applications.hlean

@@ -1,3 +1,9 @@
+/-
+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
+-/
+
 import .LES_of_homotopy_groups homotopy.connectedness homotopy.homotopy_group homotopy.join
 open eq is_trunc pointed is_conn is_equiv fiber equiv trunc nat chain_complex prod fin algebra
      group trunc_index function join pushout
@@ -49,7 +55,7 @@ namespace is_conn
         (@pgroup_of_group _ (comm_group_LES_of_homotopy_groups3 f k 1) idp)
         (homomorphism.struct (homomorphism_LES_of_homotopy_groups_fun3 f (k, 0)))},
     { /- k = 1 -/
-      exact sorry},
+      exact sorry}, -- need some more facts about anti-homomorphisms
     { /- k > 1 odd -/
       have H2' : 2 * succ k ≤ n, from le.trans !self_le_succ H2,
       have H3 : is_equiv (π→*[2*(succ k) + 1] f ∘* tinverse), from

homotopy/LES_of_homotopy_groups.hlean

@@ -3,41 +3,11 @@ 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
 
-We define the fiber sequence of a pointed map f : X →* Y. We follow the proof in section 8.4 of
+The old formalization of the LES of homotopy groups, where all the odd levels have a composition
-the book closely. First we define a sequence fiber_sequence as in Definition 8.4.3.
+  with negation
-It has types X(n) : Type*
-X(0)   := Y,
-X(1)   := X,
-X(n+1) := pfiber (f(n))
-with functions f(n) : X(n+1) →* X(n)
-f(0)   := f
-f(n+1) := ppoint f(n)
-We prove that this is an exact sequence.
-Then we prove Lemma 8.4.3, by showing that X(n+3) ≃* Ω(X(n)) and that this equivalence sends
-the map f(n+3) to -Ω(f(n)), i.e. the composition of Ω(f(n)) with path inversion.
-This is the hardest part of this formalization, because we need to show that they are the same
-as pointed maps (we define a pointed homotopy between them).
-
-Using this equivalence we get a boundary_map : Ω(Y) → pfiber f and we can define a new
-fiber sequence X'(n) : Type*
-X'(0)   := Y,
-X'(1)   := X,
-X'(2)   := pfiber f
-X'(n+3) := Ω(X'(n))
-and maps f'(n) : X'(n+1) →* X'(n)
-f'(0) := f
-f'(1) := ppoint f
-f'(2) := boundary_map f
-f'(3) := -Ω(f)
-f'(4) := -Ω(ppoint f)
-f'(5) := -Ω(boundary_map f)
-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
+import .LES2
 
 open eq pointed sigma fiber equiv is_equiv sigma.ops is_trunc nat trunc algebra function
 
@@ -47,183 +17,11 @@ open eq pointed sigma fiber equiv is_equiv sigma.ops is_trunc nat trunc algebra
 
 namespace chain_complex
 
-  definition fiber_sequence_helper [constructor] (v : Σ(X Y : Type*), X →* Y)
+  namespace old
-    : Σ(Z X : Type*), Z →* X :=
-  ⟨pfiber v.2.2, v.1, ppoint v.2.2⟩
-
-  definition fiber_sequence_helpern (v : Σ(X Y : Type*), X →* Y) (n : ℕ)
-    : Σ(Z X : Type*), Z →* X :=
-  iterate fiber_sequence_helper n v
-
   universe variable u
   variables {X Y : pType.{u}} (f : X →* Y) (n : ℕ)
   include f
 
-  definition fiber_sequence_carrier : Type* :=
-  (fiber_sequence_helpern ⟨X, Y, f⟩ n).2.1
-
-  definition fiber_sequence_fun
-    : fiber_sequence_carrier f (n + 1) →* fiber_sequence_carrier f n :=
-  (fiber_sequence_helpern ⟨X, Y, f⟩ n).2.2
-
-  /- Definition 8.4.3 -/
-  definition fiber_sequence : type_chain_complex.{0 u} +ℕ :=
-  begin
-    fconstructor,
-    { exact fiber_sequence_carrier f},
-    { exact fiber_sequence_fun f},
-    { intro n x, cases n with n,
-      { exact point_eq x},
-      { exact point_eq x}}
-  end
-
-  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) -/
-  definition fiber_sequence_carrier_equiv
-    : fiber_sequence_carrier f (n+3) ≃ Ω(fiber_sequence_carrier f n) :=
-  calc
-    fiber_sequence_carrier f (n+3) ≃ fiber (fiber_sequence_fun f (n+1)) pt : erfl
-    ... ≃ Σ(x : fiber_sequence_carrier f _), fiber_sequence_fun f (n+1) x = pt
-      : fiber.sigma_char
-    ... ≃ Σ(x : fiber (fiber_sequence_fun f n) pt), fiber_sequence_fun f _ x = pt
-      : erfl
-    ... ≃ Σ(v : Σ(x : fiber_sequence_carrier f _), fiber_sequence_fun f _ x = pt),
-            fiber_sequence_fun f _ (fiber.mk v.1 v.2) = pt
-      : by exact sigma_equiv_sigma !fiber.sigma_char (λa, erfl)
-    ... ≃ Σ(v : Σ(x : fiber_sequence_carrier f _), fiber_sequence_fun f _ x = pt),
-            v.1 = pt
-      : erfl
-    ... ≃ Σ(v : Σ(x : fiber_sequence_carrier f _), x = pt),
-            fiber_sequence_fun f _ v.1 = pt
-      : sigma_assoc_comm_equiv
-    ... ≃ fiber_sequence_fun f _ !center.1 = pt
-      : @(sigma_equiv_of_is_contr_left _) !is_contr_sigma_eq'
-    ... ≃ fiber_sequence_fun f _ pt = pt
-      : erfl
-    ... ≃ pt = pt
-      : by exact !equiv_eq_closed_left !respect_pt
-    ... ≃ Ω(fiber_sequence_carrier f n) : erfl
-
-  /- computation rule -/
-  definition fiber_sequence_carrier_equiv_eq
-    (x : fiber_sequence_carrier f (n+1)) (p : fiber_sequence_fun f n x = pt)
-    (q : fiber_sequence_fun f (n+1) (fiber.mk x p) = pt)
-    : fiber_sequence_carrier_equiv f n (fiber.mk (fiber.mk x p) q)
-      = !respect_pt⁻¹ ⬝ ap (fiber_sequence_fun f n) q⁻¹ ⬝ p :=
-  begin
-    refine _ ⬝ !con.assoc⁻¹,
-    apply whisker_left,
-    refine transport_eq_Fl _ _ ⬝ _,
-    apply whisker_right,
-    refine inverse2 !ap_inv ⬝ !inv_inv ⬝ _,
-    refine ap_compose (fiber_sequence_fun f n) pr₁ _ ⬝
-           ap02 (fiber_sequence_fun f n) !ap_pr1_center_eq_sigma_eq',
-  end
-
-  definition fiber_sequence_carrier_equiv_inv_eq
-    (p : Ω(fiber_sequence_carrier f n)) : (fiber_sequence_carrier_equiv f n)⁻¹ᵉ p =
-      fiber.mk (fiber.mk pt (respect_pt (fiber_sequence_fun f n) ⬝ p)) idp :=
-  begin
-    apply inv_eq_of_eq,
-    refine _ ⬝ !fiber_sequence_carrier_equiv_eq⁻¹, esimp,
-    exact !inv_con_cancel_left⁻¹
-  end
-
-  definition fiber_sequence_carrier_pequiv
-    : fiber_sequence_carrier f (n+3) ≃* Ω(fiber_sequence_carrier f n) :=
-  pequiv_of_equiv (fiber_sequence_carrier_equiv f n)
-    begin
-      esimp,
-      apply con.left_inv
-    end
-
-  definition fiber_sequence_carrier_pequiv_eq
-    (x : fiber_sequence_carrier f (n+1)) (p : fiber_sequence_fun f n x = pt)
-    (q : fiber_sequence_fun f (n+1) (fiber.mk x p) = pt)
-    : fiber_sequence_carrier_pequiv f n (fiber.mk (fiber.mk x p) q)
-      = !respect_pt⁻¹ ⬝ ap (fiber_sequence_fun f n) q⁻¹ ⬝ p :=
-  fiber_sequence_carrier_equiv_eq f n x p q
-
-  definition fiber_sequence_carrier_pequiv_inv_eq
-    (p : Ω(fiber_sequence_carrier f n)) : (fiber_sequence_carrier_pequiv f n)⁻¹ᵉ* p =
-      fiber.mk (fiber.mk pt (respect_pt (fiber_sequence_fun f n) ⬝ p)) idp :=
-  fiber_sequence_carrier_equiv_inv_eq f n p
-
-  attribute pequiv._trans_of_to_pmap [unfold 3]
-
-  /- Lemma 8.4.4(iii) -/
-  definition fiber_sequence_fun_eq_helper
-    (p : Ω(fiber_sequence_carrier f (n + 1))) :
-    fiber_sequence_carrier_pequiv f n
-      (fiber_sequence_fun f (n + 3)
-        ((fiber_sequence_carrier_pequiv f (n + 1))⁻¹ᵉ* p)) =
-          ap1 (fiber_sequence_fun f n) p⁻¹ :=
-  begin
-    refine ap (λx, fiber_sequence_carrier_pequiv f n (fiber_sequence_fun f (n + 3) x))
-              (fiber_sequence_carrier_pequiv_inv_eq f (n+1) p) ⬝ _,
-    /- the following three lines are rewriting some reflexivities: -/
-    -- replace (n + 3) with (n + 2 + 1),
-    -- refine ap (fiber_sequence_carrier_pequiv f n)
-    --           (fiber_sequence_fun_eq1 f (n+2) _ idp) ⬝ _,
-    refine fiber_sequence_carrier_pequiv_eq f n pt (respect_pt (fiber_sequence_fun f n)) _ ⬝ _,
-    esimp,
-    apply whisker_right,
-    apply whisker_left,
-    apply ap02, apply inverse2, apply idp_con,
-  end
-
-  theorem fiber_sequence_carrier_pequiv_eq_point_eq_idp :
-    fiber_sequence_carrier_pequiv_eq f n
-      (Point (fiber_sequence_carrier f (n+1)))
-      (respect_pt (fiber_sequence_fun f n))
-      (respect_pt (fiber_sequence_fun f (n + 1))) = idp :=
-  begin
-    apply con_inv_eq_idp,
-    refine ap (λx, whisker_left _ (_ ⬝ x)) _ ⬝ _,
-    { reflexivity},
-    { reflexivity},
-    esimp,
-    refine ap (whisker_left _)
-              (transport_eq_Fl_idp_left (fiber_sequence_fun f n)
-                                        (respect_pt (fiber_sequence_fun f n))) ⬝ _,
-    apply whisker_left_idp_con_eq_assoc
-  end
-
-  theorem fiber_sequence_fun_phomotopy_helper :
-    (fiber_sequence_carrier_pequiv f n ∘*
-      fiber_sequence_fun f (n + 3)) ∘*
-        (fiber_sequence_carrier_pequiv f (n + 1))⁻¹ᵉ* ~*
-          ap1 (fiber_sequence_fun f n) ∘* pinverse :=
-  begin
-    fapply phomotopy.mk,
-    { exact (fiber_sequence_fun_eq_helper f n)},
-    { esimp, rewrite [idp_con], refine _ ⬝ whisker_left _ !idp_con⁻¹,
-      apply whisker_right,
-      apply whisker_left,
-      exact fiber_sequence_carrier_pequiv_eq_point_eq_idp f n}
-  end
-
-  theorem fiber_sequence_fun_eq : Π(x : fiber_sequence_carrier f (n + 4)),
-    fiber_sequence_carrier_pequiv f n (fiber_sequence_fun f (n + 3) x) =
-      ap1 (fiber_sequence_fun f n) (fiber_sequence_carrier_pequiv f (n + 1) x)⁻¹ :=
-  begin
-    apply homotopy_of_inv_homotopy_pre (fiber_sequence_carrier_pequiv f (n + 1)),
-    apply fiber_sequence_fun_eq_helper f n
-  end
-
-  theorem fiber_sequence_fun_phomotopy :
-    fiber_sequence_carrier_pequiv f n ∘*
-      fiber_sequence_fun f (n + 3) ~*
-          (ap1 (fiber_sequence_fun f n) ∘* pinverse) ∘* fiber_sequence_carrier_pequiv f (n + 1) :=
-  begin
-    apply phomotopy_of_pinv_right_phomotopy,
-    apply fiber_sequence_fun_phomotopy_helper
-  end
-
-  definition boundary_map : Ω Y →* pfiber f :=
-  fiber_sequence_fun f 2 ∘* (fiber_sequence_carrier_pequiv f 0)⁻¹ᵉ*
 
 /--------------
     PART 2
@@ -324,7 +122,7 @@ namespace chain_complex
   | (k+3) :=
     begin
       refine fiber_sequence_carrier_pequiv f k ⬝e* _,
-      apply loop_space_pequiv,
+      apply loop_pequiv_loop,
       exact fiber_sequence_pequiv_homotopy_groups k
     end
 
@@ -486,7 +284,7 @@ namespace chain_complex
   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)
 
-end chain_complex
+end old end chain_complex
 
 open group prod succ_str fin
 
@@ -494,30 +292,7 @@ open group prod succ_str fin
     PART 3
  --------------/
 
-namespace chain_complex
+namespace chain_complex namespace old
-
-  --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
@@ -651,32 +426,32 @@ namespace chain_complex
       -- 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,
+      apply loop_pequiv_loop, apply loop_pequiv_loop,
       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,
+      apply loop_pequiv_loop, apply loop_pequiv_loop,
       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,
+      apply loop_pequiv_loop, apply loop_pequiv_loop,
       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,
+      apply loop_pequiv_loop, apply loop_pequiv_loop,
       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,
+      apply loop_pequiv_loop, apply loop_pequiv_loop,
       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,
+      apply loop_pequiv_loop, apply loop_pequiv_loop,
       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
@@ -744,9 +519,9 @@ namespace chain_complex
       induction n with n IH,
       { refine !pid_comp ⬝* _ ⬝* !comp_pid⁻¹*,
         refine !comp_pid⁻¹* ⬝* pconcat2 _ _,
-        { exact !comp_pid⁻¹*},
+        { exact (comp_pid (ap1 (boundary_map f) ∘* pinverse))⁻¹*},
-        { refine cast (ap (λx, _ ~* loop_space_pequiv x) !loop_space_pequiv_rfl)⁻¹ _,
+        { refine cast (ap (λx, _ ~* loop_pequiv_loop x) !loop_pequiv_loop_rfl)⁻¹ _,
-          refine cast (ap (λx, _ ~* x) !loop_space_pequiv_rfl)⁻¹ _, reflexivity}},
+          refine cast (ap (λx, _ ~* x) !loop_pequiv_loop_rfl)⁻¹ _, reflexivity}},
       { refine _ ⬝* !comp_pid⁻¹*,
         refine _ ⬝* pwhisker_right _ (!homotopy_groups_fun2_add1_5)⁻¹*,
         refine !ap1_compose⁻¹* ⬝* _ ⬝* !ap1_compose, apply ap1_phomotopy,
@@ -988,4 +763,5 @@ namespace chain_complex
 
   --TODO: the maps 3, 4 and 5 are anti-homomorphisms.
 
+  end old
 end chain_complex

homotopy/chain_complex.hlean

@@ -5,7 +5,7 @@ Authors: Floris van Doorn
 
 -/
 
-import types.int types.pointed2 types.trunc algebra.hott ..group_theory.basic .fin
+import types.int types.pointed types.trunc algebra.hott ..group_theory.basic .fin
 
 open eq pointed int unit is_equiv equiv is_trunc trunc function algebra group sigma.ops
      sum prod nat bool fin
@@ -127,7 +127,7 @@ namespace chain_complex
   --   : is_exact_at_t (type_chain_complex_from_left X) n :=
   -- H
 
-  definition transfer_type_chain_complex [constructor]
+  definition transfer_type_chain_complex [constructor] /- X -/
     {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
@@ -158,6 +158,41 @@ namespace chain_complex
     apply right_inv
   end
 
+  -- cancel automorphisms inside a long exact sequence
+  definition type_chain_complex_cancel_aut [constructor] /- X -/
+    (g : Π{n : N}, X (S n) →* X n) (e : Π{n}, X n ≃* X n)
+    (r : Π{n}, X n →* X n)
+    (p : Π{n : N} (x : X (S n)), g (e x) = tcc_to_fn X n x)
+    (pr : Π{n : N} (x : X (S n)), g x = r (g (e x))) : type_chain_complex N :=
+  type_chain_complex.mk X @g
+    abstract begin
+      have p' : Π{n : N} (x : X (S n)), g x = tcc_to_fn X n (e⁻¹ x),
+      from λn, homotopy_inv_of_homotopy_pre e _ _ p,
+      intro n x,
+      refine ap g !p' ⬝ !pr ⬝ _,
+      refine ap r !p ⬝ _,
+      refine ap r (tcc_is_chain_complex X n _) ⬝ _,
+      apply respect_pt
+    end end
+
+  theorem is_exact_at_t_cancel_aut {X : type_chain_complex N}
+    {g : Π{n : N}, X (S n) →* X n} {e : Π{n}, X n ≃* X n}
+    {r : Π{n}, X n →* X n} (l : Π{n}, X n →* X n)
+    (p : Π{n : N} (x : X (S n)), g (e x) = tcc_to_fn X n x)
+    (pr : Π{n : N} (x : X (S n)), g x = r (g (e x)))
+    (pl : Π{n : N} (x : X (S n)), g (l x) = e (g x))
+    (H : is_exact_at_t X n) : is_exact_at_t (type_chain_complex_cancel_aut X @g @e @r @p @pr) n :=
+  begin
+    intro y q, esimp at *,
+    have H2 : tcc_to_fn X n (e⁻¹ y) = pt,
+    from (homotopy_inv_of_homotopy_pre e _ _ p _)⁻¹ ⬝ q,
+    cases (H _ H2) with x s,
+    refine fiber.mk (l (e x)) _,
+    refine !pl ⬝ _,
+    refine ap e (!p ⬝ s) ⬝ _,
+    apply right_inv
+  end
+
   -- 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) :=
@@ -167,6 +202,7 @@ namespace chain_complex
     (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
 
+  -- move
   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

homotopy/sec86.hlean

@@ -267,10 +267,3 @@ namespace sphere
   -- end
 
 end sphere
-
-/-
-  changes in book:
-  proof 8.6.15: also mention that we ignore multiplication
-  proof 8.4.4: respects points
-  proof 8.4.8: do k=0 separately
--/

homotopy/spectrum.hlean

@@ -5,7 +5,7 @@ Authors: Michael Shulman
 
 -/
 
-import types.int types.pointed2 types.trunc homotopy.susp algebra.homotopy_group .chain_complex cubical
+import types.int types.pointed types.trunc homotopy.susp algebra.homotopy_group .chain_complex cubical
 open eq nat int susp pointed pmap sigma is_equiv equiv fiber algebra trunc trunc_index pi
 
 /-----------------------------------------
@@ -136,7 +136,7 @@ namespace pointed
 
   definition pequiv_postcompose {A B B' : Type*} (f : A →* B) (g : B ≃* B') : pfiber (g ∘* f) ≃* pfiber f :=
   begin
-    fapply pequiv_of_equiv, esimp, 
+    fapply pequiv_of_equiv, esimp,
     refine ((transport_fiber_equiv (g ∘* f) (respect_pt g)⁻¹) ⬝e (@fiber.equiv_postcompose A B f (Point B) B' g _)),
     esimp, apply (ap (fiber.mk (Point A))), rewrite con.assoc, apply inv_con_eq_of_eq_con,
     rewrite [con.assoc, con.right_inv, con_idp, -ap_compose'], apply ap_con_eq_con
@@ -144,7 +144,7 @@ namespace pointed
 
   definition pequiv_precompose {A A' B : Type*} (f : A →* B) (g : A' ≃* A) : pfiber (f ∘* g) ≃* pfiber f :=
   begin
-    fapply pequiv_of_equiv, esimp, 
+    fapply pequiv_of_equiv, esimp,
     refine (@fiber.equiv_precompose A B f (Point B) A' g _),
     esimp, apply (eq_of_fn_eq_fn (fiber.sigma_char _ _)), fapply sigma_eq: esimp,
     { apply respect_pt g },
@@ -157,13 +157,11 @@ namespace pointed
               ... ≃* pfiber (g ∘* h) : pfiber_equiv_of_phomotopy s
               ... ≃* pfiber g : pequiv_precompose
 
-  definition ppi {A : Type} (P : A → Type*) : Type* :=
+  definition loop_ppi_commute {A : Type} (B : A → Type*) : Ω(ppi B) ≃* Π*a, Ω (B a) :=
-    pointed.mk' (Πa, P a)
-
-  definition loop_ppi_commute {A : Type} (B : A → Type*) : Ω(ppi B) ≃* (ppi (λa, Ω (B a))) :=
     pequiv_of_equiv eq_equiv_homotopy rfl
 
-  definition equiv_ppi_right {A : Type} {P Q : A → Type*} (g : Πa, P a ≃* Q a) : ppi P ≃* ppi Q :=
+  definition equiv_ppi_right {A : Type} {P Q : A → Type*} (g : Πa, P a ≃* Q a)
+    : (Π*a, P a) ≃* (Π*a, Q a) :=
     pequiv_of_equiv (pi_equiv_pi_right g)
       begin esimp, apply eq_of_homotopy, intros a, esimp, exact (respect_pt (g a)) end
 
@@ -206,7 +204,7 @@ namespace spectrum
 
   definition glue {{N : succ_str}} := @gen_prespectrum.glue N
   --definition glue := (@gen_prespectrum.glue +ℤ)
-  definition equiv_glue {N : succ_str} (E : gen_prespectrum N) [H : is_spectrum E] (n:N) : (E n) ≃* (Ω (E (S n))) := 
+  definition equiv_glue {N : succ_str} (E : gen_prespectrum N) [H : is_spectrum E] (n:N) : (E n) ≃* (Ω (E (S n))) :=
     pequiv_of_pmap (glue E n) (is_spectrum.is_equiv_glue E n)
 
   -- Sometimes an ℕ-indexed version does arise naturally, however, so