feat(hott): Port files from other repositories to the HoTT library.

This commit adds truncated 2-quotients, groupoid quotients, Eilenberg MacLane spaces, chain complexes, the long exact sequence of homotopy groups, the Freudenthal Suspension Theorem, Whitehead's principle, and the computation of homotopy groups of almost all spheres which are known in HoTT.
2016-04-22 15:12:25 -04:00 · 2016-04-22 15:12:25 -04:00 · 52dd6cf90b
commit 52dd6cf90b
parent ab7adf3084
46 changed files with 3238 additions and 178 deletions
--- a/hott/algebra/algebra.md
+++ b/hott/algebra/algebra.md
@ -16,9 +16,10 @@ The following files are [ported](../port.md) from the standard library. If anyth
 * [ordered_field](ordered_field.hlean)
 * [bundled](bundled.hlean) : bundled versions of the algebraic structures

-Files which are HoTT specific:
+Files which are not ported from the standard library:

 * [hott](hott.hlean) : Basic theorems about the algebraic hierarchy specific to HoTT
+* [group_theory](group_theory.hlean) : Basic theorems about group homomorphisms and isomorphisms
 * [trunc_group](trunc_group.hlean) : truncate an infinity-group to a group
 * [homotopy_group](homotopy_group.hlean) : homotopy groups of a pointed type
 * [e_closure](e_closure.hlean) : the type of words formed by a relation
--- a/hott/algebra/binary.hlean
+++ b/hott/algebra/binary.hlean
@ -88,30 +88,30 @@ end binary
 open eq
 namespace is_equiv
  definition inv_preserve_binary {A B : Type} (f : A → B) [H : is_equiv f]
