diff --git a/homotopy/EM.hlean b/homotopy/EM.hlean
index 9349091..9b3cec4 100644
--- a/homotopy/EM.hlean
+++ b/homotopy/EM.hlean
@@ -326,6 +326,18 @@ namespace EM
   EMadd1_pequiv_succ_natural f n !isomorphism.refl !isomorphism.refl (π→g[n+2] f)
     proof λa, idp qed
 
+  definition EMadd1_pmap_equiv (n : ℕ) (X Y : Type*) [is_conn (n+1) X] [is_trunc (n+1+1) X]
+    [is_conn (n+1) Y] [is_trunc (n+1+1) Y] : (X →* Y) ≃ πag[n+2] X →g πag[n+2] Y :=
+  begin
+    fapply equiv.MK,
+    { exact π→g[n+2] },
+    { exact λφ, (EMadd1_pequiv_type Y n ∘* EMadd1_functor φ (n+1)) ∘* (EMadd1_pequiv_type X n)⁻¹ᵉ* },
+    { intro φ, apply homomorphism_eq,
+      refine homotopy_group_functor_compose (n+2) _ _ ⬝hty _, exact sorry }, -- easy but tedious
+    { intro f, apply eq_of_phomotopy, refine (phomotopy_pinv_right_of_phomotopy _)⁻¹*,
+      apply EMadd1_pequiv_type_natural }
+  end
+
   /- The Eilenberg-MacLane space K(G,n) with the same homotopy group as X on level n.
      On paper this is written K(πₙ(X), n). The problem is that for
      * n = 0 the expression π₀(X) is a pointed set, and K(X,0) needs X to be a pointed set
diff --git a/homotopy/pushout.hlean b/homotopy/pushout.hlean
index 844b4e9..c8f1a05 100644
--- a/homotopy/pushout.hlean
+++ b/homotopy/pushout.hlean
@@ -700,6 +700,19 @@ end
       apply eq_inv_con_of_con_eq, exact (to_homotopy_pt p)⁻¹ }
   end
 
+  definition pcofiber_elim_unique {X Y Z : Type*} {f : X →* Y}
+    {g₁ g₂ : pcofiber f →* Z} (h : g₁ ∘* pcod f ~* g₂ ∘* pcod f)
+    (sq : Πx, square (h (f x)) (respect_pt g₁ ⬝ (respect_pt g₂)⁻¹)
+      (ap g₁ (cofiber.glue x)) (ap g₂ (cofiber.glue x))) : g₁ ~* g₂ :=
+  begin
+    fapply phomotopy.mk,
+    { intro x, induction x with y x,
+      { exact h y },
+      { exact respect_pt g₁ ⬝ (respect_pt g₂)⁻¹ },
+      { apply eq_pathover, exact sq x }},
+    { apply inv_con_cancel_right }
+  end
+
   /-
     The maps  Z^{C_f} --> Z^Y --> Z^X  are exact at Z^Y.
     Here Y^X means pointed maps from X to Y and C_f is the cofiber of f.
diff --git a/homotopy/wedge.hlean b/homotopy/wedge.hlean
index 2e30696..939a415 100644
--- a/homotopy/wedge.hlean
+++ b/homotopy/wedge.hlean
@@ -1,6 +1,6 @@
 -- Authors: Floris van Doorn
 
-import homotopy.wedge
+import homotopy.wedge homotopy.cofiber ..move_to_lib .pushout
 
 open wedge pushout eq prod sum pointed equiv is_equiv unit lift bool option
 
@@ -107,4 +107,164 @@ equiv.MK add_point_of_wedge_pbool wedge_pbool_of_add_point
   calc plift.{u v} (A ∨ B) ≃* A ∨ B : by exact !pequiv_plift⁻¹ᵉ*
                        ... ≃* plift.{u v} A ∨ plift.{u v} B : by exact wedge_pequiv !pequiv_plift !pequiv_plift
 