-    (mA : A → A → A) (mB : B → B → B) (H : Π(a a' : A), mB (f a) (f a') = f (mA a a'))
+    (mA : A → A → A) (mB : B → B → B) (H : Π(a a' : A), f (mA a a') = mB (f a) (f a'))
    (b b' : B) : f⁻¹ (mB b b') = mA (f⁻¹ b) (f⁻¹ b') :=
  begin
-  have H2 : f⁻¹ (mB (f (f⁻¹ b)) (f (f⁻¹ b'))) = f⁻¹ (f (mA (f⁻¹ b) (f⁻¹ b'))), from ap f⁻¹ !H,
+  have H2 : f⁻¹ (mB (f (f⁻¹ b)) (f (f⁻¹ b'))) = f⁻¹ (f (mA (f⁻¹ b) (f⁻¹ b'))), from ap f⁻¹ !H⁻¹,
  rewrite [+right_inv f at H2,left_inv f at H2,▸* at H2,H2]
  end

  definition preserve_binary_of_inv_preserve {A B : Type} (f : A → B) [H : is_equiv f]
-    (mA : A → A → A) (mB : B → B → B) (H : Π(b b' : B), mA (f⁻¹ b) (f⁻¹ b') = f⁻¹ (mB b b'))
+    (mA : A → A → A) (mB : B → B → B) (H : Π(b b' : B), f⁻¹ (mB b b') = mA (f⁻¹ b) (f⁻¹ b'))
    (a a' : A) : f (mA a a') = mB (f a) (f a') :=
  begin
-  have H2 : f (mA (f⁻¹ (f a)) (f⁻¹ (f a'))) = f (f⁻¹ (mB (f a) (f a'))), from ap f !H,
+  have H2 : f (mA (f⁻¹ (f a)) (f⁻¹ (f a'))) = f (f⁻¹ (mB (f a) (f a'))), from ap f !H⁻¹,
  rewrite [right_inv f at H2,+left_inv f at H2,▸* at H2,H2]
  end
 end is_equiv
 namespace equiv
  open is_equiv
  definition inv_preserve_binary {A B : Type} (f : A ≃ B)
-    (mA : A → A → A) (mB : B → B → B) (H : Π(a a' : A), mB (f a) (f a') = f (mA a a'))
+    (mA : A → A → A) (mB : B → B → B) (H : Π(a a' : A), f (mA a a') = mB (f a) (f a'))
    (b b' : B) : f⁻¹ (mB b b') = mA (f⁻¹ b) (f⁻¹ b') :=
  inv_preserve_binary f mA mB H b b'

  definition preserve_binary_of_inv_preserve {A B : Type} (f : A ≃ B)
-    (mA : A → A → A) (mB : B → B → B) (H : Π(b b' : B), mA (f⁻¹ b) (f⁻¹ b') = f⁻¹ (mB b b'))
+    (mA : A → A → A) (mB : B → B → B) (H : Π(b b' : B), f⁻¹ (mB b b') = mA (f⁻¹ b) (f⁻¹ b'))
    (a a' : A) : f (mA a a') = mB (f a) (f a') :=
  preserve_binary_of_inv_preserve f mA mB H a a'
 end equiv
--- a/hott/algebra/group_theory.hlean
+++ b/hott/algebra/group_theory.hlean
@ -144,6 +144,10 @@ namespace group
  definition equiv_of_isomorphism [constructor] (φ : G₁ ≃g G₂) : G₁ ≃ G₂ :=
  equiv.mk φ _

+  definition pequiv_of_isomorphism [constructor] (φ : G₁ ≃g G₂) :
+    pType_of_Group G₁ ≃* pType_of_Group G₂ :=
+  pequiv.mk φ _ (respect_one φ)
+
  definition isomorphism_of_equiv [constructor] (φ : G₁ ≃ G₂)
    (p : Πg₁ g₂, φ (g₁ * g₂) = φ g₁ * φ g₂) : G₁ ≃g G₂ :=
  isomorphism.mk (homomorphism.mk φ p) !to_is_equiv
@ -171,8 +175,18 @@ namespace group
  definition isomorphism.trans [trans] [constructor] (φ : G₁ ≃g G₂) (ψ : G₂ ≃g G₃) : G₁ ≃g G₃ :=
  isomorphism.mk (ψ ∘g φ) !is_equiv_compose

+  definition isomorphism.eq_trans [trans] [constructor]
+     {G₁ G₂ G₃ : Group} (φ : G₁ = G₂) (ψ : G₂ ≃g G₃) : G₁ ≃g G₃ :=
+  proof isomorphism.trans (isomorphism_of_eq φ) ψ qed
+
+  definition isomorphism.trans_eq [trans] [constructor]
+    {G₁ G₂ G₃ : Group} (φ : G₁ ≃g G₂) (ψ : G₂ = G₃) : G₁ ≃g G₃ :=
+  isomorphism.trans φ (isomorphism_of_eq ψ)
+
  postfix `⁻¹ᵍ`:(max + 1) := isomorphism.symm
  infixl ` ⬝g `:75 := isomorphism.trans
+  infixl ` ⬝gp `:75 := isomorphism.trans_eq
+  infixl ` ⬝pg `:75 := isomorphism.eq_trans

  -- TODO
  -- definition Group_univalence (G₁ G₂ : Group) : (G₁ ≃g G₂) ≃ (G₁ = G₂) :=
@ -257,4 +271,31 @@ namespace group
  definition trivial_group_of_is_contr' (G : Group) [H : is_contr G] : G = G0 :=
  eq_of_isomorphism (trivial_group_of_is_contr G)

+  /-
+    A group where the point in the pointed type corresponds with 1 in the group.
+    We need this structure when we are given a pointed type, and want to say that there is a group
+    structure on it which is compatible with the point. This is used in chain complexes.
+  -/
+  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
+
 end group
--- a/hott/algebra/homotopy_group.hlean
+++ b/hott/algebra/homotopy_group.hlean
@ -8,8 +8,9 @@ homotopy groups of a pointed space

 import .trunc_group types.trunc .group_theory

-open nat eq pointed trunc is_trunc algebra group function equiv unit
+open nat eq pointed trunc is_trunc algebra group function equiv unit is_equiv

+-- TODO: consistently make n an argument before A
 namespace eq

  definition phomotopy_group [reducible] [constructor] (n : ℕ) (A : Type*) : Set* :=
@ -25,6 +26,10 @@ namespace eq
    : group (π[succ n] A) :=
  trunc_group concat inverse idp con.assoc idp_con con_idp con.left_inv

+  definition group_homotopy_group2 [instance] (k : ℕ) (A : Type*) :
+    group (carrier (ptrunctype.to_pType (π*[k + 1] A))) :=
+  group_homotopy_group k A
+
  definition comm_group_homotopy_group [constructor] [reducible] (n : ℕ) (A : Type*)
    : comm_group (π[succ (succ n)] A) :=
  trunc_comm_group concat inverse idp con.assoc idp_con con_idp con.left_inv eckmann_hilton
@ -43,7 +48,7 @@ namespace eq
  notation `πg[`:95  n:0 ` +1] `:0 A:95 := ghomotopy_group n A
  notation `πag[`:95 n:0 ` +2] `:0 A:95 := cghomotopy_group n A

-  notation `π₁` := fundamental_group
+  notation `π₁` := fundamental_group -- should this be notation for the group or pointed type?

  definition tr_mul_tr {n : ℕ} {A : Type*} (p q : Ω[n + 1] A) :
    tr p *[πg[n+1] A] tr q = tr (p ⬝ q) :=
@ -64,6 +69,15 @@ namespace eq
    exact loopn_pequiv_loopn k (pequiv_of_eq begin rewrite [trunc_index.zero_add] end)
  end

+  definition phomotopy_group_ptrunc [constructor] (k : ℕ) (A : Type*) :
+    π*[k] (ptrunc k A) ≃* π*[k] A :=
+  calc
+    π*[k] (ptrunc k A) ≃* Ω[k] (ptrunc k (ptrunc k A))
+             : phomotopy_group_pequiv_loop_ptrunc k (ptrunc k A)
+      ... ≃* Ω[k] (ptrunc k A)
+             : loopn_pequiv_loopn k (ptrunc_pequiv k (ptrunc k A) _)
+      ... ≃* π*[k] A : (phomotopy_group_pequiv_loop_ptrunc k A)⁻¹ᵉ*
+
  theorem trivial_homotopy_of_is_set (A : Type*) [H : is_set A] (n : ℕ) : πg[n+1] A ≃g G0 :=
  begin
    apply trivial_group_of_is_contr,
@ -74,11 +88,23 @@ namespace eq

  definition phomotopy_group_succ_out (A : Type*) (n : ℕ) : π*[n + 1] A = π₁ Ω[n] A := idp

-  definition phomotopy_group_succ_in (A : Type*) (n : ℕ) : π*[n + 1] A = π*[n] Ω A :=
+  definition phomotopy_group_succ_in (A : Type*) (n : ℕ) : π*[n + 1] A = π*[n] (Ω A) :> Type* :=
  ap (ptrunc 0) (loop_space_succ_eq_in A n)

  definition ghomotopy_group_succ_out (A : Type*) (n : ℕ) : πg[n +1] A = π₁ Ω[n] A := idp

+  definition phomotopy_group_succ_in_con {A : Type*} {n : ℕ} (g h : πg[succ n +1] A) :
+    pcast (phomotopy_group_succ_in A (succ n)) (g * h) =
+    pcast (phomotopy_group_succ_in A (succ n)) g *
+    pcast (phomotopy_group_succ_in A (succ n)) h :=
+  begin
+    induction g with p, induction h with q, esimp,
+    rewrite [-+ tr_eq_cast_ap, ↑phomotopy_group_succ_in, -+ tr_compose],
+    refine ap (transport _ _) !tr_mul_tr' ⬝ _,
+    rewrite [+ trunc_transport],
+    apply ap tr, apply loop_space_succ_eq_in_concat,
+  end
+
  definition ghomotopy_group_succ_in (A : Type*) (n : ℕ) : πg[succ n +1] A ≃g πg[n +1] Ω A :=
  begin
    fapply isomorphism_of_equiv,
@ -98,6 +124,36 @@ namespace eq
  notation `π→*[`:95 n:0 `] `:0 := phomotopy_group_functor n
  notation `π→[`:95  n:0 `] `:0 :=  homotopy_group_functor n

+  definition phomotopy_group_functor_phomotopy [constructor] (n : ℕ) {A B : Type*} {f g : A →* B}
+    (p : f ~* g) : π→*[n] f ~* π→*[n] g :=
+  ptrunc_functor_phomotopy 0 (apn_phomotopy n p)
+
+  definition phomotopy_group_functor_compose [constructor] (n : ℕ) {A B C : Type*} (g : B →* C)
+    (f : A →* B) : π→*[n] (g ∘* f) ~* π→*[n] g ∘* π→*[n] f :=
+  ptrunc_functor_phomotopy 0 !apn_compose ⬝* !ptrunc_functor_pcompose
+
+  definition is_equiv_homotopy_group_functor [constructor] (n : ℕ) {A B : Type*} (f : A →* B)
+    [is_equiv f] : is_equiv (π→[n] f) :=
+  @(is_equiv_trunc_functor 0 _) !is_equiv_apn
+
+  definition phomotopy_group_functor_succ_phomotopy_in (n : ℕ) {A B : Type*} (f : A →* B) :
+    pcast (phomotopy_group_succ_in B n) ∘* π→*[n + 1] f ~*
+    π→*[n] (Ω→ f) ∘* pcast (phomotopy_group_succ_in A n) :=
+  begin
+    refine pwhisker_right _ (pcast_ptrunc 0 (loop_space_succ_eq_in B n)) ⬝* _,
+    refine _ ⬝* pwhisker_left _ (pcast_ptrunc 0 (loop_space_succ_eq_in A n))⁻¹*,
+    refine !ptrunc_functor_pcompose⁻¹* ⬝* _ ⬝* !ptrunc_functor_pcompose,
+    exact ptrunc_functor_phomotopy 0 (apn_succ_phomotopy_in n f)
+  end
+
+  definition is_equiv_phomotopy_group_functor_ap1 (n : ℕ) {A B : Type*} (f : A →* B)
+    [is_equiv (π→*[n + 1] f)] : is_equiv (π→*[n] (Ω→ f)) :=
+  have is_equiv (pcast (phomotopy_group_succ_in B n) ∘* π→*[n + 1] f),
+  begin apply @(is_equiv_compose (π→*[n + 1] f) _) end,
+  have is_equiv (π→*[n] (Ω→ f) ∘ pcast (phomotopy_group_succ_in A n)),
+  from is_equiv.homotopy_closed _ (phomotopy_group_functor_succ_phomotopy_in n f),
+  is_equiv.cancel_right (pcast (phomotopy_group_succ_in A n)) _
+
  definition tinverse [constructor] {X : Type*} : π*[1] X →* π*[1] X :=
  ptrunc_functor 0 pinverse

@ -156,6 +212,36 @@ namespace eq
  isomorphism_of_eq (ap (λx, πg[x+1] A) (p⁻¹ ⬝ add.comm n k)) ⬝g
  trivial_homotopy_add_of_is_set_loop_space k H2

+  definition phomotopy_group_pequiv_loop_ptrunc_con {k : ℕ} {A : Type*} (p q : πg[k +1] A) :
+    phomotopy_group_pequiv_loop_ptrunc (succ k) A (p * q) =
+    phomotopy_group_pequiv_loop_ptrunc (succ k) A p ⬝
+    phomotopy_group_pequiv_loop_ptrunc (succ k) A q :=
+  begin
+    refine _ ⬝ !loopn_pequiv_loopn_con,
+    exact ap (loopn_pequiv_loopn _ _) !iterated_loop_ptrunc_pequiv_inv_con
+  end
+
+  definition phomotopy_group_pequiv_loop_ptrunc_inv_con {k : ℕ} {A : Type*}
+    (p q : Ω[succ k] (ptrunc (succ k) A)) :
+    (phomotopy_group_pequiv_loop_ptrunc (succ k) A)⁻¹ᵉ* (p ⬝ q) =
+    (phomotopy_group_pequiv_loop_ptrunc (succ k) A)⁻¹ᵉ* p *
+    (phomotopy_group_pequiv_loop_ptrunc (succ k) A)⁻¹ᵉ* q :=
+  inv_preserve_binary (phomotopy_group_pequiv_loop_ptrunc (succ k) A) mul concat
+    (@phomotopy_group_pequiv_loop_ptrunc_con k A) p q
+
+  definition ghomotopy_group_ptrunc [constructor] (k : ℕ) (A : Type*) :
+    πg[k+1] (ptrunc (k+1) A) ≃g πg[k+1] A :=
+  begin
+    fapply isomorphism_of_equiv,
+    { exact phomotopy_group_ptrunc (k+1) A},
+    { intro g₁ g₂, esimp,
+      refine _ ⬝ !phomotopy_group_pequiv_loop_ptrunc_inv_con,
+      apply ap ((phomotopy_group_pequiv_loop_ptrunc (k+1) A)⁻¹ᵉ*),
+      refine _ ⬝ !loopn_pequiv_loopn_con ,
+      apply ap (loopn_pequiv_loopn (k+1) _),
+      apply phomotopy_group_pequiv_loop_ptrunc_con}
+  end
+
  /- some homomorphisms -/

  definition is_homomorphism_cast_loop_space_succ_eq_in {A : Type*} (n : ℕ) :
--- a/hott/function.hlean
+++ b/hott/function.hlean
@ -13,9 +13,22 @@ open equiv sigma sigma.ops eq trunc is_trunc pi is_equiv fiber prod

 variables {A B : Type} (f : A → B) {b : B}

+/- the image of a map is the (-1)-truncated fiber -/
+definition image' [constructor] (f : A → B) (b : B) : Type := ∥ fiber f b ∥
+definition is_prop_image' [instance] (f : A → B) (b : B) : is_prop (image' f b) := !is_trunc_trunc
+definition image [constructor] (f : A → B) (b : B) : Prop := Prop.mk (image' f b) _
+
+definition image.mk [constructor] {f : A → B} {b : B} (a : A) (p : f a = b)
+  : image f b :=
+tr (fiber.mk a p)
+
+protected definition image.rec [unfold 8] [recursor 8] {f : A → B} {b : B} {P : image' f b → Type}
+  [H : Πv, is_prop (P v)] (H : Π(a : A) (p : f a = b), P (image.mk a p)) (v : image' f b) : P v :=
+begin unfold [image'] at *, induction v with v, induction v with a p, exact H a p end
+
 definition is_embedding [class] (f : A → B) := Π(a a' : A), is_equiv (ap f : a = a' → f a = f a')

-definition is_surjective [class] (f : A → B) := Π(b : B), ∥ fiber f b ∥
+definition is_surjective [class] (f : A → B) := Π(b : B), image f b

 definition is_split_surjective [class] (f : A → B) := Π(b : B), fiber f b

@ -114,13 +127,13 @@ namespace function
  λb, tr (H b)

  definition is_prop_is_surjective [instance] : is_prop (is_surjective f) :=
-  by unfold is_surjective; exact _
+  begin unfold is_surjective, exact _ end

  definition is_surjective_cancel_right {A B C : Type} (g : B → C) (f : A → B)
    [H : is_surjective (g ∘ f)] : is_surjective g :=
  begin
    intro c,
-    induction H c with v, induction v with a p,
+    induction H c with a p,
    exact tr (fiber.mk (f a) p)
  end

--- a/hott/hit/groupoid_quotient.hlean
+++ b/hott/hit/groupoid_quotient.hlean
@ -0,0 +1,245 @@
+/-
+Copyright (c) 2015-16 Floris van Doorn. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Authors: Floris van Doorn
+
+The groupoid quotient. This is a 1-type which path spaces is the same as the morphisms
+a given groupoid. We define it as the 1-truncation of a two quotient.
+-/
+
+import algebra.category.groupoid .two_quotient homotopy.connectedness
+       algebra.group_theory
+
+open trunc_two_quotient eq bool unit relation category e_closure iso is_trunc trunc equiv is_equiv
+     group
+
+namespace groupoid_quotient
+section
+  parameter (G : Groupoid)
+
+  inductive groupoid_quotient_R : G → G → Type :=
+  | Rmk : Π{a b : G} (f : a ⟶ b), groupoid_quotient_R a b
+
+  open groupoid_quotient_R
+  local abbreviation R := groupoid_quotient_R
+
+  inductive groupoid_quotient_Q : Π⦃x y : G⦄,
+    e_closure groupoid_quotient_R x y → e_closure groupoid_quotient_R x y → Type :=
+  | Qconcat : Π{a b c : G} (g : b ⟶ c) (f : a ⟶ b),
+                groupoid_quotient_Q [Rmk (g ∘ f)] ([Rmk f] ⬝r [Rmk g])
+
+  open groupoid_quotient_Q
+  local abbreviation Q := groupoid_quotient_Q
+
+  definition groupoid_quotient := trunc_two_quotient 1 R Q
+
+  local attribute groupoid_quotient [reducible]
+  definition is_trunc_groupoid_quotient [instance] : is_trunc 1 groupoid_quotient := _
+
+  parameter {G}
+  variables {a b c : G}
+  definition elt (a : G) : groupoid_quotient := incl0 a
+  definition pth (f : a ⟶ b) : elt a = elt b := incl1 (Rmk f)
+  definition resp_comp (g : b ⟶ c) (f : a ⟶ b) : pth (g ∘ f) = pth f ⬝ pth g := incl2 (Qconcat g f)
+  definition resp_id (a : G) : pth (ID a) = idp :=
+  begin
+    apply cancel_right (pth (id)), refine _ ⬝ !idp_con⁻¹,
+    refine !resp_comp⁻¹ ⬝ _,
+    exact ap pth !id_id,
+  end
+
+  definition resp_inv (f : a ⟶ b) : pth (f⁻¹) = (pth f)⁻¹ :=
+  begin
+    apply eq_inv_of_con_eq_idp',
+    refine !resp_comp⁻¹ ⬝ _,
+    refine ap pth !right_inverse ⬝ _,
+    apply resp_id
+  end
+
+  protected definition rec {P : groupoid_quotient → Type} [Πx, is_trunc 1 (P x)]
+    (Pe : Πg, P (elt g)) (Pp : Π⦃a b⦄ (f : a ⟶ b), Pe a =[pth f] Pe b)
+    (Pcomp : Π⦃a b c⦄ (g : b ⟶ c) (f : a ⟶ b),
+      change_path (resp_comp g f) (Pp (g ∘ f)) = Pp f ⬝o Pp g)
+    (x : groupoid_quotient) : P x :=
+  begin
+    induction x,
+    { apply Pe},
+    { induction s with a b f, apply Pp},
+    { induction q with a b c g f,
+      apply Pcomp}
+  end
+
+  protected definition rec_on {P : groupoid_quotient → Type} [Πx, is_trunc 1 (P x)]
+    (x : groupoid_quotient)
+    (Pe : Πg, P (elt g)) (Pp : Π⦃a b⦄ (f : a ⟶ b), Pe a =[pth f] Pe b)
+    (Pcomp : Π⦃a b c⦄ (g : b ⟶ c) (f : a ⟶ b),
+      change_path (resp_comp g f) (Pp (g ∘ f)) = Pp f ⬝o Pp g) : P x :=
+  rec Pe Pp Pcomp x
+
+  protected definition set_rec {P : groupoid_quotient → Type} [Πx, is_set (P x)]
+    (Pe : Πg, P (elt g)) (Pp : Π⦃a b⦄ (f : a ⟶ b), Pe a =[pth f] Pe b)
+    (x : groupoid_quotient) : P x :=
+  rec Pe Pp !center x
+
+  protected definition prop_rec {P : groupoid_quotient → Type} [Πx, is_prop (P x)]
+    (Pe : Πg, P (elt g)) (x : groupoid_quotient) : P x :=
+  rec Pe !center !center x
+
+  definition rec_pth {P : groupoid_quotient → Type} [Πx, is_trunc 1 (P x)]
+    {Pe : Πg, P (elt g)} {Pp : Π⦃a b⦄ (f : a ⟶ b), Pe a =[pth f] Pe b}
+    (Pcomp : Π⦃a b c⦄ (g : b ⟶ c) (f : a ⟶ b),
+      change_path (resp_comp g f) (Pp (g ∘ f)) = Pp f ⬝o Pp g)
+    {a b : G} (f : a ⟶ b) : apd (rec Pe Pp Pcomp) (pth f) = Pp f :=
+  proof !rec_incl1 qed
+
+  protected definition elim {P : Type} [is_trunc 1 P] (Pe : G → P)
+    (Pp : Π⦃a b⦄ (f : a ⟶ b), Pe a = Pe b)
+    (Pcomp : Π⦃a b c⦄ (g : b ⟶ c) (f : a ⟶ b), Pp (g ∘ f) = Pp f ⬝ Pp g)
+    (x : groupoid_quotient) : P :=
+  begin
+    induction x,
+    { exact Pe a},
+    { induction s with a b f, exact Pp f},
+    { induction q with a b c g f,
+      exact Pcomp g f}
+  end
+
+  protected definition elim_on [reducible] {P : Type} [is_trunc 1 P] (x : groupoid_quotient)
+    (Pe : G → P) (Pp : Π⦃a b⦄ (f : a ⟶ b), Pe a = Pe b)
+    (Pcomp : Π⦃a b c⦄ (g : b ⟶ c) (f : a ⟶ b), Pp (g ∘ f) = Pp f ⬝ Pp g) : P :=
+  elim Pe Pp Pcomp x
+
+  protected definition set_elim [reducible] {P : Type} [is_set P] (Pe : G → P)
+    (Pp : Π⦃a b⦄ (f : a ⟶ b), Pe a = Pe b)
+    (x : groupoid_quotient) : P :=
+  elim Pe Pp !center x
+
+  protected definition prop_elim [reducible] {P : Type} [is_prop P] (Pe : G → P)
+    (x : groupoid_quotient) : P :=
+  elim Pe !center !center x
+
+  definition elim_pth {P : Type} [is_trunc 1 P] {Pe : G → P} {Pp : Π⦃a b⦄ (f : a ⟶ b), Pe a = Pe b}
+    (Pcomp : Π⦃a b c⦄ (g : b ⟶ c) (f : a ⟶ b), Pp (g ∘ f) = Pp f ⬝ Pp g) {a b : G} (f : a ⟶ b) :
+    ap (elim Pe Pp Pcomp) (pth f) = Pp f :=
+  !elim_incl1
+
+  -- The following rule is also true because P is a 1-type, and can be proven by `!is_set.elims`
+  -- The following is the canonical proofs which holds for any truncated two-quotient.
+  theorem elim_resp_comp {P : Type} [is_trunc 1 P] {Pe : G → P}
+    {Pp : Π⦃a b⦄ (f : a ⟶ b), Pe a = Pe b}
+    (Pcomp : Π⦃a b c⦄ (g : b ⟶ c) (f : a ⟶ b), Pp (g ∘ f) = Pp f ⬝ Pp g)
+    {a b c : G} (g : b ⟶ c) (f : a ⟶ b)
+    : square (ap02 (elim Pe Pp Pcomp) (resp_comp g f))
+             (Pcomp g f)
+             (elim_pth Pcomp (g ∘ f))
+             (!ap_con ⬝ (elim_pth Pcomp f ◾ elim_pth Pcomp g)) :=
+  proof !elim_incl2 qed
+
+  protected definition elim_set.{u} (Pe : G → Set.{u}) (Pp : Π⦃a b⦄ (f : a ⟶ b), Pe a ≃ Pe b)
+    (Pcomp : Π⦃a b c⦄ (g : b ⟶ c) (f : a ⟶ b) (x : Pe a), Pp (g ∘ f) x = Pp g (Pp f x))
+    (x : groupoid_quotient) : Set.{u} :=
+  elim Pe (λa b f, tua (Pp f)) (λa b c g f, ap tua (equiv_eq (Pcomp g f)) ⬝ !tua_trans) x
+
+  theorem elim_set_pth {Pe : G → Set} {Pp : Π⦃a b⦄ (f : a ⟶ b), Pe a ≃ Pe b}
+    (Pcomp : Π⦃a b c⦄ (g : b ⟶ c) (f : a ⟶ b) (x : Pe a), Pp (g ∘ f) x = Pp g (Pp f x))
+    {a b : G} (f : a ⟶ b) :
+    transport (elim_set Pe Pp Pcomp) (pth f) = Pp f :=
+  by rewrite [tr_eq_cast_ap_fn, ↑elim_set, ▸*, ap_compose' trunctype.carrier, elim_pth];
+     apply tcast_tua_fn
+
+end
+end groupoid_quotient
+
+attribute groupoid_quotient.elt [constructor]
+attribute groupoid_quotient.rec groupoid_quotient.elim [unfold 7] [recursor 7]
+attribute groupoid_quotient.rec_on groupoid_quotient.elim_on [unfold 4]
+attribute groupoid_quotient.set_rec groupoid_quotient.set_elim [unfold 6]
+attribute groupoid_quotient.prop_rec groupoid_quotient.prop_elim
+          groupoid_quotient.elim_set [unfold 5]
+
+
+open sigma pi is_conn function
+namespace groupoid_quotient
+section
+  universe variables u v
+  variables {G : Groupoid.{u v}} (a : G) {b c : G}
+
+  include a
+
+  protected definition code [unfold 3] (x : groupoid_quotient G) : Set.{v} :=
+  begin
+    refine groupoid_quotient.elim_set _ _ _ x,
+    { intro b, exact homset a b},
+    { intro b c g, exact equiv_postcompose g},
+    { intro b c d h g f, esimp at *, apply assoc'}
+  end
+
+  omit a
+
+  local abbreviation code [unfold 3] := @groupoid_quotient.code G a
+
+  variable {a}
+  protected definition encode [unfold 4] (x : groupoid_quotient G) (p : elt a = x) : code a x :=
+  transport (code a) p (ID a)
+
+  protected definition decode [unfold 3] (x : groupoid_quotient G) (z : code a x) : elt a = x :=
+  begin
+    induction x using groupoid_quotient.set_rec with b b c g,
+    { esimp, exact pth z},
+    { apply arrow_pathover_left, esimp, intro f, apply eq_pathover_constant_left_id_right,
+      apply square_of_eq, refine !resp_comp⁻¹ ⬝ _ ⬝ !idp_con⁻¹, rewrite elim_set_pth}
+  end
+
+  local abbreviation encode [unfold_full] := @groupoid_quotient.encode G a
+  local abbreviation decode [unfold 3] := @groupoid_quotient.decode G a
+
+  protected definition decode_encode (x : groupoid_quotient G) (p : elt a = x) :
+    decode x (encode x p) = p :=
+  begin induction p, esimp, apply resp_id end
+
+  protected definition encode_decode (x : groupoid_quotient G) (z : code a x) :
+    encode x (decode x z) = z :=
+  begin
+    induction x using groupoid_quotient.prop_rec with b,
+    esimp, refine ap10 !elim_set_pth.{u v v} (ID a) ⬝ _, esimp,
+    apply id_right
+  end
+
+  definition decode_comp (z : code a (elt b)) (z' : code b (elt c)) :
+    decode (elt c) (z' ∘ z) = decode (elt b) z ⬝ decode (elt c) z' :=
+  !resp_comp
+
+  variables (a b)
+  definition elt_eq_elt_equiv [constructor] : (elt a = elt b) ≃ (a ⟶ b) :=
+  equiv.MK (encode (elt b)) (decode (elt b))
+           (groupoid_quotient.encode_decode (elt b)) (groupoid_quotient.decode_encode (elt b))
+
+  variables {a b}
+  definition encode_con (p : elt a = elt b)
+    (q : elt b = elt c) : encode (elt c) (p ⬝ q) = encode (elt c) q ∘ encode (elt b) p :=
+  begin
+    apply eq_of_fn_eq_fn (elt_eq_elt_equiv a c)⁻¹ᵉ,
+    refine !right_inv ⬝ _ ⬝ !decode_comp⁻¹,
+    apply concat2, do 2 exact (to_left_inv !elt_eq_elt_equiv _)⁻¹
+  end
+
+  variable (G)
+  definition is_conn_groupoid_quotient [H : is_conn 0 G] : is_conn 0 (groupoid_quotient G) :=
+  begin
+    have g : trunc 0 G, from !center,
+    induction g with g,
+    have p : Πh, ∥ g = h ∥,
+    begin
+      intro h, refine !tr_eq_tr_equiv _, apply is_prop.elim
+    end,
+    fapply is_contr.mk,
+    { apply trunc_functor 0 elt (tr g)},
+    { intro x, induction x with x,
+      induction x using groupoid_quotient.prop_rec with b, esimp,
+      induction p b with q, exact ap (tr ∘ elt) q}
+  end
+
+end
+
+end groupoid_quotient
--- a/hott/hit/hit.md
+++ b/hott/hit/hit.md
@ -23,4 +23,5 @@ Files in this folder:

 The following hits have also 2-constructors. They are defined only using quotients.
 * [two_quotient](two_quotient.hlean): Quotients where you can also specify 2-paths. These are used for all hits which have 2-constructors, and they are almost fully general for such hits, as long as they are nonrecursive
-* [refl_quotient](refl_quotient.hlean): Quotients where you can also specify 2-paths
+* [refl_quotient](refl_quotient.hlean): Quotients where you can also specify 2-paths
+* [groupoid_quotient](groupoid_quotient.hlean): The realization or quotient of a groupoid.
--- a/hott/hit/pushout.hlean
+++ b/hott/hit/pushout.hlean
@ -1,7 +1,7 @@
 /-
-Copyright (c) 2015 Floris van Doorn. All rights reserved.
+Copyright (c) 2015-16 Floris van Doorn. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Floris van Doorn
+Authors: Floris van Doorn, Ulrik Buchholtz

 Declaration and properties of the pushout
 -/
--- a/hott/hit/two_quotient.hlean
+++ b/hott/hit/two_quotient.hlean
@ -10,7 +10,7 @@ import homotopy.circle eq2 algebra.e_closure cubical.squareover cubical.cube cub
 open quotient eq circle sum sigma equiv function relation e_closure

  /-
-    This files defines a general class of nonrecursive HITs using just quotients.
+    This files defines a general class of nonrecursive 2-HITs using just quotients.
    We can define any HIT X which has
    - a single 0-constructor
       f : A → X (for some type A)
@ -27,6 +27,15 @@ open quotient eq circle sum sigma equiv function relation e_closure

    so an example 2-constructor could be (as long as it typechecks):
      ap f q' ⬝ ((e r)⁻¹ ⬝ ap f q)⁻¹ ⬝ e r' = idp
+
+    We first define "simple two quotients" which have as requirement that the right hand side is idp
+    Then we define "two quotients" which can have an arbitrary path on the right hand side
+    Then we define "truncated two quotients", which is a two quotient followed by n-truncation,
+    and show that this satisfies the desired induction principle and computation rule.
+
+    Caveat: for none of these constructions we show that the induction priniciple computes on
+    2-paths. However, with truncated two quotients, if the truncation is a 1-truncation, then this
+    computation rule follows automatically, since the target is a 1-type.
  -/

 namespace simple_two_quotient
@ -489,3 +498,160 @@ attribute two_quotient.rec two_quotient.elim [unfold 8] [recursor 8]
 --attribute two_quotient.elim_type [unfold 9]
 attribute two_quotient.rec_on two_quotient.elim_on [unfold 5]
 --attribute two_quotient.elim_type_on [unfold 6]
+
+open two_quotient is_trunc trunc
+
+namespace trunc_two_quotient
+
+  section
+  parameters (n : ℕ₋₂) {A : Type}
+             (R : A → A → Type)
+  local abbreviation T := e_closure R -- the (type-valued) equivalence closure of R
+  parameter (Q : Π⦃a a'⦄, T a a' → T a a' → Type)
+  variables ⦃a a' a'' : A⦄ {s : R a a'} {t t' : T a a'}
+
+  definition trunc_two_quotient := trunc n (two_quotient R Q)
+
+  parameters {n R Q}
+  definition incl0 (a : A) : trunc_two_quotient := tr (!incl0 a)
+  definition incl1 (s : R a a') : incl0 a = incl0 a' := ap tr (!incl1 s)
+  definition incltw (t : T a a') : incl0 a = incl0 a' := ap tr (!inclt t)
+  definition inclt (t : T a a') : incl0 a = incl0 a' := e_closure.elim incl1 t
+  definition incl2w (q : Q t t') : incltw t = incltw t' :=
+  ap02 tr (!incl2 q)
+  definition incl2 (q : Q t t') : inclt t = inclt t' :=
+  !ap_e_closure_elim⁻¹ ⬝ ap02 tr (!incl2 q) ⬝ !ap_e_closure_elim
+
+  local attribute trunc_two_quotient incl0 [reducible]
+  definition is_trunc_trunc_two_quotient [instance] : is_trunc n trunc_two_quotient := _
+
+  protected definition rec {P : trunc_two_quotient → Type} [H : Πx, is_trunc n (P x)]
+    (P0 : Π(a : A), P (incl0 a))
+    (P1 : Π⦃a a' : A⦄ (s : R a a'), P0 a =[incl1 s] P0 a')
+    (P2 : Π⦃a a' : A⦄ ⦃t t' : T a a'⦄ (q : Q t t'),
+      change_path (incl2 q) (e_closure.elimo incl1 P1 t) = e_closure.elimo incl1 P1 t')
+    (x : trunc_two_quotient) : P x :=
+  begin
+    induction x,
+    induction a,
+    { exact P0 a},
+    { exact !pathover_of_pathover_ap (P1 s)},
+    { exact abstract [irreducible]
+      by rewrite [+ e_closure_elimo_ap, ↓incl1, -P2 q, change_path_pathover_of_pathover_ap,
+                  - + change_path_con, ↑incl2, con_inv_cancel_right] end}
+  end
+
+  protected definition rec_on [reducible] {P : trunc_two_quotient → Type} [H : Πx, is_trunc n (P x)]
+    (x : trunc_two_quotient)
+    (P0 : Π(a : A), P (incl0 a))
+    (P1 : Π⦃a a' : A⦄ (s : R a a'), P0 a =[incl1 s] P0 a')
+    (P2 : Π⦃a a' : A⦄ ⦃t t' : T a a'⦄ (q : Q t t'),
+      change_path (incl2 q) (e_closure.elimo incl1 P1 t) = e_closure.elimo incl1 P1 t') : P x :=
+  rec P0 P1 P2 x
+
+  theorem rec_incl1 {P : trunc_two_quotient → Type} [H : Πx, is_trunc n (P x)]
+    (P0 : Π(a : A), P (incl0 a))
+    (P1 : Π⦃a a' : A⦄ (s : R a a'), P0 a =[incl1 s] P0 a')
+    (P2 : Π⦃a a' : A⦄ ⦃t t' : T a a'⦄ (q : Q t t'),
+      change_path (incl2 q) (e_closure.elimo incl1 P1 t) = e_closure.elimo incl1 P1 t')
+    ⦃a a' : A⦄ (s : R a a') : apd (rec P0 P1 P2) (incl1 s) = P1 s :=
+  !apd_ap ⬝ ap !pathover_ap !rec_incl1 ⬝ to_right_inv !pathover_compose (P1 s)
+
+  theorem rec_inclt {P : trunc_two_quotient → Type} [H : Πx, is_trunc n (P x)]
+    (P0 : Π(a : A), P (incl0 a))
+    (P1 : Π⦃a a' : A⦄ (s : R a a'), P0 a =[incl1 s] P0 a')
+    (P2 : Π⦃a a' : A⦄ ⦃t t' : T a a'⦄ (q : Q t t'),
+      change_path (incl2 q) (e_closure.elimo incl1 P1 t) = e_closure.elimo incl1 P1 t')
+    ⦃a a' : A⦄ (t : T a a') : apd (rec P0 P1 P2) (inclt t) = e_closure.elimo incl1 P1 t :=
+  ap_e_closure_elimo_h incl1 P1 (rec_incl1 P0 P1 P2) t
+
+  protected definition elim {P : Type} (P0 : A → P) [H : is_trunc n P]
+    (P1 : Π⦃a a' : A⦄ (s : R a a'), P0 a = P0 a')
+    (P2 : Π⦃a a' : A⦄ ⦃t t' : T a a'⦄ (q : Q t t'), e_closure.elim P1 t = e_closure.elim P1 t')
+    (x : trunc_two_quotient) : P :=
+  begin
+    induction x,
+    induction a,
+    { exact P0 a},
+    { exact P1 s},
+    { exact P2 q},
+  end
+  local attribute elim [unfold 10]
+
+  protected definition elim_on {P : Type} [H : is_trunc n P] (x : trunc_two_quotient) (P0 : A → P)
+    (P1 : Π⦃a a' : A⦄ (s : R a a'), P0 a = P0 a')
+    (P2 : Π⦃a a' : A⦄ ⦃t t' : T a a'⦄ (q : Q t t'), e_closure.elim P1 t = e_closure.elim P1 t')
+     : P :=
+  elim P0 P1 P2 x
+
+  definition elim_incl1 {P : Type} [H : is_trunc n P] {P0 : A → P}
+    {P1 : Π⦃a a' : A⦄ (s : R a a'), P0 a = P0 a'}
+    (P2 : Π⦃a a' : A⦄ ⦃t t' : T a a'⦄ (q : Q t t'), e_closure.elim P1 t = e_closure.elim P1 t')
+    ⦃a a' : A⦄ (s : R a a') : ap (elim P0 P1 P2) (incl1 s) = P1 s :=
+  !ap_compose⁻¹ ⬝ !elim_incl1
+
+  definition elim_inclt {P : Type} [H : is_trunc n P] {P0 : A → P}
+    {P1 : Π⦃a a' : A⦄ (s : R a a'), P0 a = P0 a'}
+    (P2 : Π⦃a a' : A⦄ ⦃t t' : T a a'⦄ (q : Q t t'), e_closure.elim P1 t = e_closure.elim P1 t')
+    ⦃a a' : A⦄ (t : T a a') : ap (elim P0 P1 P2) (inclt t) = e_closure.elim P1 t :=
+  ap_e_closure_elim_h incl1 (elim_incl1 P2) t
+
+  open function
+
+  theorem elim_incl2 {P : Type} [H : is_trunc n P] (P0 : A → P)
+    (P1 : Π⦃a a' : A⦄ (s : R a a'), P0 a = P0 a')
+    (P2 : Π⦃a a' : A⦄ ⦃t t' : T a a'⦄ (q : Q t t'), e_closure.elim P1 t = e_closure.elim P1 t')
+    ⦃a a' : A⦄ ⦃t t' : T a a'⦄ (q : Q t t')
+    : square (ap02 (elim P0 P1 P2) (incl2 q)) (P2 q) (elim_inclt P2 t) (elim_inclt P2 t') :=
+  begin
+    note Ht' := ap_ap_e_closure_elim tr (elim P0 P1 P2) (two_quotient.incl1 R Q) t',
+    note Ht := ap_ap_e_closure_elim tr (elim P0 P1 P2) (two_quotient.incl1 R Q) t,
+    note Hn := natural_square (ap_compose (elim P0 P1 P2) tr) (two_quotient.incl2 R Q q),
+    note H7 := eq_top_of_square (Ht⁻¹ʰ ⬝h Hn⁻¹ᵛ ⬝h Ht'), clear [Hn, Ht, Ht'],
+    unfold [ap02,incl2], rewrite [+ap_con,ap_inv,-ap_compose (ap _)],
+    xrewrite [H7, ↑function.compose, eq_top_of_square (elim_incl2 P0 P1 P2 q)], clear [H7],
+    have H : Π(t : T a a'),
+      ap_e_closure_elim (elim P0 P1 P2) (λa a' (r : R a a'), ap tr (two_quotient.incl1 R Q r)) t ⬝
+      (ap_e_closure_elim_h (two_quotient.incl1 R Q)
+        (λa a' (s : R a a'), ap_compose (elim P0 P1 P2) tr (two_quotient.incl1 R Q s)) t)⁻¹ ⬝
+      two_quotient.elim_inclt P2 t = elim_inclt P2 t, from
+        ap_e_closure_elim_h_zigzag (elim P0 P1 P2)
+                                   (two_quotient.incl1 R Q)
+                                   (two_quotient.elim_incl1 P2),
+    rewrite [con.assoc5, con.assoc5, H t, -inv_con_inv_right, -con_inv], xrewrite [H t'],
+    apply top_deg_square
+  end
+
+  definition elim_inclt_rel [unfold_full] {P : Type} [is_trunc n P] {P0 : A → P}
+    {P1 : Π⦃a a' : A⦄ (s : R a a'), P0 a = P0 a'}
+    (P2 : Π⦃a a' : A⦄ ⦃t t' : T a a'⦄ (q : Q t t'), e_closure.elim P1 t = e_closure.elim P1 t')
+    ⦃a a' : A⦄ (r : R a a') : elim_inclt P2 [r] = elim_incl1 P2 r :=
+  idp
+
+  definition elim_inclt_inv [unfold_full] {P : Type} [is_trunc n P] {P0 : A → P}
+    {P1 : Π⦃a a' : A⦄ (s : R a a'), P0 a = P0 a'}
+    (P2 : Π⦃a a' : A⦄ ⦃t t' : T a a'⦄ (q : Q t t'), e_closure.elim P1 t = e_closure.elim P1 t')
+    ⦃a a' : A⦄ (t : T a a')
+    : elim_inclt P2 t⁻¹ʳ = ap_inv (elim P0 P1 P2) (inclt t) ⬝ (elim_inclt P2 t)⁻² :=
+  idp
+
+  definition elim_inclt_con [unfold_full] {P : Type} [is_trunc n P] {P0 : A → P}
+    {P1 : Π⦃a a' : A⦄ (s : R a a'), P0 a = P0 a'}
+    (P2 : Π⦃a a' : A⦄ ⦃t t' : T a a'⦄ (q : Q t t'), e_closure.elim P1 t = e_closure.elim P1 t')
+    ⦃a a' a'' : A⦄ (t : T a a') (t': T a' a'')
+    : elim_inclt P2 (t ⬝r t') =
+        ap_con (elim P0 P1 P2) (inclt t) (inclt t') ⬝ (elim_inclt P2 t ◾ elim_inclt P2 t') :=
+  idp
+
+  definition inclt_rel [unfold_full] (r : R a a') : inclt [r] = incl1 r := idp
+  definition inclt_inv [unfold_full] (t : T a a') : inclt t⁻¹ʳ = (inclt t)⁻¹ := idp
+  definition inclt_con [unfold_full] (t : T a a') (t' : T a' a'')
+    : inclt (t ⬝r t') = inclt t ⬝ inclt t' := idp
+
+
+end
+end trunc_two_quotient
+
+attribute trunc_two_quotient.incl0 [constructor]
+attribute trunc_two_quotient.rec trunc_two_quotient.elim [unfold 10] [recursor 10]
+attribute trunc_two_quotient.rec_on trunc_two_quotient.elim_on [unfold 7]
--- a/hott/homotopy/EM.hlean
+++ b/hott/homotopy/EM.hlean
@ -0,0 +1,259 @@
+/-
+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
+
+Eilenberg MacLane spaces
+-/
+
+import hit.groupoid_quotient .hopf .freudenthal .homotopy_group
+open algebra pointed nat eq category group algebra is_trunc iso pointed unit trunc equiv is_conn
+
+namespace EM
+  open groupoid_quotient
+
+  variable {G : Group}
+  definition EM1 (G : Group) : Type :=
+  groupoid_quotient (Groupoid_of_Group G)
+  definition pEM1 [constructor] (G : Group) : Type* :=
+  pointed.MK (EM1 G) (elt star)
+
+  definition base : EM1 G := elt star
+  definition pth : G → base = base := pth
+  definition resp_mul (g h : G) : pth (g * h) = pth g ⬝ pth h := resp_comp h g
+  definition resp_one : pth (1 : G) = idp :=
+  resp_id star
+
+  definition resp_inv (g : G) : pth (g⁻¹) = (pth g)⁻¹ :=
+  resp_inv g
+
+  local attribute pointed.MK pointed.carrier pEM1 EM1 [reducible]
+  protected definition rec {P : EM1 G → Type} [H : Π(x : EM1 G), is_trunc 1 (P x)]
+    (Pb : P base) (Pp : Π(g : G), Pb =[pth g] Pb)
+    (Pmul : Π(g h : G), change_path (resp_mul g h) (Pp (g * h)) = Pp g ⬝o Pp h) (x : EM1 G) : P x :=
+  begin
+    induction x,
+    { induction g, exact Pb},
+    { induction a, induction b, exact Pp f},
+    { induction a, induction b, induction c, exact Pmul f g}
+  end
+
+  protected definition rec_on {P : EM1 G → Type} [H : Π(x : EM1 G), is_trunc 1 (P x)]
+    (x : EM1 G) (Pb : P base) (Pp : Π(g : G), Pb =[pth g] Pb)
+    (Pmul : Π(g h : G), change_path (resp_mul g h) (Pp (g * h)) = Pp g ⬝o Pp h) : P x :=
+  EM.rec Pb Pp Pmul x
+
+  protected definition set_rec {P : EM1 G → Type} [H : Π(x : EM1 G), is_set (P x)]
+    (Pb : P base) (Pp : Π(g : G), Pb =[pth g] Pb) (x : EM1 G) : P x :=
+  EM.rec Pb Pp !center x
+
+  protected definition prop_rec {P : EM1 G → Type} [H : Π(x : EM1 G), is_prop (P x)]
+    (Pb : P base) (x : EM1 G) : P x :=
+  EM.rec Pb !center !center x
+
+  definition rec_pth {P : EM1 G → Type} [H : Π(x : EM1 G), is_trunc 1 (P x)]
+    {Pb : P base} {Pp : Π(g : G), Pb =[pth g] Pb}
+    (Pmul : Π(g h : G), change_path (resp_mul g h) (Pp (g * h)) = Pp g ⬝o Pp h)
+    (g : G) : apd (EM.rec Pb Pp Pmul) (pth g) = Pp g :=
+  proof !rec_pth qed
+
+  protected definition elim {P : Type} [is_trunc 1 P] (Pb : P) (Pp : Π(g : G), Pb = Pb)
+    (Pmul : Π(g h : G), Pp (g * h) = Pp g ⬝ Pp h) (x : EM1 G) : P :=
+  begin
+    induction x,
+    { exact Pb},
+    { exact Pp f},
+    { exact Pmul f g}
+  end
+
+  protected definition elim_on [reducible] {P : Type} [is_trunc 1 P] (x : EM1 G)
+    (Pb : P) (Pp : G → Pb = Pb) (Pmul : Π(g h : G), Pp (g * h) = Pp g ⬝ Pp h) : P :=
+  EM.elim Pb Pp Pmul x
+
+  protected definition set_elim [reducible] {P : Type} [is_set P] (Pb : P) (Pp : G → Pb = Pb)
+    (x : EM1 G) : P :=
+  EM.elim Pb Pp !center x
+
+  protected definition prop_elim [reducible] {P : Type} [is_prop P] (Pb : P) (x : EM1 G) : P :=
+  EM.elim Pb !center !center x
+
+  definition elim_pth {P : Type} [is_trunc 1 P] {Pb : P} {Pp : G → Pb = Pb}
+    (Pmul : Π(g h : G), Pp (g * h) = Pp g ⬝ Pp h) (g : G) : ap (EM.elim Pb Pp Pmul) (pth g) = Pp g :=
+  proof !elim_pth qed
+
+  protected definition elim_set.{u} (Pb : Set.{u}) (Pp : Π(g : G), Pb ≃ Pb)
+    (Pmul : Π(g h : G) (x : Pb), Pp (g * h) x = Pp h (Pp g x)) (x : EM1 G) : Set.{u} :=
+  groupoid_quotient.elim_set (λu, Pb) (λu v, Pp) (λu v w g h, proof Pmul h g qed) x
+
+  theorem elim_set_pth {Pb : Set} {Pp : Π(g : G), Pb ≃ Pb}
+    (Pmul : Π(g h : G) (x : Pb), Pp (g * h) x = Pp h (Pp g x)) (g : G) :
+    transport (EM.elim_set Pb Pp Pmul) (pth g) = Pp g :=
+  !elim_set_pth
+
+end EM
+
+-- attribute EM.rec EM.elim [recursor 7]
+attribute EM.base [constructor]
+attribute EM.rec EM.elim [unfold 7] [recursor 7]
+attribute EM.rec_on EM.elim_on [unfold 4]
+attribute EM.set_rec EM.set_elim [unfold 6]
+attribute EM.prop_rec EM.prop_elim EM.elim_set [unfold 5]
+
+namespace EM
+  open groupoid_quotient
+
+  definition base_eq_base_equiv [constructor] (G : Group) : (base = base :> pEM1 G) ≃ G :=
+  !elt_eq_elt_equiv
+
+  definition fundamental_group_pEM1 (G : Group) : π₁ (pEM1 G) ≃g G :=
+  begin
+    fapply isomorphism_of_equiv,
+    { exact trunc_equiv_trunc 0 !base_eq_base_equiv ⬝e trunc_equiv 0 G},
+    { intros g h, induction g with p, induction h with q,
+      exact encode_con p q}
+  end
+
+  proposition is_trunc_pEM1 [instance] (G : Group) : is_trunc 1 (pEM1 G) :=
+  !is_trunc_groupoid_quotient
+
+  proposition is_trunc_EM1 [instance] (G : Group) : is_trunc 1 (EM1 G) :=
+  !is_trunc_groupoid_quotient
+
+  proposition is_conn_EM1 [instance] (G : Group) : is_conn 0 (EM1 G) :=
+  by apply @is_conn_groupoid_quotient; esimp; exact _
+
+  proposition is_conn_pEM1 [instance] (G : Group) : is_conn 0 (pEM1 G) :=
+  is_conn_EM1 G
+
+  -- TODO: prove this using truncated Whitehead.
+
+  definition EM1_map [unfold 7] {G : Group} {X : Type*} (e : Ω X ≃ G)
+    (r : Πp q, e (p ⬝ q) = e p * e q) [is_conn 0 X] [is_trunc 1 X] : EM1 G → X :=
+  begin
+    intro x, induction x using EM.elim,
+    { exact Point X},
+    { note p := e⁻¹ᵉ g, exact p},
+    { exact inv_preserve_binary e concat mul r g h}
+  end
+
+  -- TODO
+  -- definition EM1_equiv {G : Group} {X : Type*} (e : Ω X ≃ G)
+  --   (r : Πp q, e (p ⬝ q) = e p * e q) [is_conn 0 X] [is_trunc 1 X] : EM1 G ≃ X :=
+  -- begin
+  --   apply equiv.mk (EM1_map e r),
+  --   apply whiteheads_principle 1,
+  --   { apply is_equiv_of_is_contr},
+  --   { intro x n, cases n with n,
+  --     { exact sorry},
+  --     { apply @is_equiv_of_is_contr, do 2 exact sorry}}
+  -- end
+
+  -- definition pequiv_pEM1 {G : Group} {X : Type*} (e : π₁ X ≃g G) [is_conn 0 X] [is_trunc 1 X]
+  --   : X ≃* pEM1 G :=
+  -- sorry
+
+end EM
+
+open hopf susp
+namespace EM
+  -- The K(G,n+1):
+  variables (G : CommGroup) (n : ℕ)
+
+  definition EM1_mul [unfold 2 3] {G : CommGroup} (x x' : EM1 G) : EM1 G :=
+  begin
+    induction x,
+    { exact x'},
+    { induction x' using EM.set_rec,
+      { exact pth g},
+      { exact abstract begin apply loop_pathover, apply square_of_eq,
+          refine !resp_mul⁻¹ ⬝ _ ⬝ !resp_mul,
+          exact ap pth !mul.comm end end}},
+    { refine EM.prop_rec _ x', esimp, apply resp_mul},
+  end
+
+  definition EM1_mul_one (G : CommGroup) (x : EM1 G) : EM1_mul x base = x :=
+  begin
+    induction x using EM.set_rec,
+    { reflexivity},
+    { apply eq_pathover_id_right, apply hdeg_square, refine EM.elim_pth _ g}
+  end
+
+  definition h_space_EM1 [constructor] [instance] (G : CommGroup) : h_space (pEM1 G) :=
+  begin
+    fapply h_space.mk,
+    { exact EM1_mul},
+    { exact base},
+    { intro x', reflexivity},
+    { apply EM1_mul_one}
+  end
+
+  /- K(G, n+1) -/
+  definition EMadd1 (G : CommGroup) (n : ℕ) : Type* :=
+  ptrunc (n+1) (iterate_psusp n (pEM1 G))
+
+  definition loop_EM2 (G : CommGroup) : Ω[1] (EMadd1 G 1) ≃* pEM1 G :=
+  begin
+    apply hopf.delooping, reflexivity
+  end
+
+  definition homotopy_group_EM2 (G : CommGroup) : πg[1+1] (EMadd1 G 1) ≃g G :=
+  begin
+    refine ghomotopy_group_succ_in _ 0 ⬝g _,
+    refine homotopy_group_isomorphism_of_pequiv 0 (loop_EM2 G) ⬝g _,
+    apply fundamental_group_pEM1
+  end
+
+  definition homotopy_group_EMadd1 (G : CommGroup) (n : ℕ) : πg[n+1] (EMadd1 G n) ≃g G :=
+  begin
+    cases n with n,
+    { refine homotopy_group_isomorphism_of_pequiv 0 _ ⬝g fundamental_group_pEM1 G,
+      apply ptrunc_pequiv, apply is_trunc_pEM1},
+    induction n with n IH,
+    { apply homotopy_group_EM2 G},
+    refine _ ⬝g IH,
+    refine !ghomotopy_group_ptrunc ⬝g _ ⬝g !ghomotopy_group_ptrunc⁻¹ᵍ,
+    apply iterate_psusp_stability_isomorphism,
+    rexact add_mul_le_mul_add n 1 1
+  end
+
+  local attribute EMadd1 [reducible]
+  definition is_conn_EMadd1 (G : CommGroup) (n : ℕ) : is_conn n (EMadd1 G n) := _
+
+  definition is_trunc_EMadd1 (G : CommGroup) (n : ℕ) : is_trunc (n+1) (EMadd1 G n) := _
+
+  /- K(G, n+1) -/
+  definition EM (G : CommGroup) : ℕ → Type*
+  | 0     := pType_of_Group G
+  | (k+1) := EMadd1 G k
+
+  definition phomotopy_group_EM (G : CommGroup) (n : ℕ) : π*[n] (EM G n) ≃* pType_of_Group G :=
+  begin
+    cases n with n,
+    { rexact ptrunc_pequiv 0 (pType_of_Group G) _},
+    { apply pequiv_of_isomorphism (homotopy_group_EMadd1 G n)}
+  end
+
+  definition ghomotopy_group_EM (G : CommGroup) (n : ℕ) : πg[n+1] (EM G (n+1)) ≃g G :=
+  homotopy_group_EMadd1 G n
+
+  definition is_conn_EM [instance] (G : CommGroup) (n : ℕ) : is_conn (n.-1) (EM G n) :=
+  begin
+    cases n with n,
+    { apply is_conn_minus_one, apply tr, unfold [EM], exact 1},
+    { apply is_conn_EMadd1}
+  end
+
+  definition is_conn_EM_succ [instance] (G : CommGroup) (n : ℕ) : is_conn n (EM G (succ n)) :=
+  is_conn_EM G (succ n)
+
+  definition is_trunc_EM [instance] (G : CommGroup) (n : ℕ) : is_trunc n (EM G n) :=
+  begin
+    cases n with n,
+    { unfold [EM], apply semigroup.is_set_carrier},
+    { apply is_trunc_EMadd1}
+  end
+
+
+
+end EM
--- a/hott/homotopy/LES_of_homotopy_groups.hlean
+++ b/hott/homotopy/LES_of_homotopy_groups.hlean
@ -0,0 +1,826 @@
+/-
+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 eq2
+
+open eq pointed sigma fiber equiv is_equiv sigma.ops is_trunc nat trunc algebra function sum
+
+/--------------
+    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 3),
+    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,
+    do 3 (cases k with k; rotate 1),
+    { /-k≥3-/ exfalso, apply lt_le_antisymm H, apply le_add_left},
+    { /-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}},
+  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_t_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 (n : ℕ) : Π(x : fin (succ 2)),
+    group (LES_of_homotopy_groups (n + 1, x))
+  | (fin.mk 0     H) := begin rexact group_homotopy_group n Y end
+  | (fin.mk 1     H) := begin rexact group_homotopy_group n X end
+  | (fin.mk 2     H) := begin rexact group_homotopy_group n (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 Group_LES_of_homotopy_groups (x : +3ℕ) : Group.{u} :=
+  Group.mk (LES_of_homotopy_groups (nat.succ (pr1 x), pr2 x))
+           (group_LES_of_homotopy_groups (pr1 x) (pr2 x))
+
+  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ℕ),
+    Group_LES_of_homotopy_groups (S k) →g Group_LES_of_homotopy_groups k
+  | (k, fin.mk 0 H) :=
+    proof homomorphism.mk (cc_to_fn LES_of_homotopy_groups (k + 1, 0))
+                          (phomotopy_group_functor_mul _ _) qed
+  | (k, fin.mk 1 H) :=
+    proof homomorphism.mk (cc_to_fn LES_of_homotopy_groups (k + 1, 1))
+                          (phomotopy_group_functor_mul _ _) qed
+  | (k, fin.mk 2 H) :=
+    begin
+      apply homomorphism.mk (cc_to_fn LES_of_homotopy_groups (k + 1, 2)),
+      exact abstract begin rewrite [LES_of_homotopy_groups_fun_2],
+      refine @is_homomorphism_compose _ _ _ _ _ _ (π→*[k + 1] boundary_map) _ _ _,
+      { 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
+
+  /-
+    Fibration sequences
+
+    This is a similar construction, but with as input data two pointed maps,
+    and a pointed equivalence between the domain of the second map and the fiber of the first map,
+    and a pointed homotopy.
+  -/
+
+  section
+  universe variable u
+  parameters {F X Y : pType.{u}} (f : X →* Y) (g : F →* X) (e : pfiber f ≃* F)
+             (p : ppoint f ~* g ∘* e)
+  include f p
+  open succ_str prod nat
+  definition fibration_sequence_car [reducible] : +3ℕ → Type*
+  | (n, fin.mk 0 H) := Ω[n] Y
+  | (n, fin.mk 1 H) := Ω[n] X
+  | (n, fin.mk k H) := Ω[n] F
+
+  definition fibration_sequence_fun
+    : Π(n : +3ℕ), fibration_sequence_car (S n) →* fibration_sequence_car n
+  | (n, fin.mk 0 H) := proof Ω→[n] f qed
+  | (n, fin.mk 1 H) := proof Ω→[n] g qed
+  | (n, fin.mk 2 H) := proof Ω→[n] (e ∘* 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 fibration_sequence_pequiv : Π(x : +3ℕ),
+     loop_spaces2 f x ≃* fibration_sequence_car x
+  | (n, fin.mk 0 H) := by reflexivity
+  | (n, fin.mk 1 H) := by reflexivity
+  | (n, fin.mk 2 H) := loopn_pequiv_loopn n e
+  | (n, fin.mk (k+3) H) := begin exfalso, apply lt_le_antisymm H, apply le_add_left end
+
+  definition fibration_sequence_fun_phomotopy : Π(x : +3ℕ),
+    fibration_sequence_pequiv x ∘* loop_spaces_fun2 f x ~*
+      (fibration_sequence_fun x ∘* fibration_sequence_pequiv (S x))
+  | (n, fin.mk 0 H) := by reflexivity
+  | (n, fin.mk 1 H) :=
+    begin refine !pid_comp ⬝* _, refine apn_phomotopy n p ⬝* _,
+      refine !apn_compose ⬝* _, reflexivity end
+  | (n, fin.mk 2 H) := begin refine !passoc⁻¹* ⬝* _ ⬝* !comp_pid⁻¹*, apply pwhisker_right,
+      refine _ ⬝* !apn_compose⁻¹*, reflexivity end
+  | (n, fin.mk (k+3) H) := begin exfalso, apply lt_le_antisymm H, apply le_add_left end
+
+  definition type_fibration_sequence [constructor] : type_chain_complex +3ℕ :=
+  transfer_type_chain_complex
+    (LES_of_loop_spaces2 f)
+    fibration_sequence_fun
+    fibration_sequence_pequiv
+    fibration_sequence_fun_phomotopy
+
+  definition is_exact_type_fibration_sequence : is_exact_t type_fibration_sequence :=
+  begin
+    intro n,
+    apply is_exact_at_t_transfer,
+    apply is_exact_LES_of_loop_spaces2
+  end
+
+  definition fibration_sequence [constructor] : chain_complex +3ℕ :=
+  trunc_chain_complex type_fibration_sequence
+
+  end
+
+
+end chain_complex
--- a/hott/homotopy/chain_complex.hlean
+++ b/hott/homotopy/chain_complex.hlean
@ -0,0 +1,522 @@
+/-
+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
+
+Chain complexes.
+
+We define chain complexes in a general way as a sequence X of types indexes over an arbitrary type
+N with a successor S. There are maps X (S n) → X n for n : N. We can vary N to have chain complexes
+indexed by ℕ, ℤ, a finite type or something else, and for both ℕ and ℤ we can choose the maps to
+go up or down. We also use the indexing ℕ × 3 for the LES of homotopy groups, because then it
+computes better (see [LES_of_homotopy_groups]).
+
+We have two separate notions of
+chain complexes:
+- type_chain_complex: sequence of types, where exactness is formulated using pure existence.
+- chain_complex: sequence of sets, where exactness is formulated using mere existence.
+
+-/
+
+import types.int algebra.group_theory types.fin
+
+open eq pointed int unit is_equiv equiv is_trunc trunc function algebra group sigma.ops
+     sum prod nat bool fin
+
+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 : ℕ} (x : stratified_type N n)
+  : stratified_type N n :=
+(if val (pr2 x) = n then S (pr1 x) else pr1 x, cyclic_succ (pr2 x))
+
+definition stratified [reducible] [constructor] (N : succ_str) (n : ℕ) : succ_str :=
+succ_str.mk (stratified_type N n) stratified_succ
+
+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
+
+namespace chain_complex
+
+  /-
+    We define "type chain complexes" which are chain complexes without the
+    "set"-requirement. Exactness is formulated without propositional truncation.
+  -/
+  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)
+
+  section
+  variables {N : succ_str} (X : type_chain_complex N) (n : N)
+
+  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 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 :=
+  Π(n : N), is_exact_at_t X n
+
+  -- A chain complex on +ℕ can be trivially extended to a chain complex on +ℤ
+  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 tcc_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 tcc_is_chain_complex X n},
+      { esimp, intro x, reflexivity}
+    end
+
+  definition is_exact_t_from_left {X : type_chain_complex +ℕ} {n : ℕ}
+    (H : is_exact_at_t X n)
+    : is_exact_at_t (type_chain_complex_from_left X) (of_nat n) :=
+  H
+
+  /-
+    Given a natural isomorphism between a chain complex and any other sequence,
+    we can give the other sequence the structure of a chain complex, which is exact at the
+    positions where the original sequence is.
+  -/
+  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
+    abstract begin
+      intro n, apply equiv_rect (equiv_of_pequiv e), intro x,
+      refine ap g (p x)⁻¹ ⬝ _,
+      refine (p _)⁻¹ ⬝ _,
+      refine ap e (tcc_is_chain_complex X n _) ⬝ _,
+      apply respect_pt
+    end end
+
+  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 *,
+    have H2 : tcc_to_fn X n (e⁻¹ᵉ* y) = pt,
+    begin
+      refine (inv_commute (λn, equiv_of_pequiv e) _ _ @p _)⁻¹ᵖ ⬝ _,
+      refine ap _ q ⬝ _,
+      exact respect_pt e⁻¹ᵉ*
+    end,
+    cases (H _ H2) with x r,
+    refine fiber.mk (e x) _,
+    refine (p x)⁻¹ ⬝ _,
+    refine ap e r ⬝ _,
+    apply right_inv
+  end
+
+  /-
+    We want a theorem which states that if we have a chain complex, but with some
+    where the maps are composed by an equivalences, we want to remove this equivalence.
+    The following two theorems give sufficient conditions for when this is allowed.
+    We use this to transform the LES of homotopy groups where on the odd levels we have
+    maps -πₙ(...) into the LES of homotopy groups where we remove the minus signs (which
+    represents composition with path inversion).
+  -/
+  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
+
+  /-
+    A more general transfer theorem.
+    Here 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 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 (tcc_is_chain_complex X (f m) _) ⬝ _,
+      apply respect_pt
+    end
+
+  definition is_exact_at_t_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 *,
+    have H2 : tcc_to_fn X (f m) ((equiv_of_eq (ap (λx, X x) (c m)))⁻¹ᵉ (e⁻¹ y)) = pt,
+    begin
+      refine _ ⬝ ap e⁻¹ᵉ* q ⬝ (respect_pt (e⁻¹ᵉ*)), apply eq_inv_of_eq, clear q, revert y,
+      apply inv_homotopy_of_homotopy_pre e,
+      apply inv_homotopy_of_homotopy_pre, apply p
+    end,
+    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
+
+  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 cc_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 cc_is_chain_complex X n},
+      { esimp, intro x, reflexivity}
+    end
+
+  definition is_exact_from_left {X : chain_complex +ℕ} {n : ℕ} (H : is_exact_at X n)
+    : is_exact_at (chain_complex_from_left X) (of_nat 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 *,
+    have H2 : cc_to_fn X n (e⁻¹ᵉ* y) = pt,
+    begin
+      refine (inv_commute (λn, equiv_of_pequiv e) _ _ @p _)⁻¹ᵖ ⬝ _,
+      refine ap _ q ⬝ _,
+      exact respect_pt e⁻¹ᵉ*
+    end,
+    induction (H _ H2) with x r,
+    refine image.mk (e x) _,
+    refine (p x)⁻¹ ⬝ _,
+    refine ap e r ⬝ _,
+    apply right_inv
+  end
+
+  /- A type chain complex can be set-truncated to a chain complex -/
+  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 (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 (tcc_is_chain_complex X n x)
+    end
+
+  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 *,
+    note q := !tr_eq_tr_equiv p,
+    induction q with q,
+    induction H x q with y r,
+    refine image.mk (tr y) _,
+    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,
+      have H : Π (x : Y (f (S (S n)))), g (c n ▸ g (c (S n) ▸ x)) = pt,
+      begin
+        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
+      end,
+      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 *,
+    have H2 : cc_to_fn X n (e⁻¹ᵉ* ((c n)⁻¹ ▸ y)) = pt,
+    begin
+      refine (inv_commute (λn, equiv_of_pequiv e) _ _ @p _)⁻¹ᵖ ⬝ _,
+      rewrite [tr_inv_tr, q],
+      exact respect_pt e⁻¹ᵉ*
+    end,
+    induction (H _ H2) 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
+
+  /-
+    This is a start of a development of chain complexes consisting only on groups.
+    This might be useful to have in stable algebraic topology, but in the unstable case it's less
+    useful, since the smallest terms usually don't have a group structure.
+    We don't use it yet, so it's commented out for now
+  -/
+  -- 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 *,
+  --   have H2 : lgcc_to_fn X n (e⁻¹ᵉ* y) = pt,
+  --   begin
+  --     refine (inv_commute (λn, equiv_of_pequiv e) _ _ @p _)⁻¹ᵖ ⬝ _,
+  --     refine ap _ q ⬝ _,
+  --     exact respect_pt e⁻¹ᵉ*
+  --   end,
+  --   cases (H _ H2) with x r,
+  --   refine image.mk (e x) _,
+  --   refine (p x)⁻¹ ⬝ _,
+  --   refine ap e r ⬝ _,
+  --   apply right_inv
+  -- end
+
+  /-
+    The following theorems state that in a chain complex, if certain types are contractible, and
+    the chain complex is exact at the right spots, a map in the chain complex is an
+    embedding/surjection/equivalence. For the first and third we also need to assume that
+    the map is a group homomorphism (and hence that the two types around it are groups).
+  -/
+
+  definition is_embedding_of_trivial (X : chain_complex N) {n : N}
+    (H : is_exact_at X n) [HX : is_contr (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 x q,
+    have r : pt = x, from !is_prop.elim,
+    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_contr (X n)] : is_surjective (cc_to_fn X (S n)) :=
+  begin
+    intro g,
+    refine trunc.elim _ (H g !is_prop.elim),
+    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_contr (X n)] [HX2 : is_contr (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
--- a/hott/homotopy/circle.hlean
+++ b/hott/homotopy/circle.hlean
@ -285,8 +285,8 @@ namespace circle
  definition base_eq_base_equiv [constructor] : base = base ≃ ℤ :=
  circle_eq_equiv base

-  definition decode_add (a b : ℤ) : circle.decode a ⬝ circle.decode b = circle.decode (a +[ℤ] b) :=
-  !power_con_power
+  definition decode_add (a b : ℤ) : circle.decode (a +[ℤ] b) = circle.decode a ⬝ circle.decode b :=
+  !power_con_power⁻¹

  definition encode_con (p q : base = base)
    : circle.encode (p ⬝ q) = circle.encode p +[ℤ] circle.encode q :=
--- a/hott/homotopy/cofiber.hlean
+++ b/hott/homotopy/cofiber.hlean
@ -5,7 +5,7 @@ Authors: Jakob von Raumer

 The Cofiber Type
 -/
-import hit.pointed_pushout function .susp
+import hit.pointed_pushout function .susp types.unit

 open eq pushout unit pointed is_trunc is_equiv susp unit

--- a/hott/homotopy/complex_hopf.hlean
+++ b/hott/homotopy/complex_hopf.hlean
@ -1,15 +1,15 @@
 /-
 Copyright (c) 2016 Ulrik Buchholtz and Egbert Rijke. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Ulrik Buchholtz, Egbert Rijke
+Authors: Ulrik Buchholtz, Egbert Rijke, Floris van Doorn

 The H-space structure on S¹ and the complex Hopf fibration
 (the standard one).
 -/

-import .hopf .circle
+import .hopf .circle types.fin

-open eq equiv is_equiv circle is_conn trunc is_trunc sphere_index sphere susp
+open eq equiv is_equiv circle is_conn trunc is_trunc sphere susp pointed fiber sphere.ops function

 namespace hopf

@ -28,7 +28,7 @@ namespace hopf
      { apply is_prop.elimo, apply is_trunc_square } }
  end

-  open sphere.ops function
+  open sphere_index

  definition complex_hopf : S 3 → S 2 :=
  begin
@ -36,4 +36,18 @@ namespace hopf
    apply inv (hopf.total S¹), apply inv (join.spheres 1 1), exact x
  end

+  definition complex_phopf [constructor] : S. 3 →* S. 2 :=
+  proof pmap.mk complex_hopf idp qed
+
+  definition pfiber_complex_phopf : pfiber complex_phopf ≃* S. 1 :=
+  begin
+    fapply pequiv_of_equiv,
+    { esimp, unfold [complex_hopf],
+      refine fiber.equiv_precompose (sigma.pr1 ∘ (hopf.total S¹)⁻¹ᵉ)
+        (join.spheres (of_nat 1) (of_nat 1))⁻¹ᵉ _ ⬝e _,
+      refine fiber.equiv_precompose _ (hopf.total S¹)⁻¹ᵉ _ ⬝e _,
+      apply fiber_pr1},
+    { reflexivity}
+  end
+
 end hopf
--- a/hott/homotopy/connectedness.hlean
+++ b/hott/homotopy/connectedness.hlean
@ -3,7 +3,7 @@ Copyright (c) 2015 Ulrik Buchholtz. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Ulrik Buchholtz, Floris van Doorn
 -/
-import types.trunc types.arrow_2 types.fiber
+import types.trunc types.arrow_2 types.lift

 open eq is_trunc is_equiv nat equiv trunc function fiber funext pi

@ -199,7 +199,7 @@ namespace is_conn
        (fiber (λs x, s (Point A)) (λx, p))
        (fiber (λs, s (Point A)) p)
        k
-        (equiv.symm (fiber.equiv_postcompose (to_fun (arrow_unit_left (P (Point A))))))
+        (equiv.symm (fiber.equiv_postcompose _ (arrow_unit_left (P (Point A))) _))
        (is_conn_fun.elim_general n k (is_conn_fun_from_unit n A (Point A)) P (λx, p))
    end
  end is_conn
@ -251,6 +251,21 @@ namespace is_conn
  definition is_conn_minus_two (A : Type) : is_conn -2 A :=
  _

+  -- merely inhabited types are -1-connected
+  definition is_conn_minus_one (A : Type) (a : ∥ A ∥) : is_conn -1 A :=
+  is_contr.mk a (is_prop.elim _)
+
+  definition is_conn_trunc [instance] (A : Type) (n k : ℕ₋₂) [H : is_conn n A]
+    : is_conn n (trunc k A) :=
+  begin
+    apply is_trunc_equiv_closed, apply trunc_trunc_equiv_trunc_trunc
+  end
+
+  open pointed
+  definition is_conn_ptrunc [instance] (A : Type*) (n k : ℕ₋₂) [H : is_conn n A]
+    : is_conn n (ptrunc k A) :=
+  is_conn_trunc A n k
+
  -- the following trivial cases are solved by type class inference
  definition is_conn_of_is_contr (k : ℕ₋₂) (A : Type) [is_contr A] : is_conn k A := _
  definition is_conn_fun_of_is_equiv (k : ℕ₋₂) {A B : Type} (f : A → B) [is_equiv f] :
@ -301,4 +316,12 @@ namespace is_conn
    { exact is_conn_fun_trunc_functor_of_ge f H}
  end

+  open lift
+  definition is_conn_fun_lift_functor (n : ℕ₋₂) {A B : Type} (f : A → B) [is_conn_fun n f] :
+    is_conn_fun n (lift_functor f) :=
+  begin
+    intro b, cases b with b, apply is_trunc_equiv_closed_rev,
+    { apply trunc_equiv_trunc, apply fiber_lift_functor}
+  end
+
 end is_conn
--- a/hott/homotopy/cylinder.hlean
+++ b/hott/homotopy/cylinder.hlean
@ -117,6 +117,7 @@ namespace cylinder
  definition fseg (a : A) : fbase (f a) = ftop a :=
  fiber_eq (seg a) !elim_seg⁻¹

+-- TODO: define the induction principle for "fcylinder"
 --   set_option pp.notation false
 --   -- The induction principle for the dependent mapping cylinder (TODO)
 --   protected definition frec {P : Π(b), fcylinder f b → Type}
--- a/hott/homotopy/freudenthal.hlean
+++ b/hott/homotopy/freudenthal.hlean
@ -0,0 +1,241 @@
+/-
+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
+
+The Freudenthal Suspension Theorem
+-/
+
+import homotopy.wedge homotopy.circle
+
+open eq is_conn is_trunc pointed susp nat pi equiv is_equiv trunc fiber trunc_index
+
+namespace freudenthal section
+
+  parameters {A : Type*} {n : ℕ} [is_conn n A]
+
+  /-
+    This proof is ported from Agda
+    This is the 95% version of the Freudenthal Suspension Theorem, which means that we don't
+    prove that loop_susp_unit : A →* Ω(psusp A) is 2n-connected (if A is n-connected),
+    but instead we only prove that it induces an equivalence on the first 2n homotopy groups.
+  -/
+
+  private definition up (a : A) : north = north :> susp A :=
+  loop_susp_unit A a
+
+  definition code_merid : A → ptrunc (n + n) A → ptrunc (n + n) A :=
+  begin
+    have is_conn n (ptrunc (n + n) A), from !is_conn_trunc,
+    refine wedge_extension.ext n n (λ x y, ttrunc (n + n) A) _ _ _,
+    { exact tr},
+    { exact id},
+    { reflexivity}
+  end
+
+  definition code_merid_β_left (a : A) : code_merid a pt = tr a :=
+  by apply wedge_extension.β_left
+
+  definition code_merid_β_right (b : ptrunc (n + n) A) : code_merid pt b = b :=
+  by apply wedge_extension.β_right
+
+  definition code_merid_coh : code_merid_β_left pt = code_merid_β_right pt :=
+  begin
+    symmetry, apply eq_of_inv_con_eq_idp, apply wedge_extension.coh
+  end
+
+  definition is_equiv_code_merid (a : A) : is_equiv (code_merid a) :=
+  begin
+    have Πa, is_trunc n.-2.+1 (is_equiv (code_merid a)),
+      from λa, is_trunc_of_le _ !minus_one_le_succ,
+    refine is_conn.elim (n.-1) _ _ a,
+    { esimp, exact homotopy_closed id (homotopy.symm (code_merid_β_right))}
+  end
+
+  definition code_merid_equiv [constructor] (a : A) : trunc (n + n) A ≃ trunc (n + n) A :=
+  equiv.mk _ (is_equiv_code_merid a)
+
+  definition code_merid_inv_pt (x : trunc (n + n) A) : (code_merid_equiv pt)⁻¹ x = x :=
+  begin
+    refine ap010 @(is_equiv.inv _) _ x ⬝ _,
+    { exact homotopy_closed id (homotopy.symm code_merid_β_right)},
+    { apply is_conn.elim_β},
+    { reflexivity}
+  end
+
+  definition code [unfold 4] : susp A → Type :=
+  susp.elim_type (trunc (n + n) A) (trunc (n + n) A) code_merid_equiv
+
+  definition is_trunc_code (x : susp A) : is_trunc (n + n) (code x) :=
+  begin
+    induction x with a: esimp,
+    { exact _},
+    { exact _},
+    { apply is_prop.elimo}
+  end
+  local attribute is_trunc_code [instance]
+
+  definition decode_north [unfold 4] : code north → trunc (n + n) (north = north :> susp A) :=
+  trunc_functor (n + n) up
+
+  definition decode_north_pt : decode_north (tr pt) = tr idp :=
+  ap tr !con.right_inv
+
+  definition decode_south [unfold 4] : code south → trunc (n + n) (north = south :> susp A) :=
+  trunc_functor (n + n) merid
+
+  definition encode' {x : susp A} (p : north = x) : code x :=
+  transport code p (tr pt)
+
+  definition encode [unfold 5] {x : susp A} (p : trunc (n + n) (north = x)) : code x :=
+  begin
+    induction p with p,
+    exact transport code p (tr pt)
+  end
+
+  theorem encode_decode_north (c : code north) : encode (decode_north c) = c :=
+  begin
+    have H : Πc, is_trunc (n + n) (encode (decode_north c) = c), from _,
+    esimp at *,
+    induction c with a,
+    rewrite [↑[encode, decode_north, up, code], con_tr, elim_type_merid, ▸*,
+             code_merid_β_left, elim_type_merid_inv, ▸*, code_merid_inv_pt]
+  end
+
+  definition decode_coh_f (a : A) : tr (up pt) =[merid a] decode_south (code_merid a (tr pt)) :=
+  begin
+    refine _ ⬝op ap decode_south (code_merid_β_left a)⁻¹,
+    apply trunc_pathover,
+    apply eq_pathover_constant_left_id_right,
+    apply square_of_eq,
+    exact whisker_right !con.right_inv (merid a)
+  end
+
+  definition decode_coh_g (a' : A) : tr (up a') =[merid pt] decode_south (code_merid pt (tr a')) :=
+  begin
+    refine _ ⬝op ap decode_south (code_merid_β_right (tr a'))⁻¹,
+    apply trunc_pathover,
+    apply eq_pathover_constant_left_id_right,
+    apply square_of_eq, refine !inv_con_cancel_right ⬝ !idp_con⁻¹
+  end
+
+  definition decode_coh_lem {A : Type} {a a' : A} (p : a = a')
+    : whisker_right (con.right_inv p) p = inv_con_cancel_right p p ⬝ (idp_con p)⁻¹ :=
+  by induction p; reflexivity
+
+  theorem decode_coh (a : A) : decode_north =[merid a] decode_south :=
+  begin
+    apply arrow_pathover_left, intro c, esimp at *,
+    induction c with a',
+    rewrite [↑code, elim_type_merid, ▸*],
+    refine wedge_extension.ext n n _ _ _ _ a a',
+    { exact decode_coh_f},
+    { exact decode_coh_g},
+    { clear a a', unfold [decode_coh_f, decode_coh_g], refine ap011 concato_eq _ _,
+      { refine ap (λp, trunc_pathover (eq_pathover_constant_left_id_right (square_of_eq p))) _,
+        apply decode_coh_lem},
+      { apply ap (λp, ap decode_south p⁻¹), apply code_merid_coh}}
+  end
+
+  definition decode [unfold 4] {x : susp A} (c : code x) : trunc (n + n) (north = x) :=
+  begin
+    induction x with a,
+    { exact decode_north c},
+    { exact decode_south c},
+    { exact decode_coh a}
+  end
+
+  theorem decode_encode {x : susp A} (p : trunc (n + n) (north = x)) : decode (encode p) = p :=
+  begin
+    induction p with p, induction p, esimp, apply decode_north_pt
+  end
+
+  parameters (A n)
+  definition equiv' : trunc (n + n) A ≃ trunc (n + n) (Ω (psusp A)) :=
+  equiv.MK decode_north encode decode_encode encode_decode_north
+
+  definition pequiv' : ptrunc (n + n) A ≃* ptrunc (n + n) (Ω (psusp A)) :=
+  pequiv_of_equiv equiv' decode_north_pt
+
+  -- We don't prove this:
+  -- theorem freudenthal_suspension : is_conn_fun (n+n) (loop_susp_unit A) := sorry
+
+end end freudenthal
+
+open algebra group
+definition freudenthal_pequiv (A : Type*) {n k : ℕ} [is_conn n A] (H : k ≤ 2 * n)
+  : ptrunc k A ≃* ptrunc k (Ω (psusp A)) :=
+have H' : k ≤[ℕ₋₂] n + n,
+  by rewrite [mul.comm at H, -algebra.zero_add n at {1}]; exact of_nat_le_of_nat H,
+ptrunc_pequiv_ptrunc_of_le H' (freudenthal.pequiv' A n)
+
+definition freudenthal_equiv {A : Type*} {n k : ℕ} [is_conn n A] (H : k ≤ 2 * n)
+  : trunc k A ≃ trunc k (Ω (psusp A)) :=
+freudenthal_pequiv A H
+
+definition freudenthal_homotopy_group_pequiv (A : Type*) {n k : ℕ} [is_conn n A] (H : k ≤ 2 * n)
+  : π*[k + 1] (psusp A) ≃* π*[k] A  :=
+calc
+  π*[k + 1] (psusp A) ≃* π*[k] (Ω (psusp A)) : pequiv_of_eq (phomotopy_group_succ_in (psusp A) k)
+    ... ≃* Ω[k] (ptrunc k (Ω (psusp A)))     : phomotopy_group_pequiv_loop_ptrunc k (Ω (psusp A))
+    ... ≃* Ω[k] (ptrunc k A)                 : loopn_pequiv_loopn k (freudenthal_pequiv A H)
+    ... ≃* π*[k] A                           : (phomotopy_group_pequiv_loop_ptrunc k A)⁻¹ᵉ*
+
+definition freudenthal_homotopy_group_isomorphism (A : Type*) {n k : ℕ} [is_conn n A]
+  (H : k + 1 ≤ 2 * n) : πg[k+1 +1] (psusp A) ≃g πg[k+1] A :=
+begin
+  fapply isomorphism_of_equiv,
+  { exact equiv_of_pequiv (freudenthal_homotopy_group_pequiv A H)},
+  { intro g h,
+    refine _ ⬝ !phomotopy_group_pequiv_loop_ptrunc_inv_con,
+    apply ap !phomotopy_group_pequiv_loop_ptrunc⁻¹ᵉ*,
+    refine ap (loopn_pequiv_loopn _ _) _ ⬝ !loopn_pequiv_loopn_con,
+    refine ap !phomotopy_group_pequiv_loop_ptrunc _ ⬝ !phomotopy_group_pequiv_loop_ptrunc_con,
+    apply phomotopy_group_succ_in_con}
+end
+
+namespace susp
+
+  definition iterate_psusp_stability_pequiv (A : Type*) {k n : ℕ} [is_conn 0 A]
+    (H : k ≤ 2 * n) : π*[k + 1] (iterate_psusp (n + 1) A) ≃* π*[k] (iterate_psusp n A) :=
+  have is_conn n (iterate_psusp n A), by rewrite [-zero_add n]; exact _,
+  freudenthal_homotopy_group_pequiv (iterate_psusp n A) H
+
+  definition iterate_psusp_stability_isomorphism (A : Type*) {k n : ℕ} [is_conn 0 A]
+    (H : k + 1 ≤ 2 * n) : πg[k+1 +1] (iterate_psusp (n + 1) A) ≃g πg[k+1] (iterate_psusp n A) :=
+  have is_conn n (iterate_psusp n A), by rewrite [-zero_add n]; exact _,
+  freudenthal_homotopy_group_isomorphism (iterate_psusp n A) H
+
+  definition stability_helper1 {k n : ℕ} (H : k + 2 ≤ 2 * n) : k ≤ 2 * pred n :=
+  begin
+    rewrite [mul_pred_right], change pred (pred (k + 2)) ≤ pred (pred (2 * n)),
+    apply pred_le_pred, apply pred_le_pred, exact H
+  end
+
+  definition stability_helper2 (A : Type) {k n : ℕ} (H : k + 2 ≤ 2 * n) :
+    is_conn (pred n) (iterate_susp (n + 1) A) :=
+  have Π(n : ℕ), n = -2 + (succ n + 1),
+  begin intro n, induction n with n IH, reflexivity, exact ap succ IH end,
+  begin
+    cases n with n,
+    { exfalso, exact not_succ_le_zero _ H},
+    { esimp, rewrite [this n], apply is_conn_iterate_susp}
+  end
+
+  definition iterate_susp_stability_pequiv (A : Type) {k n : ℕ}
+    (H : k + 2 ≤ 2 * n) : π*[k + 1] (pointed.MK (iterate_susp (n + 2) A) !north) ≃*
+                          π*[k    ] (pointed.MK (iterate_susp (n + 1) A) !north) :=
+  have is_conn (pred n) (carrier (pointed.MK (iterate_susp (n + 1) A) !north)), from
+    stability_helper2 A H,
+  freudenthal_homotopy_group_pequiv (pointed.MK (iterate_susp (n + 1) A) !north)
+                                    (stability_helper1 H)
+
+  definition iterate_susp_stability_isomorphism (A : Type) {k n : ℕ}
+    (H : k + 3 ≤ 2 * n) : πg[k+1 +1] (pointed.MK (iterate_susp (n + 2) A) !north) ≃g
+                          πg[k+1]    (pointed.MK (iterate_susp (n + 1) A) !north) :=
+  have is_conn (pred n) (carrier (pointed.MK (iterate_susp (n + 1) A) !north)), from
+    @stability_helper2 A (k+1) n H,
+  freudenthal_homotopy_group_isomorphism (pointed.MK (iterate_susp (n + 1) A) !north)
+                                         (stability_helper1 H)
+
+end susp
--- a/hott/homotopy/homotopy.md
+++ b/hott/homotopy/homotopy.md
@ -15,12 +15,16 @@ folder (sorted such that files only import previous files).
 * [cofiber](cofiber.hlean)
 * [wedge](wedge.hlean)
 * [smash](smash.hlean)
-* [homotopy_group](homotopy_group.hlean) (theorems about homotopy groups. The definition and basic facts about homotopy groups is in [algebra/homotopy_group](../algebra/homotopy_group.hlean)).
 * [join](join.hlean)
+* [freudenthal](freudenthal.hlean) (The Freudenthal Suspension Theorem)
 * [hopf](hopf.hlean) (the Hopf construction and delooping of coherent connected H-spaces)
 * [complex_hopf](complex_hopf.hlean) (the complex Hopf fibration)
 * [imaginaroid](imaginaroid.hlean) (imaginaroids as a variant of the Cayley-Dickson construction)
 * [quaternionic_hopf](quaternionic_hopf.hlean) (the quaternionic Hopf fibration)
+* [chain_complex](chain_complex.hlean)
+* [LES_of_homotopy_groups](LES_of_homotopy_groups.hlean)
+* [homotopy_group](homotopy_group.hlean) (theorems about homotopy groups. The definition and basic facts about homotopy groups is in [algebra/homotopy_group](../algebra/homotopy_group.hlean))
+* [sphere2](sphere2.hlean) (calculation of the homotopy group of spheres)

 The following files depend on
 [hit.two_quotient](../hit/two_quotient.hlean) which on turn depends on
@ -28,3 +32,4 @@ The following files depend on

 * [red_susp](red_susp.hlean) (Reduced suspensions)
 * [torus](torus.hlean) (defined as a two-quotient)
+* [EM](EM.hlean): Eilenberg MacLane spaces
--- a/hott/homotopy/homotopy_group.hlean
+++ b/hott/homotopy/homotopy_group.hlean
@ -5,7 +5,7 @@ Authors: Floris van Doorn, Clive Newstead

 -/

-import algebra.homotopy_group .sphere
+import .LES_of_homotopy_groups .sphere .complex_hopf

 open eq is_trunc trunc_index pointed algebra trunc nat is_conn fiber pointed

@ -47,5 +47,105 @@ namespace is_trunc
    [H : is_conn_fun n f] (H2 : k ≤ n) : is_contr (π[k] (pfiber f)) :=
  @(trivial_homotopy_group_of_is_conn (pfiber f) H2) (H pt)

+  /- Corollaries of the LES of homotopy groups -/
+  local attribute comm_group.to_group [coercion]
+  local attribute is_equiv_tinverse [instance]
+  open prod chain_complex group fin equiv function is_equiv lift
+
+  /-
+    Because of the construction of the LES this proof only gives us this result when
+    A and B live in the same universe (because Lean doesn't have universe cumulativity).
+    However, below we also proof that it holds for A and B in arbitrary universes.
+  -/
+  theorem is_equiv_π_of_is_connected'.{u} {A B : pType.{u}} {n k : ℕ} (f : A →* B)
+     (H2 : k ≤ n) [H : is_conn_fun n f] : is_equiv (π→[k] f) :=
+  begin
+    cases k with k,
+    { /- k = 0 -/
+      change (is_equiv (trunc_functor 0 f)), apply is_equiv_trunc_functor_of_is_conn_fun,
+      refine is_conn_fun_of_le f (zero_le_of_nat n)},
+    { /- k > 0 -/
+     have H2' : k ≤ n, from le.trans !self_le_succ H2,
+      exact
+      @is_equiv_of_trivial _
+        (LES_of_homotopy_groups f) _
+        (is_exact_LES_of_homotopy_groups f (k, 2))
+        (is_exact_LES_of_homotopy_groups f (succ k, 0))
+        (@is_contr_HG_fiber_of_is_connected A B k n f H H2')
+        (@is_contr_HG_fiber_of_is_connected A B (succ k) n f H H2)
+        (@pgroup_of_group _ (group_LES_of_homotopy_groups f k 0) idp)
+        (@pgroup_of_group _ (group_LES_of_homotopy_groups f k 1) idp)
+        (homomorphism.struct (homomorphism_LES_of_homotopy_groups_fun f (k, 0)))},
+  end
+
+  theorem is_equiv_π_of_is_connected.{u v} {A : pType.{u}} {B : pType.{v}} {n k : ℕ} (f : A →* B)
+    (H2 : k ≤ n) [H : is_conn_fun n f] : is_equiv (π→[k] f) :=
+  begin
+    have π→*[k] pdown.{v u} ∘* π→*[k] (plift_functor f) ∘* π→*[k] pup.{u v} ~* π→*[k] f,
+    begin
+      refine pwhisker_left _ !phomotopy_group_functor_compose⁻¹* ⬝* _,
+      refine !phomotopy_group_functor_compose⁻¹* ⬝* _,
+      apply phomotopy_group_functor_phomotopy, apply plift_functor_phomotopy
+    end,
+    have π→[k] pdown.{v u} ∘ π→[k] (plift_functor f) ∘ π→[k] pup.{u v} ~ π→[k] f, from this,
+    apply is_equiv.homotopy_closed, rotate 1,
+    { exact this},
+    { do 2 apply is_equiv_compose,
+      { apply is_equiv_homotopy_group_functor, apply to_is_equiv !equiv_lift},
+      { refine @(is_equiv_π_of_is_connected' _ H2) _, apply is_conn_fun_lift_functor},
+      { apply is_equiv_homotopy_group_functor, apply to_is_equiv !equiv_lift⁻¹ᵉ}}
+  end
+
+  definition π_equiv_π_of_is_connected {A B : Type*} {n k : ℕ} (f : A →* B)
+     (H2 : k ≤ n) [H : is_conn_fun n f] : π*[k] A ≃* π*[k] B :=
+  pequiv_of_pmap (π→*[k] f) (is_equiv_π_of_is_connected f H2)
+
+  -- TODO: prove this for A and B in different universe levels
+  theorem is_surjective_π_of_is_connected.{u} {A B : pType.{u}} (n : ℕ) (f : A →* B)
+    [H : is_conn_fun n f] : is_surjective (π→[n + 1] f) :=
+  @is_surjective_of_trivial _
+    (LES_of_homotopy_groups f) _
+    (is_exact_LES_of_homotopy_groups f (n, 2))
+    (@is_contr_HG_fiber_of_is_connected A B n n f H !le.refl)
+
+  /-
+    Theorem 8.8.3: Whitehead's principle
+  -/
+  definition whiteheads_principle (n : ℕ₋₂) {A B : Type}
+    [HA : is_trunc n A] [HB : is_trunc n B] (f : A → B) (H' : is_equiv (trunc_functor 0 f))
+    (H : Πa k, is_equiv (π→*[k + 1] (pmap_of_map f a))) : is_equiv f :=
+  begin
+    revert A B HA HB f H' H, induction n with n IH: intros,
+    { apply is_equiv_of_is_contr},
+    have Πa, is_equiv (Ω→ (pmap_of_map f a)),
+    begin
+      intro a,
+      apply IH, do 2 (esimp; exact _),
+      { rexact H a 0},
+      intro p k,
+      have is_equiv (π→*[k + 1] (Ω→(pmap_of_map f a))),
+        from is_equiv_phomotopy_group_functor_ap1 (k+1) (pmap_of_map f a),
+      have Π(b : A) (p : a = b),
+        is_equiv (pmap.to_fun (π→*[k + 1] (pmap_of_map (ap f) p))),
+      begin
+        intro b p, induction p, apply is_equiv.homotopy_closed, exact this,
+        refine phomotopy_group_functor_phomotopy _ _,
+        apply ap1_pmap_of_map
+      end,
+      have is_equiv (phomotopy_group_pequiv _
+                      (pequiv_of_eq_pt (!idp_con⁻¹ : ap f p = Ω→ (pmap_of_map f a) p)) ∘
+           pmap.to_fun (π→*[k + 1] (pmap_of_map (ap f) p))),
+      begin
+        apply is_equiv_compose, exact this a p,
+      end,
+      apply is_equiv.homotopy_closed, exact this,
+      refine !phomotopy_group_functor_compose⁻¹* ⬝* _,
+      apply phomotopy_group_functor_phomotopy,
+      fapply phomotopy.mk,
+      { esimp, intro q, refine !idp_con⁻¹},
+      { esimp, refine !idp_con⁻¹},
+    end,
+    apply is_equiv_of_is_equiv_ap1_of_is_equiv_trunc
+  end

 end is_trunc
--- a/hott/homotopy/hopf.hlean
+++ b/hott/homotopy/hopf.hlean
@ -55,7 +55,7 @@ section
  variables [H : h_space A] [K : is_conn 0 A]
  include H K

-  definition hopf : susp A → Type :=
+  definition hopf [unfold 4] : susp A → Type :=
  susp.elim_type A A (λa, equiv.mk (λx, a * x) !is_equiv_mul_left)

  /- Lemma 8.5.7. The total space is A * A -/
@ -185,11 +185,11 @@ section
  equiv.MK encode decode' encode_decode' decode_encode

  definition main_lemma_point
-    : pointed.MK (trunc 1 (Ω(psusp A))) (tr idp) ≃* pointed.MK A 1 :=
+    : ptrunc 1 (Ω(psusp A)) ≃* pointed.MK A 1 :=
  pointed.pequiv_of_equiv main_lemma idp

-  protected definition delooping : (tr north = tr north :> trunc 2 (susp A)) ≃ A :=
-  (tr_eq_tr_equiv 1 north north) ⬝e main_lemma
+  protected definition delooping : Ω (ptrunc 2 (psusp A)) ≃* pointed.MK A 1 :=
+  loop_ptrunc_pequiv 1 (psusp A) ⬝e* main_lemma_point

 end

--- a/hott/homotopy/quaternionic_hopf.hlean
+++ b/hott/homotopy/quaternionic_hopf.hlean
@ -18,10 +18,10 @@ namespace hopf
  ⦃ involutive_neg, neg := empty.elim, neg_neg := by intro a; induction a ⦄

  definition involutive_neg_circle [instance] : involutive_neg circle :=
-  involutive_neg_susp
+  by change involutive_neg (susp (susp empty)); exact _

  definition has_star_circle [instance] : has_star circle :=
-  has_star_susp
+  by change has_star (susp (susp empty)); exact _

  -- this is the "natural" conjugation defined using the base-loop recursor
  definition circle_star [reducible] : S¹ → S¹ :=
@ -80,7 +80,7 @@ namespace hopf
    induction x,
    { apply inverse, exact circle_mul_base (y*) },
    { apply eq_pathover, induction y,
-      { exact natural_square_tr 
+      { exact natural_square_tr
          (λa : S¹, ap (λb : S¹, b*) (circle_mul_base a)) loop },
      { apply is_prop.elimo } }
  end
--- a/hott/homotopy/red_susp.hlean
+++ b/hott/homotopy/red_susp.hlean
@ -35,25 +35,23 @@ section
  definition merid_pt : merid pt = idp :=
  incl2 R Q Qmk

-  -- protected definition rec {P : red_susp → Type} (Pb : P base) (Pm : Π(a : A), Pb =[merid a] Pb)
-  --   (Pe : Pm pt =[merid_pt] idpo) (x : red_susp) : P x :=
-  -- begin
-  --   induction x,
-  -- end
+  protected definition rec {P : red_susp → Type} (Pb : P base) (Pm : Π(a : A), Pb =[merid a] Pb)
+    (Pe : change_path merid_pt (Pm pt) = idpo) (x : red_susp) : P x :=
+  begin
+    induction x,
+    { induction a, exact Pb},
+    { induction s, exact Pm a},
+    { induction q, esimp, exact Pe}
+  end

-  -- protected definition rec_on [reducible] {P : red_susp → Type} (x : red_susp) (Pb : P base)
-  --   (Pm : Π(a : A), Pb =[merid a] Pb) (Pe : Pm pt =[merid_pt] idpo) : P x :=
-  -- rec Pb Pm Pe x
+  protected definition rec_on [reducible] {P : red_susp → Type} (x : red_susp) (Pb : P base)
+    (Pm : Π(a : A), Pb =[merid a] Pb) (Pe : change_path merid_pt (Pm pt) = idpo) : P x :=
+  red_susp.rec Pb Pm Pe x

-  -- definition rec_merid {P : red_susp → Type} (Pb : P base) (Pm : Π(a : A), Pb =[merid a] Pb)
-  --   (Pe : Pm pt =[merid_pt] idpo) (a : A)
-  --   : apd (rec Pb Pm Pe) (merid a) = Pm a :=
-  -- !rec_incl1
-
-  -- theorem elim_merid_pt {P : red_susp → Type} (Pb : P base) (Pm : Π(a : A), Pb =[merid a] Pb)
-  --   (Pe : Pm pt =[merid_pt] idpo)
-  --   : square (ap02 (rec Pb Pm Pe) merid_pt) Pe (rec_merid Pe pt) idp :=
-  -- !rec_incl2
+  definition rec_merid {P : red_susp → Type} (Pb : P base) (Pm : Π(a : A), Pb =[merid a] Pb)
+    (Pe : change_path merid_pt (Pm pt) = idpo) (a : A)
+    : apd (rec Pb Pm Pe) (merid a) = Pm a :=
+  !rec_incl1

  protected definition elim {P : Type} (Pb : P) (Pm : Π(a : A), Pb = Pb)
    (Pe : Pm pt = idp) (x : red_susp) : P :=
@ -81,7 +79,7 @@ end
 end red_susp

 attribute red_susp.base [constructor]
-attribute /-red_susp.rec-/ red_susp.elim [unfold 6] [recursor 6]
+attribute red_susp.rec red_susp.elim [unfold 6] [recursor 6]
 --attribute red_susp.elim_type [unfold 9]
-attribute /-red_susp.rec_on-/ red_susp.elim_on [unfold 3]
+attribute red_susp.rec_on red_susp.elim_on [unfold 3]
 --attribute red_susp.elim_type_on [unfold 6]
--- a/hott/homotopy/sphere.hlean
+++ b/hott/homotopy/sphere.hlean
@ -75,15 +75,26 @@ namespace sphere_index
  definition has_le_sphere_index [instance] : has_le ℕ₋₁ :=
  has_le.mk sphere_index.le

-  definition of_nat [coercion] [reducible] (n : ℕ) : ℕ₋₁ :=
-  (nat.rec_on n -1 (λ n k, k.+1)).+1
-
  definition sub_one [reducible] (n : ℕ) : ℕ₋₁ :=
  nat.rec_on n -1 (λ n k, k.+1)

  postfix `..-1`:(max+1) := sub_one
+
+  definition of_nat [coercion] [reducible] (n : ℕ) : ℕ₋₁ :=
+  n..-1.+1
+
  -- we use a double dot to distinguish with the notation .-1 in trunc_index (of type ℕ → ℕ₋₂)

+  definition add_one [reducible] (n : ℕ₋₁) : ℕ :=
+  sphere_index.rec_on n 0 (λ n k, nat.succ k)
+
+  definition add_plus_one_of_nat (n m : ℕ) : (n +1+ m) = sphere_index.of_nat (n + m + 1) :=
+  begin
+    induction m with m IH,
+    { reflexivity },
+    { exact ap succ IH}
+  end
+
  definition succ_sub_one (n : ℕ) : (nat.succ n)..-1 = n :> ℕ₋₁ :=
  idp

@ -145,6 +156,29 @@ namespace sphere_index
  protected definition le_succ {n m : ℕ₋₁} (H1 : n ≤[ℕ₋₁] m): n ≤[ℕ₋₁] m.+1 :=
  le.step H1

+  definition add_plus_one_minus_one (n : ℕ₋₁) : n +1+ -1 = n := idp
+  definition add_plus_one_succ (n m : ℕ₋₁) : n +1+ (m.+1) = (n +1+ m).+1 := idp
+  definition minus_one_add_plus_one (n : ℕ₋₁) : -1 +1+ n = n :=
+  begin induction n with n IH, reflexivity, exact ap succ IH end
+  definition succ_add_plus_one (n m : ℕ₋₁) : (n.+1) +1+ m = (n +1+ m).+1 :=
+  begin induction m with m IH, reflexivity, exact ap succ IH end
+
+  definition sphere_index_of_nat_add_one (n : ℕ₋₁) : sphere_index.of_nat (add_one n) = n.+1 :=
+  begin induction n with n IH, reflexivity, exact ap succ IH end
+
+  definition add_one_succ (n : ℕ₋₁) : add_one (n.+1) = succ (add_one n) :=
+  by reflexivity
+
+  definition add_one_sub_one (n : ℕ) : add_one (n..-1) = n :=
+  begin induction n with n IH, reflexivity, exact ap nat.succ IH end
+
+  definition add_one_of_nat (n : ℕ) : add_one n = nat.succ n :=
+  ap nat.succ (add_one_sub_one n)
+
+  definition sphere_index.of_nat_succ (n : ℕ)
+    : sphere_index.of_nat (nat.succ n) = (sphere_index.of_nat n).+1 :=
+  begin induction n with n IH, reflexivity, exact ap succ IH end
+
  /-
    warning: if this coercion is available, the coercion ℕ → ℕ₋₂ is the composition of the coercions
    ℕ → ℕ₋₁ → ℕ₋₂. We don't want this composition as coercion, because it has worse computational
@ -152,7 +186,6 @@ namespace sphere_index
  -/
  attribute trunc_index.of_sphere_index [coercion]

-
 end sphere_index open sphere_index

 definition weak_order_sphere_index [trans_instance] [reducible] : weak_order sphere_index :=
@ -197,13 +230,18 @@ namespace trunc_index
    : trunc_index._trans_to_of_sphere_index n = of_nat n :> ℕ₋₂ :=
  of_sphere_index_of_nat n

+  definition trunc_index_of_nat_add_one (n : ℕ₋₁)
+    : trunc_index.of_nat (add_one n) = (of_sphere_index n).+1 :=
+  begin induction n with n IH, reflexivity, exact ap succ IH end
+
+  definition of_sphere_index_succ (n : ℕ₋₁) : of_sphere_index (n.+1) = (of_sphere_index n).+1 :=
+  begin induction n with n IH, reflexivity, exact ap succ IH end
+
 end trunc_index

 open sphere_index equiv

-definition sphere : ℕ₋₁ → Type₀
-| -1   := empty
-| n.+1 := susp (sphere n)
+definition sphere (n : ℕ₋₁) : Type₀ := iterate_susp (add_one n) empty

 namespace sphere

@ -214,6 +252,7 @@ namespace sphere
  pointed.mk base
  definition psphere [constructor] (n : ℕ) : Type* := pointed.mk' (sphere n)

+
  namespace ops
    abbreviation S := sphere
    notation `S.` := psphere
@ -221,13 +260,22 @@ namespace sphere
  open sphere.ops

  definition sphere_minus_one : S -1 = empty := idp
-  definition sphere_succ (n : ℕ₋₁) : S n.+1 = susp (S n) := idp
+  definition sphere_succ [unfold_full] (n : ℕ₋₁) : S n.+1 = susp (S n) := idp
+  definition psphere_succ [unfold_full] (n : ℕ) : S. (n + 1) = psusp (S. n) := idp
+  definition psphere_eq_iterate_susp (n : ℕ)
+    : S. n = pointed.MK (iterate_susp (succ n) empty) !north :=
+  begin
+    esimp,
+    apply ap (λx, pointed.MK (susp x) (@north x)); apply ap (λx, iterate_susp x empty),
+    apply add_one_sub_one
+  end
+

  definition equator (n : ℕ) : map₊ (S. n) (Ω (S. (succ n))) :=
  pmap.mk (λa, merid a ⬝ (merid base)⁻¹) !con.right_inv

  definition surf {n : ℕ} : Ω[n] S. n :=
-  nat.rec_on n (proof base qed)
+  nat.rec_on n (proof @base 0 qed)
               (begin intro m s, refine cast _ (apn m (equator m) s),
                      exact ap carrier !loop_space_succ_eq_in⁻¹ end)

--- a/hott/homotopy/sphere2.hlean
+++ b/hott/homotopy/sphere2.hlean
@ -0,0 +1,126 @@
+/-
+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
+
+Calculating homotopy groups of spheres.
+
+In this file we calculate
+π₂(S²) = Z
+πₙ(S²) = πₙ(S³) for n > 2
+πₙ(Sⁿ) = Z for n > 0
+π₂(S³) = Z
+-/
+
+import .homotopy_group .freudenthal
+open eq group algebra is_equiv equiv fin prod chain_complex pointed fiber nat is_trunc trunc_index
+     sphere.ops trunc is_conn susp
+
+namespace sphere
+  /- Corollaries of the complex hopf fibration combined with the LES of homotopy groups -/
+  open sphere sphere.ops int circle hopf
+
+  definition π2S2 : πg[1+1] (S. 2) ≃g gℤ :=
+  begin
+    refine _ ⬝g fundamental_group_of_circle,
+    refine _ ⬝g homotopy_group_isomorphism_of_pequiv _ pfiber_complex_phopf,
+    fapply isomorphism_of_equiv,
+    { fapply equiv.mk,
+      { exact cc_to_fn (LES_of_homotopy_groups complex_phopf) (1, 2)},
+      { refine @is_equiv_of_trivial _
+        _ _
+        (is_exact_LES_of_homotopy_groups _ (1, 1))
+        (is_exact_LES_of_homotopy_groups _ (1, 2))
+        _
+        _
+        (@pgroup_of_group _ (group_LES_of_homotopy_groups complex_phopf _ _) idp)
+        (@pgroup_of_group _ (group_LES_of_homotopy_groups complex_phopf _ _) idp)
+        _,
+        { rewrite [LES_of_homotopy_groups_1, ▸*],
+          have H : 1 ≤[ℕ] 2, from !one_le_succ,
+          apply trivial_homotopy_group_of_is_conn, exact H, rexact is_conn_psphere 3},
+        { refine tr_rev (λx, is_contr (ptrunctype._trans_of_to_pType x))
+                        (LES_of_homotopy_groups_1 complex_phopf 2) _,
+          apply trivial_homotopy_group_of_is_conn, apply le.refl, rexact is_conn_psphere 3},
+        { exact homomorphism.struct (homomorphism_LES_of_homotopy_groups_fun _ (0, 2))}}},
+    { exact homomorphism.struct (homomorphism_LES_of_homotopy_groups_fun _ (0, 2))}
+  end
+
+  open circle
+  definition πnS3_eq_πnS2 (n : ℕ) : πg[n+2 +1] (S. 3) ≃g πg[n+2 +1] (S. 2) :=
+  begin
+    fapply isomorphism_of_equiv,
+    { fapply equiv.mk,
+      { exact cc_to_fn (LES_of_homotopy_groups complex_phopf) (n+3, 0)},
+      { have H : is_trunc 1 (pfiber complex_phopf),
+        from @(is_trunc_equiv_closed_rev _ pfiber_complex_phopf) is_trunc_circle,
+        refine @is_equiv_of_trivial _
+        _ _
+        (is_exact_LES_of_homotopy_groups _ (n+2, 2))
+        (is_exact_LES_of_homotopy_groups _ (n+3, 0))
+        _
+        _
+        (@pgroup_of_group _ (group_LES_of_homotopy_groups complex_phopf _ _) idp)
+        (@pgroup_of_group _ (group_LES_of_homotopy_groups complex_phopf _ _) idp)
+        _,
+        { rewrite [▸*, LES_of_homotopy_groups_2 _ (n +[ℕ] 2)],
+          have H : 1 ≤[ℕ] n + 1, from !one_le_succ,
+          apply trivial_homotopy_group_of_is_trunc _ _ _ H},
+        { refine tr_rev (λx, is_contr (ptrunctype._trans_of_to_pType x))
+                        (LES_of_homotopy_groups_2 complex_phopf _) _,
+          have H : 1 ≤[ℕ] n + 2, from !one_le_succ,
+          apply trivial_homotopy_group_of_is_trunc _ _ _ H},
+        { exact homomorphism.struct (homomorphism_LES_of_homotopy_groups_fun _ (n+2, 0))}}},
+    { exact homomorphism.struct (homomorphism_LES_of_homotopy_groups_fun _ (n+2, 0))}
+  end
+
+  definition sphere_stability_pequiv (k n : ℕ) (H : k + 2 ≤ 2 * n) :
+    π*[k + 1] (S. (n+1)) ≃* π*[k] (S. n) :=
+  begin rewrite [+ psphere_eq_iterate_susp], exact iterate_susp_stability_pequiv empty H end
+
+  definition stability_isomorphism (k n : ℕ) (H : k + 3 ≤ 2 * n)
+    : πg[k+1 +1] (S. (n+1)) ≃g πg[k+1] (S. n) :=
+  begin rewrite [+ psphere_eq_iterate_susp], exact iterate_susp_stability_isomorphism empty H end
+
+  open int circle hopf
+  definition πnSn (n : ℕ) : πg[n+1] (S. (succ n)) ≃g gℤ :=
+  begin
+    cases n with n IH,
+    { exact fundamental_group_of_circle},
+    { induction n with n IH,
+      { exact π2S2},
+      { refine _ ⬝g IH, apply stability_isomorphism,
+        rexact add_mul_le_mul_add n 1 2}}
+  end
+
+  theorem not_is_trunc_sphere (n : ℕ) : ¬is_trunc n (S. (succ n)) :=
+  begin
+    intro H,
+    note H2 := trivial_homotopy_group_of_is_trunc (S. (succ n)) n n !le.refl,
+    have H3 : is_contr ℤ, from is_trunc_equiv_closed _ (equiv_of_isomorphism (πnSn n)),
+    have H4 : (0 : ℤ) ≠ (1 : ℤ), from dec_star,
+    apply H4,
+    apply is_prop.elim,
+  end
+
+  section
+    open sphere_index
+
+    definition not_is_trunc_sphere' (n : ℕ₋₁) : ¬is_trunc n (S (n.+1)) :=
+    begin
+      cases n with n,
+      { esimp [sphere.ops.S, sphere], intro H,
+        have H2 : is_prop bool, from @(is_trunc_equiv_closed -1 sphere_equiv_bool) H,
+        have H3 : bool.tt ≠ bool.ff, from dec_star, apply H3, apply is_prop.elim},
+      { intro H, apply not_is_trunc_sphere (add_one n),
+        rewrite [▸*, trunc_index_of_nat_add_one, -add_one_succ,
+                 sphere_index_of_nat_add_one],
+        exact H}
+    end
+
+  end
+
+  definition π3S2 : πg[2+1] (S. 2) ≃g gℤ :=
+  (πnS3_eq_πnS2 0)⁻¹ᵍ ⬝g πnSn 2
+
+end sphere
--- a/hott/homotopy/susp.hlean
+++ b/hott/homotopy/susp.hlean
@ -354,4 +354,29 @@ namespace susp
    apply psusp_functor_compose
  end

+  definition iterate_susp (n : ℕ) (A : Type) : Type := iterate susp n A
+  definition iterate_psusp (n : ℕ) (A : Type*) : Type* := iterate (λX, psusp X) n A
+
+  open is_conn trunc_index nat
+  definition iterate_susp_succ (n : ℕ) (A : Type) :
+    iterate_susp (succ n) A = susp (iterate_susp n A) :=
+  idp
+
+  definition is_conn_iterate_susp [instance] (n : ℕ₋₂) (m : ℕ) (A : Type)
+    [H : is_conn n A] : is_conn (n + m) (iterate_susp m A) :=
+  begin induction m with m IH, exact H, exact @is_conn_susp _ _ IH end
+
+  definition is_conn_iterate_psusp [instance] (n : ℕ₋₂) (m : ℕ) (A : Type*)
+    [H : is_conn n A] : is_conn (n + m) (iterate_psusp m A) :=
+  begin induction m with m IH, exact H, exact @is_conn_susp _ _ IH end
+
+  -- Separate cases for n = 0, which comes up often
+  definition is_conn_iterate_susp_zero [instance] (m : ℕ) (A : Type)
+    [H : is_conn 0 A] : is_conn m (iterate_susp m A) :=
+  begin induction m with m IH, exact H, exact @is_conn_susp _ _ IH end
+
+  definition is_conn_iterate_psusp_zero [instance] (m : ℕ) (A : Type*)
+    [H : is_conn 0 A] : is_conn m (iterate_psusp m A) :=
+  begin induction m with m IH, exact H, exact @is_conn_susp _ _ IH end
+
 end susp
--- a/hott/homotopy/wedge.hlean
+++ b/hott/homotopy/wedge.hlean
@ -5,7 +5,7 @@ Authors: Jakob von Raumer, Ulrik Buchholtz

 The Wedge Sum of Two pType Types
 -/
-import hit.pointed_pushout .connectedness
+import hit.pointed_pushout .connectedness types.unit

 open eq pushout pointed unit trunc_index

--- a/hott/init/equiv.hlean
+++ b/hott/init/equiv.hlean
@ -131,6 +131,7 @@ namespace is_equiv
  definition is_equiv_inv [instance] [constructor] : is_equiv f⁻¹ :=
  adjointify f⁻¹ f (left_inv f) (right_inv f)

+  -- The 2-out-of-3 properties
  definition cancel_right (g : B → C) [Hgf : is_equiv (g ∘ f)] : (is_equiv g) :=
  have Hfinv : is_equiv f⁻¹, from is_equiv_inv f,
  @homotopy_closed _ _ _ _ (is_equiv_compose f⁻¹ (g ∘ f)) (λb, ap g (@right_inv _ _ f _ b))
@ -142,28 +143,24 @@ namespace is_equiv
  definition eq_of_fn_eq_fn' {x y : A} (q : f x = f y) : x = y :=
  (left_inv f x)⁻¹ ⬝ ap f⁻¹ q ⬝ left_inv f y

-  theorem ap_eq_of_fn_eq_fn' {x y : A} (q : f x = f y) : ap f (eq_of_fn_eq_fn' f q) = q :=
-  begin
-    rewrite [↑eq_of_fn_eq_fn',+ap_con,ap_inv,-+adj,-ap_compose,con.assoc,
-             ap_con_eq_con_ap (right_inv f) q,inv_con_cancel_left,ap_id],
-  end
+  definition ap_eq_of_fn_eq_fn' {x y : A} (q : f x = f y) : ap f (eq_of_fn_eq_fn' f q) = q :=
+  !ap_con ⬝ whisker_right !ap_con _
+          ⬝ ((!ap_inv ⬝ inverse2 (adj f _)⁻¹)
+            ◾ (inverse (ap_compose f f⁻¹ _))
+            ◾ (adj f _)⁻¹)
+          ⬝ con_ap_con_eq_con_con (right_inv f) _ _
+          ⬝ whisker_right !con.left_inv _
+          ⬝ !idp_con
+
+  definition eq_of_fn_eq_fn'_ap {x y : A} (q : x = y) : eq_of_fn_eq_fn' f (ap f q) = q :=
+  by induction q; apply con.left_inv

  definition is_equiv_ap [instance] [constructor] (x y : A) : is_equiv (ap f : x = y → f x = f y) :=
  adjointify
    (ap f)
    (eq_of_fn_eq_fn' f)
-    abstract (λq, !ap_con
-      ⬝ whisker_right !ap_con _
-      ⬝ ((!ap_inv ⬝ inverse2 (adj f _)⁻¹)
-        ◾ (inverse (ap_compose f f⁻¹ _))
-        ◾ (adj f _)⁻¹)
-      ⬝ con_ap_con_eq_con_con (right_inv f) _ _
-      ⬝ whisker_right !con.left_inv _
-      ⬝ !idp_con) end
-    abstract (λp, whisker_right (whisker_left _ (ap_compose f⁻¹ f _)⁻¹) _
-      ⬝ con_ap_con_eq_con_con (left_inv f) _ _
-      ⬝ whisker_right !con.left_inv _
-      ⬝ !idp_con) end
+    (ap_eq_of_fn_eq_fn' f)
+    (eq_of_fn_eq_fn'_ap f)

  -- The function equiv_rect says that given an equivalence f : A → B,
  -- and a hypothesis from B, one may always assume that the hypothesis
--- a/hott/init/path.hlean
+++ b/hott/init/path.hlean
@ -62,6 +62,11 @@ namespace eq
    (p ⬝ q) ⬝ r = p ⬝ (q ⬝ r) :=
  by induction r; reflexivity

+  definition con.assoc5 {a₁ a₂ a₃ a₄ a₅ a₆ : A}
+    (p₁ : a₁ = a₂) (p₂ : a₂ = a₃) (p₃ : a₃ = a₄) (p₄ : a₄ = a₅) (p₅ : a₅ = a₆) :
+    p₁ ⬝ (p₂ ⬝ p₃ ⬝ p₄) ⬝ p₅ = (p₁ ⬝ p₂) ⬝ p₃ ⬝ (p₄ ⬝ p₅) :=
+  by induction p₅; induction p₄; induction p₃; reflexivity
+
  -- The left inverse law.
  definition con.right_inv [unfold 4] (p : x = y) : p ⬝ p⁻¹ = idp :=
  by induction p; reflexivity
@ -486,6 +491,11 @@ namespace eq
  -- using the following notation
  notation p ` ▸D `:65 x:64 := transportD _ p _ x

+  -- transporting over 2 one-dimensional paths
+  definition transport11 {A B : Type} (P : A → B → Type) {a a' : A} {b b' : B}
+    (p : a = a') (q : b = b') (z : P a b) : P a' b' :=
+  transport (P a') q (p ▸ z)
+
  -- Transporting along higher-dimensional paths
  definition transport2 [unfold 7] (P : A → Type) {x y : A} {p q : x = y} (r : p = q) (z : P x) :
    p ▸ z = q ▸ z :=
@ -734,3 +744,14 @@ namespace eq
  by induction r2; induction r1; induction p1; reflexivity

 end eq
+
+/-
+  an auxillary namespace for concatenation and inversion for homotopies. We put this is a separate
+  namespace because ⁻¹ʰ is also used as the inverse of a homomorphism
+-/
+
+open eq
+namespace homotopy
+  infix ` ⬝h `:75 := homotopy.trans
+  postfix `⁻¹ʰ`:(max+1) := homotopy.symm
+end homotopy
--- a/hott/init/pointed.hlean
+++ b/hott/init/pointed.hlean
@ -75,6 +75,11 @@ namespace pointed

  attribute ptrunctype._trans_of_to_pType ptrunctype.to_pType ptrunctype.to_trunctype [unfold 2]

+  -- Any contractible type is pointed
+  definition pointed_of_is_contr [instance] [priority 800] [constructor]
+    (A : Type) [H : is_contr A] : pointed A :=
+  pointed.mk !center
+
 end pointed

 /- pointed maps -/
@ -111,5 +116,4 @@ namespace pointed
  infix ` ≃* `:25 := pequiv
  attribute pequiv.to_pmap [coercion]
  attribute pequiv.to_is_equiv [instance]
-
 end pointed
--- a/hott/init/trunc.hlean
+++ b/hott/init/trunc.hlean
@ -302,6 +302,10 @@ namespace is_trunc
    (f : A → B) (g : B → A) : is_equiv f :=
  is_equiv.mk f g (λb, !is_prop.elim) (λa, !is_prop.elim) (λa, !is_set.elim)

+  definition is_equiv_of_is_contr [constructor] [HA : is_contr A] [HB : is_contr B]
+    (f : A → B) : is_equiv f :=
+  is_equiv.mk f (λx, !center) (λb, !is_prop.elim) (λa, !is_prop.elim) (λa, !is_set.elim)
+
  definition equiv_of_is_prop [constructor] [HA : is_prop A] [HB : is_prop B]
    (f : A → B) (g : B → A) : A ≃ B :=
  equiv.mk f (is_equiv_of_is_prop f g)
--- a/hott/init/ua.hlean
+++ b/hott/init/ua.hlean
@ -15,11 +15,11 @@ section
  universe variable l
  variables {A B : Type.{l}}

-  definition is_equiv_cast_of_eq [constructor] (H : A = B) : is_equiv (cast H) :=
+  definition is_equiv_cast [constructor] (H : A = B) : is_equiv (cast H) :=
  is_equiv_tr (λX, X) H

  definition equiv_of_eq [constructor] (H : A = B) : A ≃ B :=
-  equiv.mk _ (is_equiv_cast_of_eq H)
+  equiv.mk _ (is_equiv_cast H)

  definition equiv_of_eq_refl [reducible] [unfold_full] (A : Type)
    : equiv_of_eq (refl A) = equiv.refl A :=
--- a/hott/types/bool.hlean
+++ b/hott/types/bool.hlean
@ -168,6 +168,17 @@ namespace bool
    { intro b, cases b, reflexivity, reflexivity},
  end

+  /- pointed and truncated bool -/
+  open pointed
+  definition pointed_bool [instance] [constructor] : pointed bool :=
+  pointed.mk ff
+
+  definition pbool [constructor] : Set* :=
+  pSet.mk' bool
+
  definition tbool [constructor] : Set := trunctype.mk bool _

+  notation `bool*` := pbool
+
+
 end bool
--- a/hott/types/fiber.hlean
+++ b/hott/types/fiber.hlean
@ -79,15 +79,16 @@ namespace fiber
  definition pointed_fiber [constructor] (f : A → B) (a : A) : Type* :=
  pointed.Mk (fiber.mk a (idpath (f a)))

-  definition is_trunc_fun [reducible] (n : trunc_index) (f : A → B) :=
+  definition is_trunc_fun [reducible] (n : ℕ₋₂) (f : A → B) :=
  Π(b : B), is_trunc n (fiber f b)

  definition is_contr_fun [reducible] (f : A → B) := is_trunc_fun -2 f

  -- pre and post composition with equivalences
  open function
-  protected definition equiv_postcompose [constructor] {B' : Type} (g : B → B') [H : is_equiv g]
-    : fiber (g ∘ f) (g b) ≃ fiber f b :=
+  variable (f)
+  protected definition equiv_postcompose [constructor] {B' : Type} (g : B ≃ B') --[H : is_equiv g]
+    (b : B) : fiber (g ∘ f) (g b) ≃ fiber f b :=
  calc
    fiber (g ∘ f) (g b) ≃ Σa : A, g (f a) = g b : fiber.sigma_char
                    ... ≃ Σa : A, f a = b       : begin
@ -96,12 +97,12 @@ namespace fiber
                                                  end
                    ... ≃ fiber f b             : fiber.sigma_char

-  protected definition equiv_precompose [constructor] {A' : Type} (g : A' → A) [H : is_equiv g]
-    : fiber (f ∘ g) b ≃ fiber f b :=
+  protected definition equiv_precompose [constructor] {A' : Type} (g : A' ≃ A) --[H : is_equiv g]
+    (b : B) : fiber (f ∘ g) b ≃ fiber f b :=
  calc
    fiber (f ∘ g) b ≃ Σa' : A', f (g a') = b   : fiber.sigma_char
                ... ≃ Σa : A, f a = b          : begin
-                                                   apply sigma_equiv_sigma (equiv.mk g H),
+                                                   apply sigma_equiv_sigma g,
                                                   intro a', apply erfl
                                                 end
                ... ≃ fiber f b                : fiber.sigma_char
--- a/hott/types/fin.hlean
+++ b/hott/types/fin.hlean
@ -1,7 +1,7 @@
 /-
 Copyright (c) 2015 Haitao Zhang. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Haitao Zhang, Leonardo de Moura, Jakob von Raumer
+Authors: Haitao Zhang, Leonardo de Moura, Jakob von Raumer, Floris van Doorn

 Finite ordinal types.
 -/
@ -577,4 +577,54 @@ begin
    have fin m ≃ fin n, from unit_sum_equiv_cancel this,
    apply ap nat.succ, apply IH _ this },
 end
+
+  definition cyclic_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
+
+  /-
+    We want to say that fin (succ n) always has a 0 and 1. However, we want a bit more, because
+    sometimes we want a zero of (fin a) where a is either
+    - equal to a successor, but not definitionally a successor (e.g. (0 : fin (3 + n)))
+    - definitionally equal to a successor, but not in a way that type class inference can infer.
+      (e.g. (0 : fin 4). Note that 4 is bit0 (bit0 one), but (bit0 x) (defined as x + x),
+        is not always a successor)
+    To solve this we use an auxillary class `is_succ` which can solve whether a number is a
+    successor.
+  -/
+
+  inductive is_succ [class] : ℕ → Type :=
+  | mk : Π(n : ℕ), is_succ (nat.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 [instance] (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
+
+  /- this is a version of `madd` which might compute better -/
+  protected definition add {n : ℕ} (x y : fin n) : fin n :=
+  iterate cyclic_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 (cyclic_succ (fin.zero n))
+
+  definition has_add_fin [instance] (n : ℕ) : has_add (fin n) :=
+  has_add.mk fin.add
+
 end fin
--- a/hott/types/lift.hlean
+++ b/hott/types/lift.hlean
@ -146,5 +146,33 @@ namespace lift

  -- is_trunc_lift is defined in init.trunc

+  definition pup [constructor] {A : Type*} : A →* plift A :=
+  pmap.mk up idp
+
+  definition pdown [constructor] {A : Type*} : plift A →* A :=
+  pmap.mk down idp
+
+  definition plift_functor_phomotopy [constructor] {A B : Type*} (f : A →* B)
+    : pdown ∘* plift_functor f ∘* pup ~* f :=
+  begin
+    fapply phomotopy.mk,
+    { reflexivity},
+    { esimp, refine !idp_con ⬝ _, refine _ ⬝ ap02 down !idp_con⁻¹,
+      refine _ ⬝ !ap_compose, exact !ap_id⁻¹}
+  end
+
+  definition pequiv_plift [constructor] (A : Type*) : A ≃* plift A :=
+  pequiv_of_equiv (equiv_lift A) idp
+
+  definition fiber_lift_functor {A B : Type} (f : A → B) (b : B) :
+    fiber (lift_functor f) (up b) ≃ fiber f b :=
+  begin
+    fapply equiv.MK: intro v; cases v with a p,
+    { cases a with a, exact fiber.mk a (eq_of_fn_eq_fn' up p)},
+    { exact fiber.mk (up a) (ap up p)},
+    { esimp, apply ap (fiber.mk a), apply eq_of_fn_eq_fn'_ap},
+    { cases a with a, esimp, apply ap (fiber.mk (up a)), apply ap_eq_of_fn_eq_fn'}
+  end
+

 end lift
--- a/hott/types/nat/hott.hlean
+++ b/hott/types/nat/hott.hlean
@ -119,4 +119,29 @@ namespace nat
  definition pointed_nat [instance] [constructor] : pointed ℕ :=
  pointed.mk 0

+  open sigma sum
+  definition eq_even_or_eq_odd (n : ℕ) : (Σk, 2 * k = n) ⊎ (Σk, 2 * k + 1 = n) :=
+  begin
+    induction n with n IH,
+    { exact inl ⟨0, idp⟩},
+    { induction IH with H H: induction H with k p: induction p,
+      { exact inr ⟨k, idp⟩},
+      { refine inl ⟨k+1, idp⟩}}
+  end
+
+  definition rec_on_even_odd {P : ℕ → Type} (n : ℕ) (H : Πk, P (2 * k)) (H2 : Πk, P (2 * k + 1))
+    : P n :=
+  begin
+    cases eq_even_or_eq_odd n with v v: induction v with k p: induction p,
+    { exact H k},
+    { exact H2 k}
+  end
+
+  /- this inequality comes up a couple of times when using the freudenthal suspension theorem -/
+  definition add_mul_le_mul_add (n m k : ℕ) : n + (succ m) * k ≤ (succ m) * (n + k) :=
+  calc
+    n + (succ m) * k ≤ (m * n + n) + (succ m) * k : add_le_add_right !le_add_left _
+      ... = (succ m) * n + (succ m) * k : by rewrite -succ_mul
+      ... = (succ m) * (n + k) : !left_distrib⁻¹
+
 end nat
--- a/hott/types/nat/order.hlean
+++ b/hott/types/nat/order.hlean
@ -228,6 +228,12 @@ lt.base n
 lemma lt_succ_of_lt {i j : nat} : i < j → i < succ j :=
 assume Plt, lt.trans Plt (self_lt_succ j)

+lemma one_le_succ (n : ℕ) : 1 ≤ succ n :=
+nat.succ_le_succ !zero_le
+
+lemma two_le_succ_succ (n : ℕ) : 2 ≤ succ (succ n) :=
+nat.succ_le_succ !one_le_succ
+
 /- other forms of induction -/

 protected definition strong_rec_on {P : nat → Type} (n : ℕ) (H : Πn, (Πm, m < n → P m) → P n) : P n :=
--- a/hott/types/pi.hlean
+++ b/hott/types/pi.hlean
@ -341,3 +341,22 @@ namespace pi
 end pi

 attribute pi.is_trunc_pi [instance] [priority 1520]
+
+namespace pi
+
+  /- pointed pi types -/
+  open pointed
+
+  definition pointed_pi [instance] [constructor] {A : Type} (P : A → Type) [H : Πx, pointed (P x)]
+      : pointed (Πx, P x) :=
+  pointed.mk (λx, pt)
+
+  definition ppi [constructor] {A : Type} (P : A → Type*) : Type* :=
+  pointed.mk' (Πa, P a)
+
+  notation `Π*` binders `, ` r:(scoped P, ppi P) := r
+
+  definition ptpi [constructor] {n : ℕ₋₂} {A : Type} (P : A → n-Type*) : n-Type* :=
+  ptrunctype.mk' n (Πa, P a)
+
+end pi
--- a/hott/types/pointed.hlean
+++ b/hott/types/pointed.hlean
@ -13,48 +13,9 @@ open is_trunc eq prod sigma nat equiv option is_equiv bool unit algebra sigma.op
 namespace pointed
  variables {A B : Type}

-  -- Any contractible type is pointed
-  definition pointed_of_is_contr [instance] [priority 800] [constructor]
-    (A : Type) [H : is_contr A] : pointed A :=
-  pointed.mk !center
-
-  -- A pi type with a pointed target is pointed
-  definition pointed_pi [instance] [constructor] (P : A → Type) [H : Πx, pointed (P x)]
-      : pointed (Πx, P x) :=
-  pointed.mk (λx, pt)
-
-  -- A sigma type of pointed components is pointed
-  definition pointed_sigma [instance] [constructor] (P : A → Type) [G : pointed A]
-      [H : pointed (P pt)] : pointed (Σx, P x) :=
-  pointed.mk ⟨pt,pt⟩
-
-  definition pointed_prod [instance] [constructor] (A B : Type) [H1 : pointed A] [H2 : pointed B]
-      : pointed (A × B) :=
-  pointed.mk (pt,pt)
-
  definition pointed_loop [instance] [constructor] (a : A) : pointed (a = a) :=
  pointed.mk idp

-  definition pointed_bool [instance] [constructor] : pointed bool :=
-  pointed.mk ff
-
-  definition pprod [constructor] (A B : Type*) : Type* :=
-  pointed.mk' (A × B)
-
-  definition psum [constructor] (A B : Type*) : Type* :=
-  pointed.MK (A ⊎ B) (inl pt)
-
-  definition ppi [constructor] {A : Type} (P : A → Type*) : Type* :=
-  pointed.mk' (Πa, P a)
-
-  definition psigma [constructor] {A : Type*} (P : A → Type*) : Type* :=
-  pointed.mk' (Σa, P a)
-
-  infixr ` ×* `:35 := pprod
-  infixr ` +* `:30 := psum
-  notation `Σ*` binders `, ` r:(scoped P, psigma P) := r
-  notation `Π*` binders `, ` r:(scoped P, ppi P) := r
-
  definition pointed_fun_closed [constructor] (f : A → B) [H : pointed A] : pointed B :=
  pointed.mk (f pt)

@ -65,9 +26,13 @@ namespace pointed
  | iterated_ploop_space  0    X := X
  | iterated_ploop_space (n+1) X := ploop_space (iterated_ploop_space n X)

-  prefix `Ω`:(max+5) := ploop_space
+  notation `Ω` := ploop_space
  notation `Ω[`:95 n:0 `] `:0 A:95 := iterated_ploop_space n A

+  definition is_trunc_loop [instance] [priority 1100] (A : Type*)
+    (n : ℕ₋₂) [H : is_trunc (n.+1) A] : is_trunc n (Ω A) :=
+  !is_trunc_eq
+
  definition iterated_ploop_space_zero [unfold_full] (A : Type*)
    : Ω[0] A = A := rfl

@ -129,27 +94,9 @@ namespace pointed
    exact ptrunctype_eq q r
  end

-  definition pbool [constructor] : Set* :=
-  pSet.mk' bool
-
-  definition punit [constructor] : Set* :=
-  pSet.mk' unit
-
-  notation `bool*` := pbool
-  notation `unit*` := punit
-
  definition is_trunc_ptrunctype [instance] {n : ℕ₋₂} (A : n-Type*) : is_trunc n A :=
  trunctype.struct A

-  definition ptprod [constructor] {n : ℕ₋₂} (A B : n-Type*) : n-Type* :=
-  ptrunctype.mk' n (A × B)
-
-  definition ptpi [constructor] {n : ℕ₋₂} {A : Type} (P : A → n-Type*) : n-Type* :=
-  ptrunctype.mk' n (Πa, P a)
-
-  definition ptsigma [constructor] {n : ℕ₋₂} {A : n-Type*} (P : A → n-Type*) : n-Type* :=
-  ptrunctype.mk' n (Σa, P a)
-
  /- properties of iterated loop space -/
  variable (A : Type*)
  definition loop_space_succ_eq_in (n : ℕ) : Ω[succ n] A = Ω[n] (Ω A) :=
@ -206,6 +153,10 @@ namespace pointed

  /- categorical properties of pointed maps -/

+  definition pmap_of_map [constructor] {A B : Type} (f : A → B) (a : A) :
+    pointed.MK A a →* pointed.MK B (f a) :=
+  pmap.mk f idp
+
  definition pid [constructor] [refl] (A : Type*) : A →* A :=
  pmap.mk id idp

@ -297,6 +248,12 @@ namespace pointed

  /- instances of pointed maps -/

+  definition pcast [constructor] {A B : Type*} (p : A = B) : A →* B :=
+  pmap.mk (cast (ap pType.carrier p)) (by induction p; reflexivity)
+
+  definition pinverse [constructor] {X : Type*} : Ω X →* Ω X :=
+  pmap.mk eq.inverse idp
+
  definition ap1 [constructor] (f : A →* B) : Ω A →* Ω B :=
  begin
    fconstructor,
@ -304,7 +261,7 @@ namespace pointed
    { esimp, apply con.left_inv}
  end

-  definition apn (n : ℕ) (f : map₊ A B) : Ω[n] A →* Ω[n] B :=
+  definition apn (n : ℕ) (f : A →* B) : Ω[n] A →* Ω[n] B :=
  begin
  induction n with n IH,
  { exact f},
@ -314,15 +271,6 @@ namespace pointed
  prefix `Ω→`:(max+5) := ap1
  notation `Ω→[`:95 n:0 `] `:0 f:95 := apn n f

-  definition apn_zero [unfold_full] (f : map₊ A B) : Ω→[0] f = f := idp
-  definition apn_succ [unfold_full] (n : ℕ) (f : map₊ A B) : Ω→[n + 1] f = ap1 (Ω→[n] f) := idp
-
-  definition pcast [constructor] {A B : Type*} (p : A = B) : A →* B :=
-  pmap.mk (cast (ap pType.carrier p)) (by induction p; reflexivity)
-
-  definition pinverse [constructor] {X : Type*} : Ω X →* Ω X :=
-  pmap.mk eq.inverse idp
-
  /- categorical properties of pointed homotopies -/

  protected definition phomotopy.refl [constructor] [refl] (f : A →* B) : f ~* f :=
@ -332,7 +280,7 @@ namespace pointed
    { apply idp_con}
  end

-  protected definition phomotopy.rfl [constructor] {A B : Type*} {f : A →* B} : f ~* f :=
+  protected definition phomotopy.rfl [constructor] {f : A →* B} : f ~* f :=
  phomotopy.refl f

  protected definition phomotopy.trans [constructor] [trans] (p : f ~* g) (q : g ~* h)
@ -355,14 +303,14 @@ namespace pointed

  /- properties about the given pointed maps -/

-  definition is_equiv_ap1 {A B : Type*} (f : A →* B) [is_equiv f] : is_equiv (ap1 f) :=
+  definition is_equiv_ap1 (f : A →* B) [is_equiv f] : is_equiv (ap1 f) :=
  begin
    induction B with B b, induction f with f pf, esimp at *, cases pf, esimp,
    apply is_equiv.homotopy_closed (ap f),
    intro p, exact !idp_con⁻¹
  end

-  definition is_equiv_apn {A B : Type*} (n : ℕ) (f : A →* B) [H : is_equiv f]
+  definition is_equiv_apn (n : ℕ) (f : A →* B) [H : is_equiv f]
    : is_equiv (apn n f) :=
  begin
    induction n with n IH,
@ -370,6 +318,9 @@ namespace pointed
    { exact is_equiv_ap1 (apn n f)}
  end

+  definition is_equiv_pcast [instance] {A B : Type*} (p : A = B) : is_equiv (pcast p) :=
+  !is_equiv_cast
+
  definition ap1_id [constructor] {A : Type*} : ap1 (pid A) ~* pid (Ω A) :=
  begin
    fapply phomotopy.mk,
@ -426,6 +377,12 @@ namespace pointed
    : pinverse p⁻¹ = (pinverse p)⁻¹ :=
  idp

+  definition pcast_idp [constructor] {A : Type*} : pcast (idpath A) ~* pid A :=
+  by reflexivity
+
+  definition apn_zero [unfold_full] (f : A →* B) : Ω→[0] f = f := idp
+  definition apn_succ [unfold_full] (n : ℕ) (f : A →* B) : Ω→[n + 1] f = Ω→ (Ω→[n] f) := idp
+
  /- more on pointed homotopies -/

  definition phomotopy_of_eq [constructor] {A B : Type*} {f g : A →* B} (p : f = g) : f ~* g :=
@ -474,11 +431,10 @@ namespace pointed
    In general we need function extensionality for pap,
    but for particular F we can do it without function extensionality.
  -/
-  definition pap {A B C D : Type*} (F : (A →* B) → (C →* D))
-    {f g : A →* B} (p : f ~* g) : F f ~* F g :=
+  definition pap (F : (A →* B) → (C →* D)) {f g : A →* B} (p : f ~* g) : F f ~* F g :=
  phomotopy.mk (ap010 F (eq_of_phomotopy p)) begin cases eq_of_phomotopy p, apply idp_con end

-  definition ap1_phomotopy {A B : Type*} {f g : A →* B} (p : f ~* g)
+  definition ap1_phomotopy {f g : A →* B} (p : f ~* g)
    : ap1 f ~* ap1 g :=
  begin
    induction p with p q, induction f with f pf, induction g with g pg, induction B with B b,
@ -490,6 +446,13 @@ namespace pointed
      induction q, reflexivity}
  end

+  definition apn_phomotopy {f g : A →* B} (n : ℕ) (p : f ~* g) : apn n f ~* apn n g :=
+  begin
+    induction n with n IH,
+    { exact p},
+    { exact ap1_phomotopy IH}
+  end
+
  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,
@ -518,6 +481,38 @@ namespace pointed
    { reflexivity}
  end

+  definition pcast_loop_space [constructor] {A B : Type*} (p : A = B) :
+    pcast (ap Ω p) ~* ap1 (pcast p) :=
+  begin
+    fapply phomotopy.mk,
+    { intro a, induction p, esimp, exact (!idp_con ⬝ !ap_id)⁻¹},
+    { induction p, reflexivity}
+  end
+
+  definition apn_succ_phomotopy_in (n : ℕ) (f : A →* B) :
+    pcast (loop_space_succ_eq_in B n) ∘* Ω→[n + 1] f ~*
+    Ω→[n] (Ω→ f) ∘* pcast (loop_space_succ_eq_in A n) :=
+  begin
+    induction n with n IH,
+    { reflexivity},
+    { refine pwhisker_right _ (pcast_loop_space (loop_space_succ_eq_in B n)) ⬝* _,
+      refine _ ⬝* pwhisker_left _ (pcast_loop_space (loop_space_succ_eq_in A n))⁻¹*,
+      refine (ap1_compose _ (Ω→[n + 1] f))⁻¹* ⬝* _ ⬝* ap1_compose (Ω→[n] (Ω→ f)) _,
+      exact ap1_phomotopy IH}
+  end
+
+  definition ap1_pmap_of_map [constructor] {A B : Type} (f : A → B) (a : A) :
+    ap1 (pmap_of_map f a) ~* pmap_of_map (ap f) (idpath a) :=
+  begin
+    fapply phomotopy.mk,
+    { intro a, esimp, apply idp_con},
+    { reflexivity}
+  end
+
+  definition pmap_of_eq_pt [constructor] {A : Type} {a a' : A} (p : a = a') :
+    pointed.MK A a →* pointed.MK A a' :=
+  pmap.mk id p
+
  /- pointed equivalences -/

  definition pequiv_of_pmap [constructor] (f : A →* B) (H : is_equiv f) : A ≃* B :=
@ -750,6 +745,10 @@ namespace pointed
    loopn_pequiv_loopn (n+1) f p ⬝ loopn_pequiv_loopn (n+1) f q :=
  ap1_con (loopn_pequiv_loopn n f) p q

+  definition loop_pequiv_loop_con {A B : Type*} (f : A ≃* B) (p q : Ω A)
+    : loop_pequiv_loop f (p ⬝ q) = loop_pequiv_loop f p ⬝ loop_pequiv_loop f q :=
+  loopn_pequiv_loopn_con 0 f p q
+
  definition loopn_pequiv_loopn_rfl (n : ℕ) (A : Type*) :
    loopn_pequiv_loopn n (pequiv.refl A) = pequiv.refl (Ω[n] A) :=
  begin
@ -773,6 +772,10 @@ namespace pointed
  definition pequiv_pinverse (A : Type*) : Ω A ≃* Ω A :=
  pequiv_of_pmap pinverse !is_equiv_eq_inverse

+  definition pequiv_of_eq_pt [constructor] {A : Type} {a a' : A} (p : a = a') :
+    pointed.MK A a ≃* pointed.MK A a' :=
+  pequiv_of_pmap (pmap_of_eq_pt p) !is_equiv_id
+
 /- -- TODO
  definition pmap_pequiv_pmap {A A' B B' : Type*} (f : A ≃* A') (g : B ≃* B') :
    ppmap A B ≃* ppmap A' B' :=
--- a/hott/types/prod.hlean
+++ b/hott/types/prod.hlean
@ -249,7 +249,33 @@ namespace prod
 end prod

 attribute prod.is_trunc_prod [instance] [priority 1510]
-definition tprod [constructor] {n : trunc_index} (A B : n-Type) : n-Type :=
-trunctype.mk (A × B) _

-infixr `×t`:30 := tprod
+namespace prod
+  /- pointed products -/
+  open pointed
+  definition pointed_prod [instance] [constructor] (A B : Type) [H1 : pointed A] [H2 : pointed B]
+      : pointed (A × B) :=
+  pointed.mk (pt,pt)
+
+  definition pprod [constructor] (A B : Type*) : Type* :=
+  pointed.mk' (A × B)
+
+  infixr ` ×* `:35 := pprod
+
+  definition ppr1 [constructor] {A B : Type*} : A ×* B →* A :=
+  pmap.mk pr1 idp
+
+  definition ppr2 [constructor] {A B : Type*} : A ×* B →* B :=
+  pmap.mk pr2 idp
+
+  definition tprod [constructor] {n : trunc_index} (A B : n-Type) : n-Type :=
+  trunctype.mk (A × B) _
+
+  infixr `×t`:30 := tprod
+
+  definition ptprod [constructor] {n : ℕ₋₂} (A B : n-Type*) : n-Type* :=
+  ptrunctype.mk' n (A × B)
+
+
+
+end prod
--- a/hott/types/sigma.hlean
+++ b/hott/types/sigma.hlean
@ -491,3 +491,28 @@ end sigma

 attribute sigma.is_trunc_sigma [instance] [priority 1490]
 attribute sigma.is_trunc_subtype [instance] [priority 1200]
+
+namespace sigma
+
+  /- pointed sigma type -/
+  open pointed
+
+  definition pointed_sigma [instance] [constructor] {A : Type} (P : A → Type) [G : pointed A]
+      [H : pointed (P pt)] : pointed (Σx, P x) :=
+  pointed.mk ⟨pt,pt⟩
+
+  definition psigma [constructor] {A : Type*} (P : A → Type*) : Type* :=
+  pointed.mk' (Σa, P a)
+
+  notation `Σ*` binders `, ` r:(scoped P, psigma P) := r
+
+  definition ppr1 [constructor] {A : Type*} {B : A → Type*} : (Σ*(x : A), B x) →* A :=
+  pmap.mk pr1 idp
+
+  definition ppr2 [unfold_full] {A : Type*} {B : A → Type*} (v : (Σ*(x : A), B x)) : B (ppr1 v) :=
+  pr2 v
+
+  definition ptsigma [constructor] {n : ℕ₋₂} {A : n-Type*} (P : A → n-Type*) : n-Type* :=
+  ptrunctype.mk' n (Σa, P a)
+
+end sigma
--- a/hott/types/sum.hlean
+++ b/hott/types/sum.hlean
@ -353,6 +353,15 @@ namespace sum
           begin intro v, induction v with b x, induction b, all_goals reflexivity end
           begin intro z, induction z with a b, all_goals reflexivity end

+  /- pointed sums. We arbitrarily choose (inl pt) as basepoint for the sum -/
+
+  open pointed
+  definition psum [constructor] (A B : Type*) : Type* :=
+  pointed.MK (A ⊎ B) (inl pt)
+
+  infixr ` +* `:30 := psum
+
+
 end sum
 open sum pi

--- a/hott/types/trunc.hlean
+++ b/hott/types/trunc.hlean
@ -332,6 +332,9 @@ namespace is_trunc
  definition tcast [unfold 4] {n : ℕ₋₂} {A B : n-Type} (p : A = B) (a : A) : B :=
  cast (ap trunctype.carrier p) a

+  definition ptcast [constructor] {n : ℕ₋₂} {A B : n-Type*} (p : A = B) : A →* B :=
+  pcast (ap ptrunctype.to_pType p)
+
  theorem tcast_tua_fn {n : ℕ₋₂} {A B : n-Type} (f : A ≃ B) : tcast (tua f) = to_fun f :=
  begin
    cases A with A HA, cases B with B HB, esimp at *,
@ -579,6 +582,12 @@ namespace trunc
    { apply trunc_trunc_equiv_left, exact H},
  end

+  definition trunc_functor_homotopy [unfold 7] {X Y : Type} (n : ℕ₋₂) {f g : X → Y}
+    (p : f ~ g) (x : trunc n X) : trunc_functor n f x = trunc_functor n g x :=
+  begin
+    induction x with x, esimp, exact ap tr (p x)
+  end
+
  definition trunc_functor_homotopy_of_le {n k : ℕ₋₂} {A B : Type} (f : A → B) (H : n ≤ k) :
    to_fun (trunc_trunc_equiv_left B H) ∘
    trunc_functor n (trunc_functor k f) ∘
@ -601,17 +610,10 @@ namespace trunc
    cases n with n: intro b,
    { exact tr (fiber.mk !center !is_prop.elim)},
    { refine @trunc.rec _ _ _ _ _ b, {intro x, exact is_trunc_of_le _ !minus_one_le_succ},
-      clear b, intro b, induction H b with v, induction v with a p,
+      clear b, intro b, induction H b with a p,
      exact tr (fiber.mk (tr a) (ap tr p))}
  end

-  /- the image of a map is the (-1)-truncated fiber -/
-  definition image [constructor] {A B : Type} (f : A → B) (b : B) : Prop := ∥ fiber f b ∥
-
-  definition image.mk [constructor] {A B : Type} {f : A → B} {b : B} (a : A) (p : f a = b)
-    : image f b :=
-  tr (fiber.mk a p)
-
  /- truncation of pointed types and its functorial action -/
  definition ptrunc [constructor] (n : ℕ₋₂) (X : Type*) : n-Type* :=
  ptrunctype.mk (trunc n X) _ (tr pt)
@ -666,6 +668,24 @@ namespace trunc
      rewrite succ_add_nat}
  end

+  definition iterated_loop_ptrunc_pequiv_con {n : ℕ₋₂} {k : ℕ} {A : Type*}
+    (p q : Ω[succ k] (ptrunc (n+succ k) A)) :
+    iterated_loop_ptrunc_pequiv n (succ k) A (p ⬝ q) =
+    trunc_concat (iterated_loop_ptrunc_pequiv n (succ k) A p)
+                 (iterated_loop_ptrunc_pequiv n (succ k) A q)  :=
+  begin
+    refine _ ⬝ loop_ptrunc_pequiv_con _ _,
+    exact ap !loop_ptrunc_pequiv !loop_pequiv_loop_con
+  end
+
+  definition iterated_loop_ptrunc_pequiv_inv_con {n : ℕ₋₂} {k : ℕ} {A : Type*}
+    (p q : ptrunc n (Ω[succ k] A)) :
+    (iterated_loop_ptrunc_pequiv n (succ k) A)⁻¹ᵉ* (trunc_concat p q) =
+    (iterated_loop_ptrunc_pequiv n (succ k) A)⁻¹ᵉ* p ⬝
+    (iterated_loop_ptrunc_pequiv n (succ k) A)⁻¹ᵉ* q :=
+  equiv.inv_preserve_binary (iterated_loop_ptrunc_pequiv n (succ k) A) concat trunc_concat
+    (@iterated_loop_ptrunc_pequiv_con n k A) p q
+
  definition ptrunc_functor_pcompose [constructor] {X Y Z : Type*} (n : ℕ₋₂) (g : Y →* Z)
    (f : X →* Y) : ptrunc_functor n (g ∘* f) ~* ptrunc_functor n g ∘* ptrunc_functor n f :=
  begin
@ -692,16 +712,73 @@ namespace trunc
    { induction p, reflexivity},
  end

+  definition ptrunc_functor_phomotopy [constructor] {X Y : Type*} (n : ℕ₋₂) {f g : X →* Y}
+    (p : f ~* g) : ptrunc_functor n f ~* ptrunc_functor n g :=
+  begin
+    fapply phomotopy.mk,
+    { exact trunc_functor_homotopy n p},
+    { esimp, refine !ap_con⁻¹ ⬝ _, exact ap02 tr !to_homotopy_pt},
+  end
+
+  definition pcast_ptrunc [constructor] (n : ℕ₋₂) {A B : Type*} (p : A = B) :
+    pcast (ap (ptrunc n) p) ~* ptrunc_functor n (pcast p) :=
+  begin
+    fapply phomotopy.mk,
+    { intro a, induction p, esimp, exact !trunc_functor_id⁻¹},
+    { induction p, reflexivity}
+  end
+
 end trunc open trunc

+/- some consequences for properties about functions (surjectivity etc.) -/
 namespace function
  variables {A B : Type}
  definition is_surjective_of_is_equiv [instance] (f : A → B) [H : is_equiv f] : is_surjective f :=
-  λb, begin esimp, apply center end
+  λb, begin esimp, apply center, apply is_trunc_trunc_of_is_trunc end

  definition is_equiv_equiv_is_embedding_times_is_surjective [constructor] (f : A → B)
    : is_equiv f ≃ (is_embedding f × is_surjective f) :=
  equiv_of_is_prop (λH, (_, _))
                    (λP, prod.rec_on P (λH₁ H₂, !is_equiv_of_is_surjective_of_is_embedding))

+  /-
+    Theorem 8.8.1:
+    A function is an equivalence if it's an embedding and it's action on sets is an surjection
+  -/
+  definition is_equiv_of_is_surjective_trunc_of_is_embedding {A B : Type} (f : A → B)
+    [H : is_embedding f] [H' : is_surjective (trunc_functor 0 f)] : is_equiv f :=
+  have is_surjective f,
+  begin
+    intro b,
+    induction H' (tr b) with a p,
+    induction a with a, esimp at p,
+    induction (tr_eq_tr_equiv _ _ _ p) with q,
+    exact image.mk a q
+  end,
+  is_equiv_of_is_surjective_of_is_embedding f
+
+  /-
+    Corollary 8.8.2:
+    A function f is an equivalence if Ωf and trunc_functor 0 f are equivalences
+  -/
+  definition is_equiv_of_is_equiv_ap1_of_is_equiv_trunc {A B : Type} (f : A → B)
+    [H : Πa, is_equiv (ap1 (pmap_of_map f a))] [H' : is_equiv (trunc_functor 0 f)] :
+    is_equiv f :=
+  have is_embedding f,
+  begin
+    intro a a',
+    apply is_equiv_of_imp_is_equiv,
+    intro p,
+    note q := ap (@tr 0 _) p,
+    note r := @(eq_of_fn_eq_fn' (trunc_functor 0 f)) _ (tr a) (tr a') q,
+    induction (tr_eq_tr_equiv _ _ _ r) with s,
+    induction s,
+    apply is_equiv.homotopy_closed (ap1 (pmap_of_map f a)),
+    intro p, apply idp_con
+  end,
+  is_equiv_of_is_surjective_trunc_of_is_embedding f
+
+  -- Whitehead's principle itself is in homotopy.homotopy_group, since it needs the definition of
+  -- a homotopy group.
+
 end function
--- a/hott/types/unit.hlean
+++ b/hott/types/unit.hlean
@ -6,7 +6,7 @@ Authors: Floris van Doorn
 Theorems about the unit type
 -/

-open equiv option eq
+open equiv option eq pointed is_trunc

 namespace unit

@ -25,6 +25,13 @@ namespace unit
  -- equivalences involving unit and other type constructors are in the file
  -- of the other constructor

+  /- pointed and truncated unit -/
+
+  definition punit [constructor] : Set* :=
+  pSet.mk' unit
+
+  notation `unit*` := punit
+
 end unit

 open unit is_trunc
--- a/library/data/nat/order.lean
+++ b/library/data/nat/order.lean
@ -228,6 +228,12 @@ lt.base n
 lemma lt_succ_of_lt {i j : nat} : i < j → i < succ j :=
 assume Plt, lt.trans Plt (self_lt_succ j)

+lemma one_le_succ (n : ℕ) : 1 ≤ succ n :=
+nat.succ_le_succ !zero_le
+
+lemma two_le_succ_succ (n : ℕ) : 2 ≤ succ (succ n) :=
+nat.succ_le_succ !one_le_succ
+
 /- increasing and decreasing functions -/

 section