+  protected definition pelim [constructor] {X Y Z : Type*} (f : X →* Z) (g : Y →* Z) : X ∨ Y →* Z :=
+  pmap.mk (wedge.elim f g (respect_pt f ⬝ (respect_pt g)⁻¹)) (respect_pt f)
+
+  definition wedge_pr1 [constructor] (X Y : Type*) : X ∨ Y →* X := wedge.pelim (pid X) (pconst Y X)
+  definition wedge_pr2 [constructor] (X Y : Type*) : X ∨ Y →* Y := wedge.pelim (pconst X Y) (pid Y)
+
+  open fiber prod cofiber pi
+
+variables {X Y : Type*}
+definition pcofiber_pprod_incl1_of_pfiber_wedge_pr2' [unfold 3]
+  (x : pfiber (wedge_pr2 X Y)) : pcofiber (pprod_incl1 (Ω Y) X) :=
+begin
+  induction x with x p, induction x with x y,
+  { exact cod _ (p, x) },
+  { exact pt },
+  { apply arrow_pathover_constant_right, intro p, apply cofiber.glue }
+end
+
+--set_option pp.all true
+/-
+  X : Type* has a nondegenerate basepoint iff
+  it has the homotopy extension property iff
+  Π(f : X → Y) (y : Y) (p : f pt = y), ∃(g : X → Y) (h : f ~ g) (q : y = g pt), h pt = p ⬝ q
+ (or Σ?)
+-/
+
+definition pfiber_wedge_pr2_of_pcofiber_pprod_incl1' [unfold 3]
+  (x : pcofiber (pprod_incl1 (Ω Y) X)) : pfiber (wedge_pr2 X Y) :=
+begin
+  induction x with v p,
+  { induction v with p x, exact fiber.mk (inl x) p },
+  { exact fiber.mk (inr pt) idp },
+  { esimp, apply fiber_eq (wedge.glue ⬝ ap inr p), symmetry,
+      refine !ap_con ⬝ !wedge.elim_glue ◾ (!ap_compose'⁻¹ ⬝ !ap_id) ⬝ !idp_con }
+end
+
+variables (X Y)
+definition pcofiber_pprod_incl1_of_pfiber_wedge_pr2 [constructor] :
+  pfiber (wedge_pr2 X Y) →* pcofiber (pprod_incl1 (Ω Y) X) :=
+pmap.mk pcofiber_pprod_incl1_of_pfiber_wedge_pr2' (cofiber.glue idp)
+
+-- definition pfiber_wedge_pr2_of_pprod [constructor] :
+--   Ω Y ×* X →* pfiber (wedge_pr2 X Y) :=
+-- begin
+--   fapply pmap.mk,
+--   { intro v, induction v with p x, exact fiber.mk (inl x) p },
+--   { reflexivity }
+-- end
+
+definition pfiber_wedge_pr2_of_pcofiber_pprod_incl1 [constructor] :
+  pcofiber (pprod_incl1 (Ω Y) X) →* pfiber (wedge_pr2 X Y) :=
+pmap.mk pfiber_wedge_pr2_of_pcofiber_pprod_incl1'
+  begin refine (fiber_eq wedge.glue _)⁻¹, exact !wedge.elim_glue⁻¹ end
+-- pcofiber.elim (pfiber_wedge_pr2_of_pprod X Y)
+--   begin
+--     fapply phomotopy.mk,
+--     { intro p, apply fiber_eq (wedge.glue ⬝ ap inr p ⬝ wedge.glue⁻¹), symmetry,
+--       refine !ap_con ⬝ (!ap_con ⬝ !wedge.elim_glue ◾ (!ap_compose'⁻¹ ⬝ !ap_id)) ◾
+--         (!ap_inv ⬝ !wedge.elim_glue⁻²) ⬝ _, exact idp_con p },
+--     { esimp, refine fiber_eq2 (con.right_inv wedge.glue) _ ⬝ !fiber_eq_eta⁻¹,
+--       rewrite [idp_con, ↑fiber_eq_pr2, con2_idp, whisker_right_idp, whisker_right_idp],
+--       -- refine _ ⬝ (eq_bot_of_square (transpose (ap_con_right_inv_sq
+--       --              (wedge.elim (λx : X, Point Y) (@id Y) idp) wedge.glue)))⁻¹,
+--       -- refine whisker_right _ !con_inv ⬝ _,
+--       exact sorry
+-- }
+--   end
+
+--set_option pp.notation false
+set_option pp.binder_types true
+open sigma.ops
+definition pfiber_wedge_pr2_pequiv_pcofiber_pprod_incl1 [constructor] :
+  pfiber (wedge_pr2 X Y) ≃* pcofiber (pprod_incl1 (Ω Y) X) :=
+pequiv.MK (pcofiber_pprod_incl1_of_pfiber_wedge_pr2 _ _)
+          (pfiber_wedge_pr2_of_pcofiber_pprod_incl1 _ _)
+  abstract begin
+    fapply phomotopy.mk,
+    { intro x, esimp, induction x with x p,  induction x with x y,
+      { reflexivity },
+      { refine (fiber_eq (ap inr p) _)⁻¹, refine !ap_id⁻¹ ⬝ !ap_compose' },
+      { apply @pi_pathover_right' _ _ _ _ (λ(xp : Σ(x : X ∨ Y), pppi.to_fun (wedge_pr2 X Y) x = pt),
+          pfiber_wedge_pr2_of_pcofiber_pprod_incl1'
+          (pcofiber_pprod_incl1_of_pfiber_wedge_pr2' (mk xp.1 xp.2)) = mk xp.1 xp.2),
+        intro p, apply eq_pathover, exact sorry }},
+    { symmetry, refine !cofiber.elim_glue ◾ idp ⬝ _, apply con_inv_eq_idp,
+      apply ap (fiber_eq wedge.glue), esimp, rewrite [idp_con], refine !whisker_right_idp⁻² }
+  end end
+  abstract begin
+    exact sorry
+  end end
+-- apply eq_pathover_id_right, refine ap_compose pcofiber_pprod_incl1_of_pfiber_wedge_pr2 _ _ ⬝ ap02 _ !elim_glue ⬝ph _
+-- apply eq_pathover_id_right, refine ap_compose pfiber_wedge_pr2_of_pcofiber_pprod_incl1 _ _ ⬝ ap02 _ !elim_glue ⬝ph _
+
+/- move -/
+definition ap1_idp {A B : Type*} (f : A →* B) : Ω→ f idp = idp :=
+respect_pt (Ω→ f)
+
+definition ap1_phomotopy_idp {A B : Type*} {f g : A →* B} (h : f ~* g) :
+  Ω⇒ h idp = !respect_pt ⬝ !respect_pt⁻¹ :=
+sorry
+
+
+variables {A} {B : Type*} {f : A →* B} {g : B →* A} (h : f ∘* g ~* pid B)
+include h
+definition nar_of_noo' (p : Ω A) : Ω (pfiber f) ×* Ω B :=
+begin
+  refine (_, Ω→ f p),
+  have z : Ω A →* Ω A, from pmap.mk (λp, Ω→ (g ∘* f) p ⬝ p⁻¹) proof (respect_pt (Ω→ (g ∘* f))) qed,
+  refine fiber_eq ((Ω→ g ∘* Ω→ f) p ⬝ p⁻¹) (!idp_con⁻¹ ⬝ whisker_right (respect_pt f) _⁻¹),
+  induction B with B b₀, induction f with f f₀, esimp at * ⊢, induction f₀,
+  refine !idp_con⁻¹ ⬝ ap1_con (pmap_of_map f pt) _ _ ⬝
+    ((ap1_pcompose (pmap_of_map f pt) g _)⁻¹ ⬝ Ω⇒ h _ ⬝ ap1_pid _) ◾ ap1_inv _ _ ⬝ !con.right_inv
+end
+
+definition noo_of_nar' (x : Ω (pfiber f) ×* Ω B) : Ω A :=
+begin
+  induction x with p q, exact Ω→ (ppoint f) p ⬝ Ω→ g q
+end
+
+variables (f g)
+definition nar_of_noo [constructor] :
+  Ω A →* Ω (pfiber f) ×* Ω B :=
+begin
+  refine pmap.mk (nar_of_noo' h) (prod_eq _ (ap1_gen_idp f (respect_pt f))),
+  esimp [nar_of_noo'],
+  refine fiber_eq2 (ap (ap1_gen _ _ _) (ap1_gen_idp f _) ⬝ !ap1_gen_idp) _ ⬝ !fiber_eq_eta⁻¹,
+  induction B with B b₀, induction f with f f₀, esimp at * ⊢, induction f₀, esimp,
+  refine (!idp_con ⬝ !whisker_right_idp) ◾ !whisker_right_idp ⬝ _, esimp [fiber_eq_pr2],
+  apply inv_con_eq_idp,
+  refine ap (ap02 f) !idp_con ⬝ _,
+  esimp [ap1_con, ap1_gen_con, ap1_inv, ap1_gen_inv],
+  refine _ ⬝ whisker_left _ (!con2_idp ⬝ !whisker_right_idp ⬝ idp ◾ ap1_phomotopy_idp h)⁻¹ᵖ,
+  esimp, exact sorry
+end
+
+definition noo_of_nar [constructor] :
+  Ω (pfiber f) ×* Ω B →* Ω A :=
+pmap.mk (noo_of_nar' h) (respect_pt (Ω→ (ppoint f)) ◾ respect_pt (Ω→ g))
+
+definition noo_pequiv_nar [constructor] :
+  Ω A ≃* Ω (pfiber f) ×* Ω B :=
+pequiv.MK (nar_of_noo f g h) (noo_of_nar f g h)
+  abstract begin
+    exact sorry
+  end end
+  abstract begin
+    exact sorry
+  end end
+-- apply eq_pathover_id_right, refine ap_compose nar_of_noo _ _ ⬝ ap02 _ !elim_glue ⬝ph _
+-- apply eq_pathover_id_right, refine ap_compose noo_of_nar _ _ ⬝ ap02 _ !elim_glue ⬝ph _
+
+  definition loop_pequiv_of_cross_section {A B : Type*} (f : A →* B) (g : B →* A)
+    (h : f ∘* g ~* pid B) : Ω A ≃* Ω (pfiber f) ×* Ω B :=
+
+
+
+
+
+
+
 end wedge
diff --git a/move_to_lib.hlean b/move_to_lib.hlean
index 8b1b094..5e7e23f 100644
--- a/move_to_lib.hlean
+++ b/move_to_lib.hlean
@@ -5,617 +5,55 @@ import homotopy.sphere2 homotopy.cofiber homotopy.wedge hit.prop_trunc hit.set_q
 open eq nat int susp pointed sigma is_equiv equiv fiber algebra trunc pi group
      is_trunc function unit prod bool
 
-attribute pType.sigma_char sigma_pi_equiv_pi_sigma sigma.coind_unc [constructor]
-attribute ap1_gen [unfold 8 9 10]
-attribute ap010 [unfold 7]
-attribute tro_invo_tro [unfold 9] -- TODO: move
-  -- TODO: homotopy_of_eq and apd10 should be the same
-  -- TODO: there is also apd10_eq_of_homotopy in both pi and eq(?)
 universe variable u
 
-
-namespace algebra
-
-variables {A : Type} [add_ab_inf_group A]
-definition add_sub_cancel_middle (a b : A) : a + (b - a) = b :=
-!add.comm ⬝ !sub_add_cancel
-
-end algebra
+/-
+eq_of_homotopy_eta     > eq_of_homotopy_apd10
+pathover_of_tr_eq_idp  > pathover_idp_of_eq
+pathover_of_tr_eq_idp' > pathover_of_tr_eq_idp
+homotopy_group_isomorphism_of_ptrunc_pequiv > ghomotopy_group_isomorphism_of_ptrunc_pequiv
+equiv_pathover <> equiv_pathover2
+homotopy_group_functor_succ_phomotopy_in > homotopy_group_succ_in_natural
+homotopy_group_succ_in_natural > homotopy_group_succ_in_natural_unpointed
+le_step_left > le_of_succ_le
+pmap.eta > pmap_eta
+pType.sigma_char' > pType.sigma_char
+cghomotopy_group to aghomotopy_group
+-/
 
 namespace eq
 
-  -- this should maybe replace whisker_left_idp and whisker_left_idp_con
-  definition whisker_left_idp_square {A : Type} {a a' : A} {p q : a = a'} (r : p = q) :
-    square (whisker_left idp r) r (idp_con p) (idp_con q) :=
-  begin induction r, exact hrfl end
+  definition transport_lemma {A : Type} {C : A → Type} {g₁ : A → A}
+    {x y : A} (p : x = y) (f : Π⦃x⦄, C x → C (g₁ x)) (z : C x) :
+    transport C (ap g₁ p)⁻¹ (f (transport C p z)) = f z :=
+  by induction p; reflexivity
 
-  definition ap_con_idp_left {A B : Type} (f : A → B) {a a' : A} (p : a = a') :
-    square (ap_con f idp p) idp (ap02 f (idp_con p)) (idp_con (ap f p)) :=
-  begin induction p, exact ids end
-
-  definition pathover_tr_pathover_idp_of_eq {A : Type} {B : A → Type} {a a' : A} {b : B a} {b' : B a'} {p : a = a'}
-    (q : b =[p] b') :
-    pathover_tr p b ⬝o pathover_idp_of_eq (tr_eq_of_pathover q) = q :=
-  begin induction q; reflexivity end
-
-  -- rename pathover_of_tr_eq_idp
-  definition pathover_of_tr_eq_idp' {A : Type} {B : A → Type} {a a₂ : A} (p : a = a₂) (b : B a) :
-    pathover_of_tr_eq idp = pathover_tr p b :=
-  by induction p; constructor
-
-definition homotopy.symm_symm {A : Type} {P : A → Type} {f g : Πx, P x} (H : f ~ g) :
-  H⁻¹ʰᵗʸ⁻¹ʰᵗʸ = H :=
-begin apply eq_of_homotopy, intro x, apply inv_inv end
-
-  definition apd10_prepostcompose_nondep {A B C D : Type} (h : C → D) {g g' : B → C} (p : g = g')
-    (f : A → B) (a : A) : apd10 (ap (λg a, h (g (f a))) p) a = ap h (apd10 p (f a)) :=
-  begin induction p, reflexivity end
-
-  definition apd10_prepostcompose {A B : Type} {C : B → Type} {D : A → Type}
-    (f : A → B) (h : Πa, C (f a) → D a) {g g' : Πb, C b}
-    (p : g = g') (a : A) :
-    apd10 (ap (λg a, h a (g (f a))) p) a = ap (h a) (apd10 p (f a)) :=
-  begin induction p, reflexivity end
-
-  definition eq.rec_to {A : Type} {a₀ : A} {P : Π⦃a₁⦄, a₀ = a₁ → Type}
-    {a₁ : A} (p₀ : a₀ = a₁) (H : P p₀) ⦃a₂ : A⦄ (p : a₀ = a₂) : P p :=
-  begin
-    induction p₀, induction p, exact H
-  end
-
-  definition eq.rec_to2 {A : Type} {P : Π⦃a₀ a₁⦄, a₀ = a₁ → Type}
-    {a₀ a₀' a₁' : A} (p' : a₀' = a₁') (p₀ : a₀ = a₀') (H : P p') ⦃a₁ : A⦄ (p : a₀ = a₁) : P p :=
-  begin
-   induction p₀, induction p', induction p, exact H
-  end
-
-  definition eq.rec_right_inv {A : Type} (f : A ≃ A) {P : Π⦃a₀ a₁⦄, f a₀ = a₁ → Type}
-    (H : Πa, P (right_inv f a)) ⦃a₀ a₁ : A⦄ (p : f a₀ = a₁) : P p :=
-  begin
-    revert a₀ p, refine equiv_rect f⁻¹ᵉ _ _,
-    intro a₀ p, exact eq.rec_to (right_inv f a₀) (H a₀) p,
-  end
-
-  definition eq.rec_equiv {A B : Type} {a₀ : A} (f : A ≃ B) {P : Π{a₁}, f a₀ = f a₁ → Type}
-    (H : P (idpath (f a₀))) ⦃a₁ : A⦄ (p : f a₀ = f a₁) : P p :=
-  begin
-    assert qr : Σ(q : a₀ = a₁), ap f q = p,
-    { exact ⟨eq_of_fn_eq_fn f p, ap_eq_of_fn_eq_fn' f p⟩ },
-    cases qr with q r, apply transport P r, induction q, exact H
-  end
-
-  definition eq.rec_equiv_symm {A B : Type} {a₁ : A} (f : A ≃ B) {P : Π{a₀}, f a₀ = f a₁ → Type}
-    (H : P (idpath (f a₁))) ⦃a₀ : A⦄ (p : f a₀ = f a₁) : P p :=
-  begin
-    assert qr : Σ(q : a₀ = a₁), ap f q = p,
-    { exact ⟨eq_of_fn_eq_fn f p, ap_eq_of_fn_eq_fn' f p⟩ },
-    cases qr with q r, apply transport P r, induction q, exact H
-  end
-
-  definition eq.rec_equiv_to_same {A B : Type} {a₀ : A} (f : A ≃ B) {P : Π{a₁}, f a₀ = f a₁ → Type}
-    ⦃a₁' : A⦄ (p' : f a₀ = f a₁') (H : P p') ⦃a₁ : A⦄ (p : f a₀ = f a₁) : P p :=
-  begin
-    revert a₁' p' H a₁ p,
-    refine eq.rec_equiv f _,
-    exact eq.rec_equiv f
-  end
-
-  definition eq.rec_equiv_to {A A' B : Type} {a₀ : A} (f : A ≃ B) (g : A' ≃ B)
-    {P : Π{a₁}, f a₀ = g a₁ → Type}
-    ⦃a₁' : A'⦄ (p' : f a₀ = g a₁') (H : P p') ⦃a₁ : A'⦄ (p : f a₀ = g a₁) : P p :=
-  begin
-    assert qr : Σ(q : g⁻¹ (f a₀) = a₁), (right_inv g (f a₀))⁻¹ ⬝ ap g q = p,
-    { exact ⟨eq_of_fn_eq_fn g (right_inv g (f a₀) ⬝ p),
-             whisker_left _ (ap_eq_of_fn_eq_fn' g _) ⬝ !inv_con_cancel_left⟩ },
-    assert q'r' : Σ(q' : g⁻¹ (f a₀) = a₁'), (right_inv g (f a₀))⁻¹ ⬝ ap g q' = p',
-    { exact ⟨eq_of_fn_eq_fn g (right_inv g (f a₀) ⬝ p'),
-             whisker_left _ (ap_eq_of_fn_eq_fn' g _) ⬝ !inv_con_cancel_left⟩ },
-    induction qr with q r, induction q'r' with q' r',
-    induction q, induction q',
-    induction r, induction r',
-    exact H
-  end
-
-  definition eq.rec_grading {A A' B : Type} {a : A} (f : A ≃ B) (g : A' ≃ B)
-    {P : Π{b}, f a = b → Type}
-    {a' : A'} (p' : f a = g a') (H : P p') ⦃b : B⦄ (p : f a = b) : P p :=
-  begin
-    revert b p, refine equiv_rect g _ _,
-    exact eq.rec_equiv_to f g p' H
-  end
-
-  definition eq.rec_grading_unbased {A B B' C : Type} (f : A ≃ B) (g : B ≃ C) (h : B' ≃ C)
-    {P : Π{b c}, g b = c → Type}
-    {a' : A} {b' : B'} (p' : g (f a') = h b') (H : P p') ⦃b : B⦄ ⦃c : C⦄ (q : f a' = b)
-    (p : g b = c) : P p :=
-  begin
-    induction q, exact eq.rec_grading (f ⬝e g) h p' H p
-  end
-
-  -- definition homotopy_group_homomorphism_pinv (n : ℕ) {A B : Type*} (f : A ≃* B) :
-  --   π→g[n+1] f⁻¹ᵉ* ~ (homotopy_group_isomorphism_of_pequiv n f)⁻¹ᵍ :=
-  -- begin
-  --   -- refine ptrunc_functor_phomotopy 0 !apn_pinv ⬝hty _,
-  --   -- intro x, esimp,
-  -- end
-
-  -- definition natural_square_tr_eq {A B : Type} {a a' : A} {f g : A → B}
-  --   (p : f ~ g) (q : a = a') : natural_square p q = square_of_pathover (apd p q) :=
-  -- idp
-
-  lemma homotopy_group_isomorphism_of_ptrunc_pequiv {A B : Type*}
-    (n k : ℕ) (H : n+1 ≤[ℕ] k) (f : ptrunc k A ≃* ptrunc k B) : πg[n+1] A ≃g πg[n+1] B :=
-  (ghomotopy_group_ptrunc_of_le H A)⁻¹ᵍ ⬝g
-  homotopy_group_isomorphism_of_pequiv n f ⬝g
-  ghomotopy_group_ptrunc_of_le H B
-
-definition fundamental_group_isomorphism {X : Type*} {G : Group}
-  (e : Ω X ≃ G) (hom_e : Πp q, e (p ⬝ q) = e p * e q) : π₁ X ≃g G :=
-isomorphism_of_equiv (trunc_equiv_trunc 0 e ⬝e (trunc_equiv 0 G))
-  begin intro p q, induction p with p, induction q with q, exact hom_e p q end
-
-definition equiv_pathover2 {A : Type} {a a' : A} (p : a = a')
-  {B : A → Type} {C : A → Type} (f : B a ≃ C a) (g : B a' ≃ C a')
-  (r : to_fun f =[p] to_fun g) : f =[p] g :=
-begin
-  fapply pathover_of_fn_pathover_fn,
-  { intro a, apply equiv.sigma_char },
-  { apply sigma_pathover _ _ _ r, apply is_prop.elimo }
-end
-
-definition equiv_pathover_inv {A : Type} {a a' : A} (p : a = a')
-  {B : A → Type} {C : A → Type} (f : B a ≃ C a) (g : B a' ≃ C a')
-  (r : to_inv f =[p] to_inv g) : f =[p] g :=
-begin
-  /- this proof is a bit weird, but it works -/
-  apply equiv_pathover2,
-  change f⁻¹ᶠ⁻¹ᶠ =[p] g⁻¹ᶠ⁻¹ᶠ,
-  apply apo (λ(a: A) (h : C a ≃ B a), h⁻¹ᶠ),
-  apply equiv_pathover2,
-  exact r
-end
-
-definition transport_lemma {A : Type} {C : A → Type} {g₁ : A → A}
-  {x y : A} (p : x = y) (f : Π⦃x⦄, C x → C (g₁ x)) (z : C x) :
-  transport C (ap g₁ p)⁻¹ (f (transport C p z)) = f z :=
-by induction p; reflexivity
-
-definition transport_lemma2 {A : Type} {C : A → Type} {g₁ : A → A}
-  {x y : A} (p : x = y) (f : Π⦃x⦄, C x → C (g₁ x)) (z : C x) :
-  transport C (ap g₁ p) (f z) = f (transport C p z) :=
-by induction p; reflexivity
-
-definition eq_of_pathover_apo {A C : Type} {B : A → Type} {a a' : A} {b : B a} {b' : B a'}
-  {p : a = a'} (g : Πa, B a → C) (q : b =[p] b') :
-  eq_of_pathover (apo g q) = apd011 g p q :=
-by induction q; reflexivity
-
-  definition apd02 [unfold 8] {A : Type} {B : A → Type} (f : Πa, B a) {a a' : A} {p q : a = a'}
-    (r : p = q) : change_path r (apd f p) = apd f q :=
-  by induction r; reflexivity
-
-  definition pathover_ap_cono {A A' : Type} {a₁ a₂ a₃ : A}
-    {p₁ : a₁ = a₂} {p₂ : a₂ = a₃} (B' : A' → Type) (f : A → A')
-    {b₁ : B' (f a₁)} {b₂ : B' (f a₂)} {b₃ : B' (f a₃)}
-    (q₁ : b₁ =[p₁] b₂) (q₂ : b₂ =[p₂] b₃) :
-    pathover_ap B' f (q₁ ⬝o q₂) =
-    change_path !ap_con⁻¹ (pathover_ap B' f q₁ ⬝o pathover_ap B' f q₂) :=
-  by induction q₁; induction q₂; reflexivity
-
-  definition concato_eq_eq {A : Type} {B : A → Type} {a₁ a₂ : A} {p₁ : a₁ = a₂}
-    {b₁ : B a₁} {b₂ b₂' : B a₂} (r : b₁ =[p₁] b₂) (q : b₂ = b₂') :
-    r ⬝op q = r ⬝o pathover_idp_of_eq q :=
-  by induction q; reflexivity
-
-definition ap_apd0111 {A₁ A₂ A₃ : Type} {B : A₁ → Type} {C : Π⦃a⦄, B a → Type} {a a₂ : A₁}
-  {b : B a} {b₂ : B a₂} {c : C b} {c₂ : C b₂}
-  (g : A₂ → A₃) (f : Πa b, C b → A₂) (Ha : a = a₂) (Hb : b =[Ha] b₂)
-    (Hc : c =[apd011 C Ha Hb] c₂) :
-  ap g (apd0111 f Ha Hb Hc) = apd0111 (λa b c, (g (f a b c))) Ha Hb Hc :=
-by induction Hb; induction Hc using idp_rec_on; reflexivity
-
-section squareover
-
-  variables {A A' : Type} {B : A → Type}
-            {a a' a'' a₀₀ a₂₀ a₄₀ a₀₂ a₂₂ a₂₄ a₀₄ a₄₂ a₄₄ : A}
-            /-a₀₀-/ {p₁₀ : a₀₀ = a₂₀} /-a₂₀-/ {p₃₀ : a₂₀ = a₄₀} /-a₄₀-/
-       {p₀₁ : a₀₀ = a₀₂} /-s₁₁-/ {p₂₁ : a₂₀ = a₂₂} /-s₃₁-/ {p₄₁ : a₄₀ = a₄₂}
-            /-a₀₂-/ {p₁₂ : a₀₂ = a₂₂} /-a₂₂-/ {p₃₂ : a₂₂ = a₄₂} /-a₄₂-/
-       {p₀₃ : a₀₂ = a₀₄} /-s₁₃-/ {p₂₃ : a₂₂ = a₂₄} /-s₃₃-/ {p₄₃ : a₄₂ = a₄₄}
-            /-a₀₄-/ {p₁₄ : a₀₄ = a₂₄} /-a₂₄-/ {p₃₄ : a₂₄ = a₄₄} /-a₄₄-/
-            {s₁₁ : square p₁₀ p₁₂ p₀₁ p₂₁} {s₃₁ : square p₃₀ p₃₂ p₂₁ p₄₁}
-            {s₁₃ : square p₁₂ p₁₄ p₀₃ p₂₃} {s₃₃ : square p₃₂ p₃₄ p₂₃ p₄₃}
-
-            {b : B a}
-            {b₀₀ : B a₀₀} {b₂₀ : B a₂₀} {b₄₀ : B a₄₀}
-            {b₀₂ : B a₀₂} {b₂₂ : B a₂₂} {b₄₂ : B a₄₂}
-            {b₀₄ : B a₀₄} {b₂₄ : B a₂₄} {b₄₄ : B a₄₄}
-            /-b₀₀-/ {q₁₀ : b₀₀ =[p₁₀] b₂₀} /-b₂₀-/ {q₃₀ : b₂₀ =[p₃₀] b₄₀} /-b₄₀-/
-            /-b₀₂-/ {q₁₂ : b₀₂ =[p₁₂] b₂₂} /-b₂₂-/ {q₃₂ : b₂₂ =[p₃₂] b₄₂} /-b₄₂-/
-            /-b₀₄-/ {q₁₄ : b₀₄ =[p₁₄] b₂₄} /-b₂₄-/ {q₃₄ : b₂₄ =[p₃₄] b₄₄} /-b₄₄-/
-   {q₀₁ : b₀₀ =[p₀₁] b₀₂} /-t₁₁-/ {q₂₁ : b₂₀ =[p₂₁] b₂₂} /-t₃₁-/ {q₄₁ : b₄₀ =[p₄₁] b₄₂}
-   {q₀₃ : b₀₂ =[p₀₃] b₀₄} /-t₁₃-/ {q₂₃ : b₂₂ =[p₂₃] b₂₄} /-t₃₃-/ {q₄₃ : b₄₂ =[p₄₃] b₄₄}
-
-  definition move_right_of_top_over {p : a₀₀ = a} {p' : a = a₂₀}
-    {s : square p p₁₂ p₀₁ (p' ⬝ p₂₁)} {q : b₀₀ =[p] b} {q' : b =[p'] b₂₀}
-    (t : squareover B (move_top_of_right s) (q ⬝o q') q₁₂ q₀₁ q₂₁) :
-    squareover B s q q₁₂ q₀₁ (q' ⬝o q₂₁) :=
-  begin induction q', induction q, induction q₂₁, exact t end
-
-  /- TODO: replace the version in the library by this -/
-  definition hconcato_pathover' {p : a₂₀ = a₂₂} {sp : p = p₂₁} {s : square p₁₀ p₁₂ p₀₁ p}
-    {q : b₂₀ =[p] b₂₂} (t₁₁ : squareover B (s ⬝hp sp) q₁₀ q₁₂ q₀₁ q₂₁)
-    (r : change_path sp q = q₂₁) : squareover B s q₁₀ q₁₂ q₀₁ q :=
-  by induction sp; induction r; exact t₁₁
-
-  variables (s₁₁ q₀₁ q₁₀ q₂₁ q₁₂)
-  definition squareover_fill_t : Σ (q : b₀₀ =[p₁₀] b₂₀), squareover B s₁₁ q q₁₂ q₀₁ q₂₁ :=
-  begin
-    induction s₁₁, induction q₀₁ using idp_rec_on, induction q₂₁ using idp_rec_on,
-    induction q₁₂ using idp_rec_on, exact ⟨idpo, idso⟩
-  end
-
-  definition squareover_fill_b : Σ (q : b₀₂ =[p₁₂] b₂₂), squareover B s₁₁ q₁₀ q q₀₁ q₂₁ :=
-  begin
-    induction s₁₁, induction q₀₁ using idp_rec_on, induction q₂₁ using idp_rec_on,
-    induction q₁₀ using idp_rec_on, exact ⟨idpo, idso⟩
-  end
-
-  definition squareover_fill_l : Σ (q : b₀₀ =[p₀₁] b₀₂), squareover B s₁₁ q₁₀ q₁₂ q q₂₁ :=
-  begin
-    induction s₁₁, induction q₁₀ using idp_rec_on, induction q₂₁ using idp_rec_on,
-    induction q₁₂ using idp_rec_on, exact ⟨idpo, idso⟩
-  end
-
-  definition squareover_fill_r : Σ (q : b₂₀ =[p₂₁] b₂₂) , squareover B s₁₁ q₁₀ q₁₂ q₀₁ q :=
-  begin
-    induction s₁₁, induction q₀₁ using idp_rec_on, induction q₁₀ using idp_rec_on,
-    induction q₁₂ using idp_rec_on, exact ⟨idpo, idso⟩
-  end
-
-
-end squareover
-
-/- move this to types.eq, and replace the proof there -/
-  section
-    parameters {A : Type} (a₀ : A) (code : A → Type) (H : is_contr (Σa, code a))
-      (c₀ : code a₀)
-    include H c₀
-    protected definition encode2 {a : A} (q : a₀ = a) : code a :=
-    transport code q c₀
-
-    protected definition decode2' {a : A} (c : code a) : a₀ = a :=
-    have ⟨a₀, c₀⟩ = ⟨a, c⟩ :> Σa, code a, from !is_prop.elim,
-    this..1
-
-    protected definition decode2 {a : A} (c : code a) : a₀ = a :=
-    (decode2' c₀)⁻¹ ⬝ decode2' c
-
-    open sigma.ops
-    definition total_space_method2 (a : A) : (a₀ = a) ≃ code a :=
-    begin
-      fapply equiv.MK,
-      { exact encode2 },
-      { exact decode2 },
-      { intro c, unfold [encode2, decode2, decode2'],
-        rewrite [is_prop_elim_self, ▸*, idp_con],
-        apply tr_eq_of_pathover, apply eq_pr2 },
-      { intro q, induction q, esimp, apply con.left_inv, },
-    end
-  end
-
-definition total_space_method2_refl {A : Type} (a₀ : A) (code : A → Type) (H : is_contr (Σa, code a))
-  (c₀ : code a₀) : total_space_method2 a₀ code H c₀ a₀ idp = c₀ :=
-begin
-  reflexivity
-end
-
-  section hsquare
-  variables {A₀₀ A₂₀ A₄₀ A₀₂ A₂₂ A₄₂ A₀₄ A₂₄ A₄₄ : Type}
-            {f₁₀ : A₀₀ → A₂₀} {f₃₀ : A₂₀ → A₄₀}
-            {f₀₁ : A₀₀ → A₀₂} {f₂₁ : A₂₀ → A₂₂} {f₄₁ : A₄₀ → A₄₂}
-            {f₁₂ : A₀₂ → A₂₂} {f₃₂ : A₂₂ → A₄₂}
-            {f₀₃ : A₀₂ → A₀₄} {f₂₃ : A₂₂ → A₂₄} {f₄₃ : A₄₂ → A₄₄}
-            {f₁₄ : A₀₄ → A₂₄} {f₃₄ : A₂₄ → A₄₄}
-
-  definition trunc_functor_hsquare (n : ℕ₋₂) (h : hsquare f₁₀ f₁₂ f₀₁ f₂₁) :
-    hsquare (trunc_functor n f₁₀) (trunc_functor n f₁₂)
-            (trunc_functor n f₀₁) (trunc_functor n f₂₁) :=
-  λa, !trunc_functor_compose⁻¹ ⬝ trunc_functor_homotopy n h a ⬝ !trunc_functor_compose
-
-  attribute hhconcat hvconcat [unfold_full]
-
-  definition rfl_hhconcat (q : hsquare f₃₀ f₃₂ f₂₁ f₄₁) : homotopy.rfl ⬝htyh q ~ q :=
-  homotopy.rfl
-
-  definition hhconcat_rfl (q : hsquare f₃₀ f₃₂ f₂₁ f₄₁) : q ⬝htyh homotopy.rfl ~ q :=
-  λx, !idp_con ⬝ ap_id (q x)
-
-  definition rfl_hvconcat (q : hsquare f₃₀ f₃₂ f₂₁ f₄₁) : homotopy.rfl ⬝htyv q ~ q :=
-  λx, !idp_con
-
-  definition hvconcat_rfl (q : hsquare f₃₀ f₃₂ f₂₁ f₄₁) : q ⬝htyv homotopy.rfl ~ q :=
-  λx, !ap_id
-
-  end hsquare
-  definition homotopy_group_succ_in_natural (n : ℕ) {A B : Type*} (f : A →* B) :
-    hsquare (homotopy_group_succ_in A n) (homotopy_group_succ_in B n) (π→[n+1] f) (π→[n] (Ω→ f)) :=
-  trunc_functor_hsquare _ (loopn_succ_in_natural n f)⁻¹*
-
-  definition homotopy2.refl {A} {B : A → Type} {C : Π⦃a⦄, B a → Type} (f : Πa (b : B a), C b) :
-    f ~2 f :=
-  λa b, idp
-
-  definition homotopy2.rfl [refl] {A} {B : A → Type} {C : Π⦃a⦄, B a → Type}
-    {f : Πa (b : B a), C b} : f ~2 f :=
-  λa b, idp
-
-  definition homotopy3.refl {A} {B : A → Type} {C : Πa, B a → Type}
-    {D : Π⦃a⦄ ⦃b : B a⦄, C a b → Type} (f : Πa b (c : C a b), D c) : f ~3 f :=
-  λa b c, idp
-
-  definition homotopy3.rfl {A} {B : A → Type} {C : Πa, B a → Type}
-    {D : Π⦃a⦄ ⦃b : B a⦄, C a b → Type} {f : Πa b (c : C a b), D c} : f ~3 f :=
-  λa b c, idp
-
-  definition eq_tr_of_pathover_con_tr_eq_of_pathover {A : Type} {B : A → Type}
-    {a₁ a₂ : A} (p : a₁ = a₂) {b₁ : B a₁} {b₂ : B a₂} (q : b₁ =[p] b₂) :
-    eq_tr_of_pathover q ⬝ tr_eq_of_pathover q⁻¹ᵒ = idp :=
-  by induction q; reflexivity
+  definition transport_lemma2 {A : Type} {C : A → Type} {g₁ : A → A}
+    {x y : A} (p : x = y) (f : Π⦃x⦄, C x → C (g₁ x)) (z : C x) :
+    transport C (ap g₁ p) (f z) = f (transport C p z) :=
+  by induction p; reflexivity
 
 end eq open eq
 
 namespace nat
 
-  protected definition rec_down (P : ℕ → Type) (s : ℕ) (H0 : P s) (Hs : Πn, P (n+1) → P n) : P 0 :=
-  begin
-    induction s with s IH,
-    { exact H0 },
-    { exact IH (Hs s H0) }
-  end
-
-  definition rec_down_le (P : ℕ → Type) (s : ℕ) (H0 : Πn, s ≤ n → P n) (Hs : Πn, P (n+1) → P n)
-    : Πn, P n :=
-  begin
-    induction s with s IH: intro n,
-    { exact H0 n (zero_le n) },
-    { apply IH, intro n' H, induction H with n' H IH2, apply Hs, exact H0 _ !le.refl,
-      exact H0 _ (succ_le_succ H) }
-  end
-
-  definition rec_down_le_univ {P : ℕ → Type} {s : ℕ} {H0 : Π⦃n⦄, s ≤ n → P n}
-    {Hs : Π⦃n⦄, P (n+1) → P n} (Q : Π⦃n⦄, P n → P (n + 1) → Type)
-    (HQ0 : Πn (H : s ≤ n), Q (H0 H) (H0 (le.step H))) (HQs : Πn (p : P (n+1)), Q (Hs p) p) :
-    Πn, Q (rec_down_le P s H0 Hs n) (rec_down_le P s H0 Hs (n + 1)) :=
-  begin
-    induction s with s IH: intro n,
-    { apply HQ0 },
-    { apply IH, intro n' H, induction H with n' H IH2,
-      { esimp, apply HQs },
-      { apply HQ0 }}
-  end
-
-  definition rec_down_le_beta_ge (P : ℕ → Type) (s : ℕ) (H0 : Πn, s ≤ n → P n)
-    (Hs : Πn, P (n+1) → P n) (n : ℕ) (Hn : s ≤ n) : rec_down_le P s H0 Hs n = H0 n Hn :=
-  begin
-    revert n Hn, induction s with s IH: intro n Hn,
-    { exact ap (H0 n) !is_prop.elim },
-    { have Hn' : s ≤ n, from le.trans !self_le_succ Hn,
-      refine IH _ _ Hn' ⬝ _,
-      induction Hn' with n Hn' IH',
-      { exfalso, exact not_succ_le_self Hn },
-      { exact ap (H0 (succ n)) !is_prop.elim }}
-  end
-
-  definition rec_down_le_beta_lt (P : ℕ → Type) (s : ℕ) (H0 : Πn, s ≤ n → P n)
-    (Hs : Πn, P (n+1) → P n) (n : ℕ) (Hn : n < s) :
-    rec_down_le P s H0 Hs n = Hs n (rec_down_le P s H0 Hs (n+1)) :=
-  begin
-    revert n Hn, induction s with s IH: intro n Hn,
-    { exfalso, exact not_succ_le_zero n Hn },
-    { have Hn' : n ≤ s, from le_of_succ_le_succ Hn,
-      --esimp [rec_down_le],
-      exact sorry
-      -- induction Hn' with s Hn IH,
-      -- { },
-      -- { }
-}
-  end
-
-  /- this generalizes iterate_commute -/
-  definition iterate_hsquare {A B : Type} {f : A → A} {g : B → B}
-    (h : A → B) (p : hsquare f g h h) (n : ℕ) : hsquare (f^[n]) (g^[n]) h h :=
-  begin
-    induction n with n q,
-      exact homotopy.rfl,
-      exact q ⬝htyh p
-  end
-
-definition iterate_equiv2 {A : Type} {C : A → Type} (f : A → A) (h : Πa, C a ≃ C (f a))
-  (k : ℕ) (a : A) : C a ≃ C (f^[k] a) :=
-begin induction k with k IH, reflexivity, exact IH ⬝e h (f^[k] a) end
-
-
-
-  /- replace proof of le_of_succ_le by this -/
-  definition le_step_left {n m : ℕ} (H : succ n ≤ m) : n ≤ m :=
-  by induction H with H m H'; exact le_succ n; exact le.step H'
-
-  /- TODO: make proof of le_succ_of_le simpler -/
-
-  definition nat.add_le_add_left2 {n m : ℕ} (H : n ≤ m) (k : ℕ) : k + n ≤ k + m :=
-  by induction H with m H H₂; reflexivity; exact le.step H₂
+--   definition rec_down_le_beta_lt (P : ℕ → Type) (s : ℕ) (H0 : Πn, s ≤ n → P n)
+--     (Hs : Πn, P (n+1) → P n) (n : ℕ) (Hn : n < s) :
+--     rec_down_le P s H0 Hs n = Hs n (rec_down_le P s H0 Hs (n+1)) :=
+--   begin
+--     revert n Hn, induction s with s IH: intro n Hn,
+--     { exfalso, exact not_succ_le_zero n Hn },
+--     { have Hn' : n ≤ s, from le_of_succ_le_succ Hn,
+--       --esimp [rec_down_le],
+--       exact sorry
+--       -- induction Hn' with s Hn IH,
+--       -- { },
+--       -- { }
+-- }
+--   end
 
 end nat
 
-
-namespace trunc_index
-  open is_conn nat trunc is_trunc
-  lemma minus_two_add_plus_two (n : ℕ₋₂) : -2+2+n = n :=
-  by induction n with n p; reflexivity; exact ap succ p
-
-  protected definition of_nat_monotone {n k : ℕ} : n ≤ k → of_nat n ≤ of_nat k :=
-  begin
-    intro H, induction H with k H K,
-    { apply le.tr_refl },
-    { apply le.step K }
-  end
-
-  lemma add_plus_two_comm (n k : ℕ₋₂) : n +2+ k = k +2+ n :=
-  begin
-    induction n with n IH,
-    { exact minus_two_add_plus_two k },
-    { exact !succ_add_plus_two ⬝ ap succ IH}
-  end
-
-  lemma sub_one_add_plus_two_sub_one (n m : ℕ) : n.-1 +2+ m.-1 = of_nat (n + m) :=
-  begin
-    induction m with m IH,
-    { reflexivity },
-    { exact ap succ IH }
-  end
-
-end trunc_index
-
-namespace int
-
-  private definition maxm2_le.lemma₁ {n k : ℕ} : n+(1:int) + -[1+ k] ≤ n :=
-  le.intro (
-    calc n + 1 + -[1+ k] + k
-      = n + 1 + (-(k + 1)) + k : by reflexivity
-  ... = n + 1 + (- 1 - k) + k    : by krewrite (neg_add_rev k 1)
-  ... = n + 1 + (- 1 - k + k)    : add.assoc
-  ... = n + 1 + (- 1 + -k + k)   : by reflexivity
-  ... = n + 1 + (- 1 + (-k + k)) : add.assoc
-  ... = n + 1 + (- 1 + 0)        : add.left_inv
-  ... = n + (1 + (- 1 + 0))      : add.assoc
-  ... = n                       : int.add_zero)
-
-  private definition maxm2_le.lemma₂ {n : ℕ} {k : ℤ} : -[1+ n] + 1 + k ≤ k :=
-  le.intro (
-    calc -[1+ n] + 1 + k + n
-      = - (n + 1) + 1 + k + n : by reflexivity
-  ... = -n - 1 + 1 + k + n    : by rewrite (neg_add n 1)
-  ... = -n + (- 1 + 1) + k + n : by krewrite (int.add_assoc (-n) (- 1) 1)
-  ... = -n + 0 + k + n        : add.left_inv 1
-  ... = -n + k + n            : int.add_zero
-  ... = k + -n + n            : int.add_comm
-  ... = k + (-n + n)          : int.add_assoc
-  ... = k + 0                 : add.left_inv n
-  ... = k                     : int.add_zero)
-
-  open trunc_index
-  /-
-    The function from integers to truncation indices which sends
-    positive numbers to themselves, and negative numbers to negative
-    2. In particular -1 is sent to -2, but since we only work with
-    pointed types, that doesn't matter for us -/
-  definition maxm2 [unfold 1] : ℤ → ℕ₋₂ :=
-  λ n, int.cases_on n trunc_index.of_nat (λk, -2)
-
-  -- we also need the max -1 - function
-  definition maxm1 [unfold 1] : ℤ → ℕ₋₂ :=
-  λ n, int.cases_on n trunc_index.of_nat (λk, -1)
-
-  definition maxm2_le_maxm1 (n : ℤ) : maxm2 n ≤ maxm1 n :=
-  begin
-    induction n with n n,
-    { exact le.tr_refl n },
-    { exact minus_two_le -1 }
-  end
-
-  -- the is maxm1 minus 1
-  definition maxm1m1 [unfold 1] : ℤ → ℕ₋₂ :=
-  λ n, int.cases_on n (λ k, k.-1) (λ k, -2)
-
-  definition maxm1_eq_succ (n : ℤ) : maxm1 n = (maxm1m1 n).+1 :=
-  begin
-    induction n with n n,
-    { reflexivity },
-    { reflexivity }
-  end
-
-  definition maxm2_le_maxm0 (n : ℤ) : maxm2 n ≤ max0 n :=
-  begin
-    induction n with n n,
-    { exact le.tr_refl n },
-    { exact minus_two_le 0 }
-  end
-
-  definition max0_le_of_le {n : ℤ} {m : ℕ} (H : n ≤ of_nat m)
-    : nat.le (max0 n) m :=
-  begin
-    induction n with n n,
-    { exact le_of_of_nat_le_of_nat H },
-    { exact nat.zero_le m }
-  end
-
-  definition not_neg_succ_le_of_nat {n m : ℕ} : ¬m ≤ -[1+n] :=
-  by cases m: exact id
-
-  definition maxm2_monotone {n m : ℤ} (H : n ≤ m) : maxm2 n ≤ maxm2 m :=
-  begin
-    induction n with n n,
-    { induction m with m m,
-      { apply of_nat_le_of_nat, exact le_of_of_nat_le_of_nat H },
-      { exfalso, exact not_neg_succ_le_of_nat H }},
-    { apply minus_two_le }
-  end
-
-  definition sub_nat_le (n : ℤ) (m : ℕ) : n - m ≤ n :=
-  le.intro !sub_add_cancel
-
-  definition sub_nat_lt (n : ℤ) (m : ℕ) : n - m < n + 1 :=
-  add_le_add_right (sub_nat_le n m) 1
-
-  definition sub_one_le (n : ℤ) : n - 1 ≤ n :=
-  sub_nat_le n 1
-
-  definition le_add_nat (n : ℤ) (m : ℕ) : n ≤ n + m :=
-  le.intro rfl
-
-  definition le_add_one (n : ℤ) : n ≤ n + 1:=
-  le_add_nat n 1
-
-  open trunc_index
-
-  definition maxm2_le (n k : ℤ) : maxm2 (n+1+k) ≤ (maxm1m1 n).+1+2+(maxm1m1 k) :=
-  begin
-    rewrite [-(maxm1_eq_succ n)],
-    induction n with n n,
-    { induction k with k k,
-      { induction k with k IH,
-        { apply le.tr_refl },
-        { exact succ_le_succ IH } },
-      { exact trunc_index.le_trans (maxm2_monotone maxm2_le.lemma₁)
-                                   (maxm2_le_maxm1 n) } },
-    { krewrite (add_plus_two_comm -1 (maxm1m1 k)),
-      rewrite [-(maxm1_eq_succ k)],
-      exact trunc_index.le_trans (maxm2_monotone maxm2_le.lemma₂)
-                                 (maxm2_le_maxm1 k) }
-  end
-
-end int open int
-
-namespace pmap
-
-  /- rename: pmap_eta in namespace pointed -/
-  definition eta {A B : Type*} (f : A →* B) : pmap.mk f (respect_pt f) = f :=
-  begin induction f, reflexivity end
-
-end pmap
-
-namespace lift
-
-  definition is_trunc_plift [instance] [priority 1450] (A : Type*) (n : ℕ₋₂)
-    [H : is_trunc n A] : is_trunc n (plift A) :=
-  is_trunc_lift A n
-
-  definition lift_functor2 {A B C : Type} (f : A → B → C) (x : lift A) (y : lift B) : lift C :=
-  up (f (down x) (down y))
-
-end lift
-
   -- definition ppi_eq_equiv_internal : (k = l) ≃ (k ~* l) :=
   --   calc (k = l) ≃ ppi.sigma_char P p₀ k = ppi.sigma_char P p₀ l
   --                  : eq_equiv_fn_eq (ppi.sigma_char P p₀) k l
@@ -639,211 +77,101 @@ end lift
 namespace pointed
 /- move to pointed -/
 open sigma.ops
-definition pType.sigma_char' [constructor] : pType.{u} ≃ Σ(X : Type.{u}), X :=
-begin
-  fapply equiv.MK,
-  { intro X, exact ⟨X, pt⟩ },
-  { intro X, exact pointed.MK X.1 X.2 },
-  { intro x, induction x with X x, reflexivity },
-  { intro x, induction x with X x, reflexivity },
-end
 
-definition ap_equiv_eq {X Y : Type} {e e' : X ≃ Y} (p : e ~ e') (x : X) :
-  ap (λ(e : X ≃ Y), e x) (equiv_eq p) = p x :=
-begin
-  cases e with e He, cases e' with e' He', esimp at *, esimp [equiv_eq],
-  refine homotopy.rec_on' p _, intro q, induction q, esimp [equiv_eq', equiv_mk_eq],
-  assert H : He = He', apply is_prop.elim, induction H, rewrite [is_prop_elimo_self]
-end
-
-definition pequiv.sigma_char_equiv [constructor] (X Y : Type*) :
-  (X ≃* Y) ≃ Σ(e : X ≃ Y), e pt = pt :=
-begin
-  fapply equiv.MK,
-  { intro e, exact ⟨equiv_of_pequiv e, respect_pt e⟩ },
-  { intro e, exact pequiv_of_equiv e.1 e.2 },
-  { intro e, induction e with e p, fapply sigma_eq,
-    apply equiv_eq, reflexivity, esimp,
-    apply eq_pathover_constant_right, esimp,
-    refine _ ⬝ph vrfl,
-    apply ap_equiv_eq },
-  { intro e, apply pequiv_eq, fapply phomotopy.mk, intro x, reflexivity,
-    refine !idp_con ⬝ _, reflexivity },
-end
-
-definition pequiv.sigma_char_pmap [constructor] (X Y : Type*) :
-  (X ≃* Y) ≃ Σ(f : X →* Y), is_equiv f :=
-begin
-  fapply equiv.MK,
-  { intro e, exact ⟨ pequiv.to_pmap e , pequiv.to_is_equiv e ⟩ },
-  { intro w, exact pequiv_of_pmap w.1 w.2 },
-  { intro w, induction w with f p, fapply sigma_eq,
-    { reflexivity }, { apply is_prop.elimo } },
-  { intro e, apply pequiv_eq, fapply phomotopy.mk,
-    { intro x, reflexivity },
-    { refine !idp_con ⬝ _, reflexivity } }
-end
-
-definition pType_eq_equiv (X Y : Type*) : (X = Y) ≃ (X ≃* Y) :=
-begin
-  refine eq_equiv_fn_eq pType.sigma_char' X Y ⬝e !sigma_eq_equiv ⬝e _, esimp,
-  transitivity Σ(p : X = Y), cast p pt = pt,
-  apply sigma_equiv_sigma_right, intro p, apply pathover_equiv_tr_eq,
-  transitivity Σ(e : X ≃ Y), e pt = pt,
-  refine sigma_equiv_sigma (eq_equiv_equiv X Y) (λp, equiv.rfl),
-  exact (pequiv.sigma_char_equiv X Y)⁻¹ᵉ
-end
 
 end pointed open pointed
 
 namespace trunc
   open trunc_index sigma.ops
 
-definition ptrunctype.sigma_char [constructor] (n : ℕ₋₂) :
-  n-Type* ≃ Σ(X : Type*), is_trunc n X :=
-equiv.MK (λX, ⟨ptrunctype.to_pType X, _⟩)
-         (λX, ptrunctype.mk (carrier X.1) X.2 pt)
-         begin intro X, induction X with X HX, induction X, reflexivity end
-         begin intro X, induction X, reflexivity end
+  -- TODO: redefine loopn_ptrunc_pequiv
+  definition apn_ptrunc_functor (n : ℕ₋₂) (k : ℕ) {A B : Type*} (f : A →* B) :
+    Ω→[k] (ptrunc_functor (n+k) f) ∘* (loopn_ptrunc_pequiv n k A)⁻¹ᵉ* ~*
+    (loopn_ptrunc_pequiv n k B)⁻¹ᵉ* ∘* ptrunc_functor n (Ω→[k] f) :=
+  begin
+    revert n, induction k with k IH: intro n,
+    { reflexivity },
+    { exact sorry }
+  end
 
-definition is_embedding_ptrunctype_to_pType (n : ℕ₋₂) : is_embedding (@ptrunctype.to_pType n) :=
-begin
-  intro X Y, fapply is_equiv_of_equiv_of_homotopy,
-  { exact eq_equiv_fn_eq (ptrunctype.sigma_char n) _ _ ⬝e subtype_eq_equiv _ _ },
-  intro p, induction p, reflexivity
-end
+  definition ptrunctype.sigma_char [constructor] (n : ℕ₋₂) :
+    n-Type* ≃ Σ(X : Type*), is_trunc n X :=
+  equiv.MK (λX, ⟨ptrunctype.to_pType X, _⟩)
+           (λX, ptrunctype.mk (carrier X.1) X.2 pt)
+           begin intro X, induction X with X HX, induction X, reflexivity end
+           begin intro X, induction X, reflexivity end
 
-definition ptrunctype_eq_equiv {n : ℕ₋₂} (X Y : n-Type*) : (X = Y) ≃ (X ≃* Y) :=
-equiv.mk _ (is_embedding_ptrunctype_to_pType n X Y) ⬝e pType_eq_equiv X Y
+  definition is_embedding_ptrunctype_to_pType (n : ℕ₋₂) : is_embedding (@ptrunctype.to_pType n) :=
+  begin
+    intro X Y, fapply is_equiv_of_equiv_of_homotopy,
+    { exact eq_equiv_fn_eq (ptrunctype.sigma_char n) _ _ ⬝e subtype_eq_equiv _ _ },
+    intro p, induction p, reflexivity
+  end
 
-/- replace trunc_trunc_equiv_left by this -/
-definition trunc_trunc_equiv_left' [constructor] (A : Type) {n m : ℕ₋₂} (H : n ≤ m)
-  : trunc n (trunc m A) ≃ trunc n A :=
-begin
-  note H2 := is_trunc_of_le (trunc n A) H,
-  fapply equiv.MK,
-  { intro x, induction x with x, induction x with x, exact tr x },
-  { exact trunc_functor n tr },
-  { intro x, induction x with x, reflexivity},
-  { intro x, induction x with x, induction x with x, reflexivity}
-end
+  definition ptrunctype_eq_equiv {n : ℕ₋₂} (X Y : n-Type*) : (X = Y) ≃ (X ≃* Y) :=
+  equiv.mk _ (is_embedding_ptrunctype_to_pType n X Y) ⬝e pType_eq_equiv X Y
 
-definition is_equiv_ptrunc_functor_ptr [constructor] (A : Type*) {n m : ℕ₋₂} (H : n ≤ m)
-  : is_equiv (ptrunc_functor n (ptr m A)) :=
-to_is_equiv (trunc_trunc_equiv_left' A H)⁻¹ᵉ
+  definition Prop_eq {P Q : Prop} (H : P ↔ Q) : P = Q :=
+  tua (equiv_of_is_prop (iff.mp H) (iff.mpr H))
 
-definition Prop_eq {P Q : Prop} (H : P ↔ Q) : P = Q :=
-tua (equiv_of_is_prop (iff.mp H) (iff.mpr H))
+  definition is_trunc_ptrunc_of_is_trunc [instance] [priority 500] (A : Type*)
+    (n m : ℕ₋₂) [H : is_trunc n A] : is_trunc n (ptrunc m A) :=
+  is_trunc_trunc_of_is_trunc A n m
 
-definition trunc_index_equiv_nat [constructor] : ℕ₋₂ ≃ ℕ :=
-equiv.MK add_two sub_two add_two_sub_two sub_two_add_two
+  definition ptrunc_pequiv_ptrunc_of_is_trunc {n m k : ℕ₋₂} {A : Type*}
+    (H1 : n ≤ m) (H2 : n ≤ k) (H : is_trunc n A) : ptrunc m A ≃* ptrunc k A :=
+  have is_trunc m A, from is_trunc_of_le A H1,
+  have is_trunc k A, from is_trunc_of_le A H2,
+  pequiv.MK (ptrunc.elim _ (ptr k A)) (ptrunc.elim _ (ptr m A))
+    abstract begin
+      refine !ptrunc_elim_pcompose⁻¹* ⬝* _,
+      exact ptrunc_elim_phomotopy _ !ptrunc_elim_ptr ⬝* !ptrunc_elim_ptr_phomotopy_pid,
+    end end
+    abstract begin
+      refine !ptrunc_elim_pcompose⁻¹* ⬝* _,
+      exact ptrunc_elim_phomotopy _ !ptrunc_elim_ptr ⬝* !ptrunc_elim_ptr_phomotopy_pid,
+    end end
 
-definition is_set_trunc_index [instance] : is_set ℕ₋₂ :=
-is_trunc_equiv_closed_rev 0 trunc_index_equiv_nat
+  definition ptrunc_change_index {k l : ℕ₋₂} (p : k = l) (X : Type*)
+    : ptrunc k X ≃* ptrunc l X :=
+  pequiv_ap (λ n, ptrunc n X) p
 
-definition is_contr_ptrunc_minus_one (A : Type*) : is_contr (ptrunc -1 A) :=
-is_contr_of_inhabited_prop pt
+  definition ptrunc_functor_le {k l : ℕ₋₂} (p : l ≤ k) (X : Type*)
+    : ptrunc k X →* ptrunc l X :=
+  have is_trunc k (ptrunc l X), from is_trunc_of_le _ p,
+  ptrunc.elim _ (ptr l X)
 
--- TODO: redefine loopn_ptrunc_pequiv
-definition apn_ptrunc_functor (n : ℕ₋₂) (k : ℕ) {A B : Type*} (f : A →* B) :
-  Ω→[k] (ptrunc_functor (n+k) f) ∘* (loopn_ptrunc_pequiv n k A)⁻¹ᵉ* ~*
-  (loopn_ptrunc_pequiv n k B)⁻¹ᵉ* ∘* ptrunc_functor n (Ω→[k] f) :=
-begin
-  revert n, induction k with k IH: intro n,
-  { reflexivity },
-  { exact sorry }
-end
+  definition trunc_index.pred [unfold 1] (n : ℕ₋₂) : ℕ₋₂ :=
+  begin cases n with n, exact -2, exact n end
 
-definition ptrunc_pequiv_natural [constructor] (n : ℕ₋₂) {A B : Type*} (f : A →* B) [is_trunc n A]
-  [is_trunc n B] : f ∘* ptrunc_pequiv n A ~* ptrunc_pequiv n B ∘* ptrunc_functor n f :=
-begin
-  fapply phomotopy.mk,
-  { intro a, induction a with a, reflexivity },
-  { refine !idp_con ⬝ _ ⬝ !idp_con⁻¹, refine !ap_compose'⁻¹ ⬝ _, apply ap_id }
-end
+  /- A more general version of ptrunc_elim_phomotopy, where the proofs of truncatedness might be different -/
+  definition ptrunc_elim_phomotopy2 [constructor] (k : ℕ₋₂) {A B : Type*} {f g : A →* B} (H₁ : is_trunc k B)
+    (H₂ : is_trunc k B) (p : f ~* g) : @ptrunc.elim k A B H₁ f ~* @ptrunc.elim k A B H₂ g :=
+  begin
+    fapply phomotopy.mk,
+    { intro x, induction x with a, exact p a },
+    { exact to_homotopy_pt p }
+  end
 
-definition ptr_natural [constructor] (n : ℕ₋₂) {A B : Type*} (f : A →* B) :
-  ptrunc_functor n f ∘* ptr n A ~* ptr n B ∘* f :=
-begin
-  fapply phomotopy.mk,
-  { intro a, reflexivity },
-  { reflexivity }
-end
+  definition pmap_ptrunc_equiv [constructor] (n : ℕ₋₂) (A B : Type*) [H : is_trunc n B] :
+    (ptrunc n A →* B) ≃ (A →* B) :=
+  begin
+    fapply equiv.MK,
+    { intro g, exact g ∘* ptr n A },
+    { exact ptrunc.elim n },
+    { intro f, apply eq_of_phomotopy, apply ptrunc_elim_ptr },
+    { intro g, apply eq_of_phomotopy,
+      exact ptrunc_elim_pcompose n g (ptr n A) ⬝* pwhisker_left g (ptrunc_elim_ptr_phomotopy_pid n A) ⬝*
+        pcompose_pid g }
+  end
 
-definition ptrunc_elim_pcompose (n : ℕ₋₂) {A B C : Type*} (g : B →* C) (f : A →* B) [is_trunc n B]
-  [is_trunc n C] : ptrunc.elim n (g ∘* f) ~* g ∘* ptrunc.elim n f :=
-begin
-  fapply phomotopy.mk,
-  { intro a, induction a with a, reflexivity },
-  { apply idp_con }
-end
+  definition pmap_ptrunc_pequiv [constructor] (n : ℕ₋₂) (A B : Type*) [H : is_trunc n B] :
+    ppmap (ptrunc n A) B ≃* ppmap A B :=
+  pequiv_of_equiv (pmap_ptrunc_equiv n A B) (eq_of_phomotopy (pconst_pcompose (ptr n A)))
 
-definition ptrunc_elim_ptr_phomotopy_pid (n : ℕ₋₂) (A : Type*):
-  ptrunc.elim n (ptr n A) ~* pid (ptrunc n A) :=
-begin
-  fapply phomotopy.mk,
-  { intro a, induction a with a, reflexivity },
-  { apply idp_con }
-end
-
-definition is_trunc_ptrunc_of_is_trunc [instance] [priority 500] (A : Type*)
-  (n m : ℕ₋₂) [H : is_trunc n A] : is_trunc n (ptrunc m A) :=
-is_trunc_trunc_of_is_trunc A n m
-
-definition ptrunc_pequiv_ptrunc_of_is_trunc {n m k : ℕ₋₂} {A : Type*}
-  (H1 : n ≤ m) (H2 : n ≤ k) (H : is_trunc n A) : ptrunc m A ≃* ptrunc k A :=
-have is_trunc m A, from is_trunc_of_le A H1,
-have is_trunc k A, from is_trunc_of_le A H2,
-pequiv.MK (ptrunc.elim _ (ptr k A)) (ptrunc.elim _ (ptr m A))
-  abstract begin
-    refine !ptrunc_elim_pcompose⁻¹* ⬝* _,
-    exact ptrunc_elim_phomotopy _ !ptrunc_elim_ptr ⬝* !ptrunc_elim_ptr_phomotopy_pid,
-  end end
-  abstract begin
-    refine !ptrunc_elim_pcompose⁻¹* ⬝* _,
-    exact ptrunc_elim_phomotopy _ !ptrunc_elim_ptr ⬝* !ptrunc_elim_ptr_phomotopy_pid,
-  end end
-
-definition ptrunc_change_index {k l : ℕ₋₂} (p : k = l) (X : Type*)
-  : ptrunc k X ≃* ptrunc l X :=
-pequiv_ap (λ n, ptrunc n X) p
-
-definition ptrunc_functor_le {k l : ℕ₋₂} (p : l ≤ k) (X : Type*)
-  : ptrunc k X →* ptrunc l X :=
-have is_trunc k (ptrunc l X), from is_trunc_of_le _ p,
-ptrunc.elim _ (ptr l X)
-
-definition trunc_index.pred [unfold 1] (n : ℕ₋₂) : ℕ₋₂ :=
-begin cases n with n, exact -2, exact n end
-
-/- A more general version of ptrunc_elim_phomotopy, where the proofs of truncatedness might be different -/
-definition ptrunc_elim_phomotopy2 [constructor] (k : ℕ₋₂) {A B : Type*} {f g : A →* B} (H₁ : is_trunc k B)
-  (H₂ : is_trunc k B) (p : f ~* g) : @ptrunc.elim k A B H₁ f ~* @ptrunc.elim k A B H₂ g :=
-begin
-  fapply phomotopy.mk,
-  { intro x, induction x with a, exact p a },
-  { exact to_homotopy_pt p }
-end
-
-definition pmap_ptrunc_equiv [constructor] (n : ℕ₋₂) (A B : Type*) [H : is_trunc n B] :
-  (ptrunc n A →* B) ≃ (A →* B) :=
-begin
-  fapply equiv.MK,
-  { intro g, exact g ∘* ptr n A },
-  { exact ptrunc.elim n },
-  { intro f, apply eq_of_phomotopy, apply ptrunc_elim_ptr },
-  { intro g, apply eq_of_phomotopy,
-    exact ptrunc_elim_pcompose n g (ptr n A) ⬝* pwhisker_left g (ptrunc_elim_ptr_phomotopy_pid n A) ⬝*
-      pcompose_pid g }
-end
-
-definition pmap_ptrunc_pequiv [constructor] (n : ℕ₋₂) (A B : Type*) [H : is_trunc n B] :
-  ppmap (ptrunc n A) B ≃* ppmap A B :=
-pequiv_of_equiv (pmap_ptrunc_equiv n A B) (eq_of_phomotopy (pconst_pcompose (ptr n A)))
-
-definition loopn_ptrunc_pequiv_nat (n : ℕ) (k : ℕ) (A : Type*) :
-  Ω[k] (ptrunc (n+k) A) ≃* ptrunc n (Ω[k] A) :=
-loopn_pequiv_loopn k (ptrunc_change_index (of_nat_add_of_nat n k)⁻¹ A) ⬝e* loopn_ptrunc_pequiv n k A
+  definition loopn_ptrunc_pequiv_nat (n : ℕ) (k : ℕ) (A : Type*) :
+    Ω[k] (ptrunc (n+k) A) ≃* ptrunc n (Ω[k] A) :=
+  loopn_pequiv_loopn k (ptrunc_change_index (of_nat_add_of_nat n k)⁻¹ A) ⬝e* loopn_ptrunc_pequiv n k A
 
 end trunc open trunc
 
@@ -886,6 +214,45 @@ namespace is_trunc
     (H2 : is_conn (m.-1) A) : is_trunc m A :=
   is_trunc_of_is_trunc_loopn m 0 A H H2
 
+  definition is_trunc_of_trivial_homotopy {n : ℕ} {m : ℕ₋₂} {A : Type} (H : is_trunc m A)
+    (H2 : Πk a, k > n → is_contr (π[k] (pointed.MK A a))) : is_trunc n A :=
+  begin
+    fapply is_trunc_is_equiv_closed_rev, { exact @tr n A },
+    apply whitehead_principle m,
+    { apply is_equiv_trunc_functor_of_is_conn_fun,
+      note z := is_conn_fun_tr n A,
+      apply is_conn_fun_of_le _ (of_nat_le_of_nat (zero_le n)), },
+    intro a k,
+    apply @nat.lt_ge_by_cases n (k+1),
+    { intro H3, apply @is_equiv_of_is_contr, exact H2 _ _ H3,
+      refine @trivial_homotopy_group_of_is_trunc _ _ _ _ H3, apply is_trunc_trunc },
+    { intro H3, apply @(is_equiv_π_of_is_connected _ H3), apply is_conn_fun_tr }
+  end
+
+  definition is_trunc_of_trivial_homotopy_pointed {n : ℕ} {m : ℕ₋₂} {A : Type*} (H : is_trunc m A)
+    (Hconn : is_conn 0 A) (H2 : Πk, k > n → is_contr (π[k] A)) : is_trunc n A :=
+  begin
+    apply is_trunc_of_trivial_homotopy H,
+    intro k a H3, revert a, apply is_conn.elim -1,
+    cases A with A a₀, exact H2 k H3
+  end
+
+  definition is_trunc_of_is_trunc_succ {n : ℕ} {A : Type} (H : is_trunc (n.+1) A)
+    (H2 : Πa, is_contr (π[n+1] (pointed.MK A a))) : is_trunc n A :=
+  begin
+    apply is_trunc_of_trivial_homotopy H,
+    intro k a H3, induction H3 with k H3 IH, exact H2 a,
+    apply @trivial_homotopy_group_of_is_trunc _ (n+1) _ H, exact succ_le_succ H3
+  end
+
+  definition is_trunc_of_is_trunc_succ_pointed {n : ℕ} {A : Type*} (H : is_trunc (n.+1) A)
+    (Hconn : is_conn 0 A) (H2 : is_contr (π[n+1] A)) : is_trunc n A :=
+  begin
+    apply is_trunc_of_trivial_homotopy_pointed H Hconn,
+    intro k H3, induction H3 with k H3 IH, exact H2,
+    apply @trivial_homotopy_group_of_is_trunc _ (n+1) _ H, exact succ_le_succ H3
+  end
+
 end is_trunc
 namespace sigma
   open sigma.ops
@@ -1383,11 +750,30 @@ begin
   induction p2, induction p1, induction r₃, reflexivity
 end
 
-definition fiber_eq_equiv' [constructor] {A B : Type} {f : A → B} {b : B} (x y : fiber f b)
-  : (x = y) ≃ (Σ(p : point x = point y), point_eq x = ap f p ⬝ point_eq y) :=
+definition fiber_eq_equiv' [constructor] {A B : Type} {f : A → B} {b : B} (x y : fiber f b) :
+  (x = y) ≃ (Σ(p : point x = point y), point_eq x = ap f p ⬝ point_eq y) :=
 @equiv_change_inv _ _ (fiber_eq_equiv x y) (λpq, fiber_eq pq.1 pq.2)
   begin intro pq, cases pq, reflexivity end
 
+definition fiber_eq2_equiv {A B : Type} {f : A → B} {b : B} {x y : fiber f b}
+  (p₁ p₂ : point x = point y) (q₁ : point_eq x = ap f p₁ ⬝ point_eq y)
+  (q₂ : point_eq x = ap f p₂ ⬝ point_eq y) : (fiber_eq p₁ q₁ = fiber_eq p₂ q₂) ≃
+  (Σ(r : p₁ = p₂), q₁ ⬝ whisker_right (point_eq y) (ap02 f r) = q₂) :=
+begin
+  refine (eq_equiv_fn_eq_of_equiv (fiber_eq_equiv' x y)⁻¹ᵉ _ _)⁻¹ᵉ ⬝e sigma_eq_equiv _ _ ⬝e _,
+  apply sigma_equiv_sigma_right, esimp, intro r,
+  refine !eq_pathover_equiv_square ⬝e _,
+  refine eq_hconcat_equiv !ap_constant ⬝e hconcat_eq_equiv (ap_compose (λx, x ⬝ _) _ _) ⬝e _,
+  refine !square_equiv_eq ⬝e _,
+  exact eq_equiv_eq_closed idp (idp_con q₂)
+end
+
+definition fiber_eq2 {A B : Type} {f : A → B} {b : B} {x y : fiber f b}
+  {p₁ p₂ : point x = point y} {q₁ : point_eq x = ap f p₁ ⬝ point_eq y}
+  {q₂ : point_eq x = ap f p₂ ⬝ point_eq y} (r : p₁ = p₂)
+  (s : q₁ ⬝ whisker_right (point_eq y) (ap02 f r) = q₂) : (fiber_eq p₁ q₁ = fiber_eq p₂ q₂) :=
+(fiber_eq2_equiv p₁ p₂ q₁ q₂)⁻¹ᵉ ⟨r, s⟩
+
 definition is_contr_pfiber_pid (A : Type*) : is_contr (pfiber (pid A)) :=
 is_contr.mk pt begin intro x, induction x with a p, esimp at p, cases p, reflexivity end
 
@@ -1522,6 +908,18 @@ namespace function
     exact sorry
   end
 
+  definition is_embedding_of_square {A B C D : Type} {f : A → B} {g : C → D} (h : A ≃ C)
+    (k : B ≃ D) (s : k ∘ f ~ g ∘ h) (Hf : is_embedding f) : is_embedding g :=
+  begin
+    apply is_embedding_homotopy_closed, exact inv_homotopy_of_homotopy_pre _ _ _ s,
+    apply is_embedding_compose, apply is_embedding_compose,
+    apply is_embedding_of_is_equiv, exact Hf, apply is_embedding_of_is_equiv
+  end
+
+  definition is_embedding_of_square_rev {A B C D : Type} {f : A → B} {g : C → D} (h : A ≃ C)
+    (k : B ≃ D) (s : k ∘ f ~ g ∘ h) (Hg : is_embedding g) : is_embedding f :=
+  is_embedding_of_square h⁻¹ᵉ k⁻¹ᵉ s⁻¹ʰᵗʸᵛ Hg
+
 end function open function
 
 namespace is_conn
@@ -1970,6 +1368,9 @@ namespace prod
   infix ` ×→ `:63 := prod_functor
   infix ` ×≃ `:63 := prod_equiv_prod
 
+  definition pprod_incl1 [constructor] (X Y : Type*) : X →* X ×* Y := pmap.mk (λx, (x, pt)) idp
+  definition pprod_incl2 [constructor] (X Y : Type*) : Y →* X ×* Y := pmap.mk (λy, (pt, y)) idp
+
 end prod
 
 namespace equiv
@@ -2118,6 +1519,17 @@ end
 
 end list
 
+namespace chain_complex
+
+open fin
+definition LES_is_contr_of_is_embedding_of_is_surjective (n : ℕ) {X Y : pType.{u}} (f : X →* Y)
+  (H : is_embedding (π→[n] f)) (H2 : is_surjective (π→[n+1] f)) : is_contr (π[n] (pfiber f)) :=
+begin
+  rexact @is_contr_of_is_embedding_of_is_surjective +3ℕ (LES_of_homotopy_groups f) (n, 0)
+    (is_exact_LES_of_homotopy_groups f _) proof H qed proof H2 qed
+end
+
+end chain_complex
 
 namespace susp
 open trunc_index
diff --git a/pointed.hlean b/pointed.hlean
index fd5b27f..a0b9d2b 100644
--- a/pointed.hlean
+++ b/pointed.hlean
@@ -606,5 +606,31 @@ definition ap1_gen_idp_eq {A B : Type} (f : A → B) {a : A} (q : f a = f a) (r
   ap1_gen_idp f q = ap (λx, ap1_gen f x x idp) r :=
 begin cases r, reflexivity end
 
+definition pointed_change_point [constructor] (A : Type*) {a : A} (p : a = pt) :
+  pointed.MK A a ≃* A :=
+pequiv_of_eq_pt p ⬝e* (pointed_eta_pequiv A)⁻¹ᵉ*
+
+definition change_path_psquare {A B : Type*} (f : A →* B)
+  {a' : A} {b' : B} (p : a' = pt) (q : pt = b') :
+  psquare (pointed_change_point _ p)
+          (pointed_change_point _ q⁻¹)
+          (pmap.mk f (ap f p ⬝ respect_pt f ⬝ q)) f :=
+begin
+  fapply phomotopy.mk, exact homotopy.rfl,
+  exact !idp_con ⬝ !ap_id ◾ !ap_id ⬝ !con_inv_cancel_right ⬝ whisker_right _ (ap02 f !ap_id⁻¹)
+end
+
+definition change_path_psquare_cod {A B : Type*} (f : A →* B) {b' : B} (p : pt = b') :
+  f ~* pointed_change_point _ p⁻¹ ∘* pmap.mk f (respect_pt f ⬝ p) :=
+begin
+  fapply phomotopy.mk, exact homotopy.rfl, exact !idp_con ⬝ !ap_id ◾ !ap_id ⬝ !con_inv_cancel_right
+end
+
+definition change_path_psquare_cod' {A B : Type} (f : A → B) (a : A) {b' : B} (p : f a = b') :
+  pointed_change_point _ p ∘* pmap_of_map f a ~* pmap.mk f p :=
+begin
+  fapply phomotopy.mk, exact homotopy.rfl, refine whisker_left idp (ap_id p)⁻¹
+end
+
 
 end pointed