move definitions from spectral repository here

hott/algebra/category/constructions/rezk.hlean

@@ -157,7 +157,7 @@ namespace rezk
     --induction b using rezk.rec with b' b' b g, --why does this not work if it works below?
     refine @rezk.rec _ _ _ (rezk_hom_left_pth_1_trunc a a' f) _ _ _ b,
     intro b, apply equiv_precompose (to_hom f⁻¹ⁱ), --how do i unfold properly at this point?
-    { intro b b' g, apply equiv_pathover, intro g' g'' H,
+    { intro b b' g, apply equiv_pathover2, intro g' g'' H,
       refine !pathover_rezk_hom_left_pt ⬝op _,
       refine !assoc ⬝ ap (λ x, x ∘ _) _,  refine eq_of_parallel_po_right _ H,
       apply pathover_rezk_hom_left_pt },

hott/algebra/group_theory.hlean

@@ -6,7 +6,7 @@ Authors: Floris van Doorn
 Basic group theory
 -/
 
-import algebra.category.category algebra.bundled .homomorphism
+import algebra.category.category algebra.bundled .homomorphism types.pointed2
 
 open eq algebra pointed function is_trunc pi equiv is_equiv
 set_option class.force_new true
@@ -590,5 +590,14 @@ 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)
 
+  definition pequiv_of_isomorphism_of_eq {G₁ G₂ : Group} (p : G₁ = G₂) :
+    pequiv_of_isomorphism (isomorphism_of_eq p) = pequiv_of_eq (ap pType_of_Group p) :=
+  begin
+    induction p,
+    apply pequiv_eq,
+    fapply phomotopy.mk,
+    { intro g, reflexivity },
+    { apply is_prop.elim }
+  end
 
 end group

hott/algebra/homotopy_group.hlean

@@ -11,7 +11,6 @@ import .trunc_group types.trunc .group_theory types.nat.hott
 open nat eq pointed trunc is_trunc algebra group function equiv unit is_equiv nat
 
 -- TODO: consistently make n an argument before A
--- TODO: rename cghomotopy_group to aghomotopy_group
 -- TODO: rename homotopy_group_functor_compose to homotopy_group_functor_pcompose
 namespace eq
 
@@ -60,14 +59,14 @@ namespace eq
   definition ghomotopy_group [constructor] (n : ℕ) [is_succ n] (A : Type*) : Group :=
   Group.mk (π[n] A) _
 
-  definition cghomotopy_group [constructor] (n : ℕ) [is_at_least_two n] (A : Type*) : AbGroup :=
+  definition aghomotopy_group [constructor] (n : ℕ) [is_at_least_two n] (A : Type*) : AbGroup :=
   AbGroup.mk (π[n] A) _
 
   definition fundamental_group [constructor] (A : Type*) : Group :=
   ghomotopy_group 1 A
 
   notation `πg[`:95  n:0 `]`:0 := ghomotopy_group n
-  notation `πag[`:95 n:0 `]`:0 := cghomotopy_group n
+  notation `πag[`:95 n:0 `]`:0 := aghomotopy_group n
 
   notation `π₁` := fundamental_group -- should this be notation for the group or pointed type?
 
@@ -163,7 +162,7 @@ namespace eq
     [is_equiv f] : is_equiv (π→[n] f) :=
   @(is_equiv_trunc_functor 0 _) !is_equiv_apn
 
-  definition homotopy_group_functor_succ_phomotopy_in (n : ℕ) {A B : Type*} (f : A →* B) :
+  definition homotopy_group_succ_in_natural (n : ℕ) {A B : Type*} (f : A →* B) :
     homotopy_group_succ_in B n ∘* π→[n + 1] f ~*
     π→[n] (Ω→ f) ∘* homotopy_group_succ_in A n :=
   begin
@@ -171,11 +170,15 @@ namespace eq
     exact ptrunc_functor_phomotopy 0 (apn_succ_phomotopy_in n f)
   end
 
+  definition homotopy_group_succ_in_natural_unpointed (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)) :=
+  (homotopy_group_succ_in_natural n f)⁻¹*
+
   definition is_equiv_homotopy_group_functor_ap1 (n : ℕ) {A B : Type*} (f : A →* B)
     [is_equiv (π→[n + 1] f)] : is_equiv (π→[n] (Ω→ f)) :=
   have is_equiv (π→[n] (Ω→ f) ∘ homotopy_group_succ_in A n),
   from is_equiv_of_equiv_of_homotopy (equiv.mk (π→[n+1] f) _ ⬝e homotopy_group_succ_in B n)
-                                     (homotopy_group_functor_succ_phomotopy_in n f),
+                                     (homotopy_group_succ_in_natural n f),
   is_equiv.cancel_right (homotopy_group_succ_in A n) _
 
   definition tinverse [constructor] {X : Type*} : π[1] X →* π[1] X :=
@@ -275,10 +278,39 @@ namespace eq
       apply homotopy_group_pequiv_loop_ptrunc_con}
   end
 
+  lemma ghomotopy_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 ghomotopy_group_ptrunc [constructor] (k : ℕ) [is_succ k] (A : Type*) :
     πg[k] (ptrunc k A) ≃g πg[k] A :=
   ghomotopy_group_ptrunc_of_le (le.refl k) A
 
+  section psquare
+  variables {A₀₀ A₂₀ A₀₂ A₂₂ : Type*}
+            {f₁₀ : A₀₀ →* A₂₀} {f₁₂ : A₀₂ →* A₂₂}
+            {f₀₁ : A₀₀ →* A₀₂} {f₂₁ : A₂₀ →* A₂₂}
+
+  definition homotopy_group_functor_psquare (n : ℕ) (p : psquare f₁₀ f₁₂ f₀₁ f₂₁) :
+        psquare (π→[n] f₁₀) (π→[n] f₁₂) (π→[n] f₀₁) (π→[n] f₂₁) :=
+  !homotopy_group_functor_compose⁻¹* ⬝* homotopy_group_functor_phomotopy n p ⬝*
+  !homotopy_group_functor_compose
+
+  definition homotopy_group_homomorphism_psquare (n : ℕ) [H : is_succ n]
+    (p : psquare f₁₀ f₁₂ f₀₁ f₂₁) : hsquare (π→g[n] f₁₀) (π→g[n] f₁₂) (π→g[n] f₀₁) (π→g[n] f₂₁) :=
+  begin
+    induction H with n, exact to_homotopy (ptrunc_functor_psquare 0 (apn_psquare (succ n) p))
+  end
+
+  end psquare
+
   /- some homomorphisms -/
 
   -- definition is_homomorphism_cast_loopn_succ_eq_in {A : Type*} (n : ℕ) :

hott/algebra/inf_group.hlean

@@ -582,6 +582,10 @@ section add_ab_inf_group
 
   theorem neg_neg_sub_neg (a b : A) : - (-a - -b) = a - b :=
     by rewrite [neg_sub, sub_neg_eq_add, neg_add_eq_sub]
+
+  definition add_sub_cancel_middle (a b : A) : a + (b - a) = b :=
+  !add.comm ⬝ !sub_add_cancel
+
 end add_ab_inf_group
 
 definition inf_group_of_add_inf_group (A : Type) [G : add_inf_group A] : inf_group A :=

hott/arity.hlean

@@ -51,6 +51,22 @@ namespace eq
   infix ` ~2 `:50 := homotopy2
   infix ` ~3 `:50 := homotopy3
 
+  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 ap0111 (f : U → V → W → X) (Hu : u = u') (Hv : v = v') (Hw : w = w')
       : f u v w = f u' v' w' :=
   by cases Hu; congruence; repeat assumption
@@ -70,13 +86,13 @@ namespace eq
       : f u v w x y z = f u' v' w' x' y' z' :=
   by cases Hu; congruence; repeat assumption
 
-  definition ap010 (f : X → Πa, B a) (Hx : x = x') : f x ~ f x' :=
+  definition ap010 [unfold 7] (f : X → Πa, B a) (Hx : x = x') : f x ~ f x' :=
   by intros; cases Hx; reflexivity
 
-  definition ap0100 (f : X → Πa b, C a b) (Hx : x = x') : f x ~2 f x' :=
+  definition ap0100 [unfold 8] (f : X → Πa b, C a b) (Hx : x = x') : f x ~2 f x' :=
   by intros; cases Hx; reflexivity
 
-  definition ap01000 (f : X → Πa b c, D a b c) (Hx : x = x') : f x ~3 f x' :=
+  definition ap01000 [unfold 9] (f : X → Πa b c, D a b c) (Hx : x = x') : f x ~3 f x' :=
   by intros; cases Hx; reflexivity
 
   definition apdt011 (f : Πa, B a → Z) (Ha : a = a') (Hb : transport B Ha b = b')
@@ -189,6 +205,13 @@ namespace eq
     : eq_of_homotopy3 (λa b c, H1 a b c ⬝ H2 a b c) = eq_of_homotopy3 H1 ⬝ eq_of_homotopy3 H2 :=
   ap eq_of_homotopy (eq_of_homotopy (λa, !eq_of_homotopy2_con)) ⬝ !eq_of_homotopy_con
 
+  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
+
 end eq
 
 open eq equiv is_equiv

hott/cubical/pathover2.hlean

@@ -30,7 +30,7 @@ namespace eq
       = change_path (ap_compose g f p) (pathover_ap B (g ∘ f) q) :=
   by induction q; reflexivity
 
-  definition pathover_of_tr_eq_idp (r : b = b') : pathover_of_tr_eq r = pathover_idp_of_eq r :=
+  definition pathover_idp_of_eq_def (r : b = b') : pathover_of_tr_eq r = pathover_idp_of_eq r :=
   idp
 
   definition pathover_of_tr_eq_eq_concato (r : p ▸ b = b₂)
@@ -134,4 +134,36 @@ namespace eq
     tr_eq_of_pathover (q ⬝op r) = tr_eq_of_pathover q ⬝ r :=
   by induction r; reflexivity
 
+  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
+
+  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 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 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 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
+
 end eq

hott/cubical/square.hlean

@@ -722,4 +722,14 @@ namespace eq
     (r : p₂₁' = p₂₁) : aps f (q ⬝ph s₁₁ ⬝hp r⁻¹) = ap02 f q ⬝ph aps f s₁₁ ⬝hp (ap02 f r)⁻¹ :=
   by induction q; induction r; reflexivity
 
+  definition eq_hconcat_equiv [constructor] {p : a₀₀ = a₀₂} (r : p = p₀₁) :
+    square p₁₀ p₁₂ p p₂₁ ≃ square p₁₀ p₁₂ p₀₁ p₂₁ :=
+  equiv.MK (eq_hconcat r⁻¹) (eq_hconcat r)
+    begin intro s, induction r, reflexivity end begin intro s, induction r, reflexivity end
+
+  definition hconcat_eq_equiv [constructor] {p : a₂₀ = a₂₂} (r : p₂₁ = p) :
+    square p₁₀ p₁₂ p₀₁ p₂₁ ≃ square p₁₀ p₁₂ p₀₁ p :=
+  equiv.MK (λs, hconcat_eq s r) (λs, hconcat_eq s r⁻¹)
+    begin intro s, induction r, reflexivity end begin intro s, induction r, reflexivity end
+
 end eq

hott/cubical/squareover.hlean

@@ -35,6 +35,7 @@ namespace eq
             {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₄₄}
@@ -117,9 +118,9 @@ namespace eq
     squareover B (sp ⬝ph s₁₁) q₁₀ q₁₂ q q₂₁ :=
   by induction sp; induction r; exact t₁₁
 
-  definition hconcato_pathover {p : a₂₀ = a₂₂} {sp : p₂₁ = p} {q : b₂₀ =[p] b₂₂}
+  definition hconcato_pathover {p : a₂₀ = a₂₂} {sp : p = p₂₁} {s : square p₁₀ p₁₂ p₀₁ p}
-    (t₁₁ : squareover B s₁₁ q₁₀ q₁₂ q₀₁ q₂₁) (r : change_path sp q₂₁ = q) :
+    {q : b₂₀ =[p] b₂₂} (t₁₁ : squareover B (s ⬝hp sp) q₁₀ q₁₂ q₀₁ q₂₁)
-    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₁₁
 
   infix ` ⬝ho `:69 := hconcato --type using \tr
@@ -304,4 +305,37 @@ namespace eq
     exact square_dpair_eq_dpair s₁₁ t₁₁
   end
 
+  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 -/
+
+  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 eq

hott/eq2.hlean

@@ -7,7 +7,7 @@ Theorems about 2-dimensional paths
 -/
 
 import .cubical.square .function
-open function is_equiv equiv
+open function is_equiv equiv sigma trunc
 
 namespace eq
   variables {A B C : Type} {f : A → B} {a a' a₁ a₂ a₃ a₄ : A} {b b' : B}
@@ -141,6 +141,10 @@ namespace eq
     : whisker_left p q⁻² ⬝ q = con.right_inv p :=
   by cases q; reflexivity
 
+  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 cast_fn_cast_square {A : Type} {B C : A → Type} (f : Π⦃a⦄, B a → C a) {a₁ a₂ : A}
     (p : a₁ = a₂) (q : a₂ = a₁) (r : p ⬝ q = idp) (b : B a₁) :
     cast (ap C q) (f (cast (ap B p) b)) = f b :=
@@ -206,53 +210,94 @@ namespace eq
     (q : p = p') : square (ap_constant p b) (ap_constant p' b) (ap02 (λx, b) q) idp :=
   by induction q; exact vrfl
 
-  section hsquare
+  definition ap_con_idp_left {A B : Type} (f : A → B) {a a' : A} (p : a = a') :
-  variables {A₀₀ A₂₀ A₄₀ A₀₂ A₂₂ A₄₂ A₀₄ A₂₄ A₄₄ : Type}
+    square (ap_con f idp p) idp (ap02 f (idp_con p)) (idp_con (ap f p)) :=
-            {f₁₀ : A₀₀ → A₂₀} {f₃₀ : A₂₀ → A₄₀}
+  begin induction p, exact ids end
-            {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 hsquare [reducible] (f₁₀ : A₀₀ → A₂₀) (f₁₂ : A₀₂ → A₂₂)
+  definition apd10_prepostcompose_nondep {A B C D : Type} (h : C → D) {g g' : B → C} (p : g = g')
-                                 (f₀₁ : A₀₀ → A₀₂) (f₂₁ : A₂₀ → A₂₂) : Type :=
+    (f : A → B) (a : A) : apd10 (ap (λg a, h (g (f a))) p) a = ap h (apd10 p (f a)) :=
-  f₂₁ ∘ f₁₀ ~ f₁₂ ∘ f₀₁
+  begin induction p, reflexivity end
 
-  definition hsquare_of_homotopy (p : f₂₁ ∘ f₁₀ ~ f₁₂ ∘ f₀₁) : hsquare f₁₀ f₁₂ f₀₁ f₂₁ :=
+  definition apd10_prepostcompose {A B : Type} {C : B → Type} {D : A → Type}
-  p
+    (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 homotopy_of_hsquare (p : hsquare f₁₀ f₁₂ f₀₁ f₂₁) : f₂₁ ∘ f₁₀ ~ f₁₂ ∘ f₀₁ :=
+  /- alternative induction principles -/
-  p
+  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 homotopy_top_of_hsquare {f₂₁ : A₂₀ ≃ A₂₂} (p : hsquare f₁₀ f₁₂ f₀₁ f₂₁) :
+  definition eq.rec_to2 {A : Type} {P : Π⦃a₀ a₁⦄, a₀ = a₁ → Type}
-    f₁₀ ~ f₂₁⁻¹ ∘ f₁₂ ∘ f₀₁ :=
+    {a₀ a₀' a₁' : A} (p' : a₀' = a₁') (p₀ : a₀ = a₀') (H : P p') ⦃a₁ : A⦄ (p : a₀ = a₁) : P p :=
-  homotopy_inv_of_homotopy_post _ _ _ p
+  begin
+   induction p₀, induction p', induction p, exact H
+  end
 
-  definition homotopy_top_of_hsquare' [is_equiv f₂₁] (p : hsquare f₁₀ f₁₂ f₀₁ f₂₁) :
+  definition eq.rec_right_inv {A : Type} (f : A ≃ A) {P : Π⦃a₀ a₁⦄, f a₀ = a₁ → Type}
-    f₁₀ ~ f₂₁⁻¹ ∘ f₁₂ ∘ f₀₁ :=
+    (H : Πa, P (right_inv f a)) ⦃a₀ a₁ : A⦄ (p : f a₀ = a₁) : P p :=
-  homotopy_inv_of_homotopy_post _ _ _ 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 hhconcat (p : hsquare f₁₀ f₁₂ f₀₁ f₂₁) (q : hsquare f₃₀ f₃₂ f₂₁ f₄₁) :
+  definition eq.rec_equiv {A B : Type} {a₀ : A} (f : A ≃ B) {P : Π{a₁}, f a₀ = f a₁ → Type}
-    hsquare (f₃₀ ∘ f₁₀) (f₃₂ ∘ f₁₂) f₀₁ f₄₁ :=
+    (H : P (idpath (f a₀))) ⦃a₁ : A⦄ (p : f a₀ = f a₁) : P p :=
-  hwhisker_right f₁₀ q ⬝hty hwhisker_left f₃₂ 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 hvconcat (p : hsquare f₁₀ f₁₂ f₀₁ f₂₁) (q : hsquare f₁₂ f₁₄ f₀₃ f₂₃) :
+  definition eq.rec_equiv_symm {A B : Type} {a₁ : A} (f : A ≃ B) {P : Π{a₀}, f a₀ = f a₁ → Type}
-    hsquare f₁₀ f₁₄ (f₀₃ ∘ f₀₁) (f₂₃ ∘ f₂₁) :=
+    (H : P (idpath (f a₁))) ⦃a₀ : A⦄ (p : f a₀ = f a₁) : P p :=
-  hwhisker_left f₂₃ p ⬝hty hwhisker_right f₀₁ q
+  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 hhinverse {f₁₀ : A₀₀ ≃ A₂₀} {f₁₂ : A₀₂ ≃ A₂₂} (p : hsquare f₁₀ f₁₂ f₀₁ f₂₁) :
+  definition eq.rec_equiv_to_same {A B : Type} {a₀ : A} (f : A ≃ B) {P : Π{a₁}, f a₀ = f a₁ → Type}
-    hsquare f₁₀⁻¹ᵉ f₁₂⁻¹ᵉ f₂₁ f₀₁ :=
+    ⦃a₁' : A⦄ (p' : f a₀ = f a₁') (H : P p') ⦃a₁ : A⦄ (p : f a₀ = f a₁) : P p :=
-  λb, eq_inv_of_eq ((p (f₁₀⁻¹ᵉ b))⁻¹ ⬝ ap f₂₁ (to_right_inv f₁₀ b))
+  begin
+    revert a₁' p' H a₁ p,
+    refine eq.rec_equiv f _,
+    exact eq.rec_equiv f
+  end
 
-  definition hvinverse {f₀₁ : A₀₀ ≃ A₀₂} {f₂₁ : A₂₀ ≃ A₂₂} (p : hsquare f₁₀ f₁₂ f₀₁ f₂₁) :
+  definition eq.rec_equiv_to {A A' B : Type} {a₀ : A} (f : A ≃ B) (g : A' ≃ B)
-    hsquare f₁₂ f₁₀ f₀₁⁻¹ᵉ f₂₁⁻¹ᵉ :=
+    {P : Π{a₁}, f a₀ = g a₁ → Type}
-  λa, inv_eq_of_eq (p (f₀₁⁻¹ᵉ a) ⬝ ap f₁₂ (to_right_inv f₀₁ a))⁻¹
+    ⦃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
 
-  infix ` ⬝htyh `:73 := hhconcat
+  definition eq.rec_grading {A A' B : Type} {a : A} (f : A ≃ B) (g : A' ≃ B)
-  infix ` ⬝htyv `:73 := hvconcat
+    {P : Π{b}, f a = b → Type}
-  postfix `⁻¹ʰᵗʸʰ`:(max+1) := hhinverse
+    {a' : A'} (p' : f a = g a') (H : P p') ⦃b : B⦄ (p : f a = b) : P p :=
-  postfix `⁻¹ʰᵗʸᵛ`:(max+1) := hvinverse
+  begin
+    revert b p, refine equiv_rect g _ _,
+    exact eq.rec_equiv_to f g p' H
+  end
 
-  end hsquare
+  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
 
 end eq

hott/homotopy/circle.hlean

@@ -316,7 +316,7 @@ namespace circle
   begin
     induction x,
     { apply base_eq_base_equiv},
-    { apply equiv_pathover, intro p p' q, apply pathover_of_eq,
+    { apply equiv_pathover2, intro p p' q, apply pathover_of_eq,
       note H := eq_of_square (square_of_pathover q),
       rewrite con_comm_base at H,
       note H' := cancel_left _ H,

hott/homotopy/connectedness.hlean

@@ -458,11 +458,34 @@ namespace is_conn
     { intro f', reflexivity }
   end
 
-
   definition is_contr_of_is_conn_of_is_trunc {n : ℕ₋₂} {A : Type} (H : is_trunc n A)
     (K : is_conn n A) : is_contr A :=
   is_contr_equiv_closed (trunc_equiv n A)
 
+  definition is_trunc_succ_succ_of_is_trunc_loop (n : ℕ₋₂) (A : Type*) (H : is_trunc (n.+1) (Ω A))
+    (H2 : is_conn 0 A) : is_trunc (n.+2) A :=
+  begin
+    apply is_trunc_succ_of_is_trunc_loop, apply minus_one_le_succ,
+    refine is_conn.elim -1 _ _, exact H
+  end
+
+  lemma is_trunc_of_is_trunc_loopn (m n : ℕ) (A : Type*) (H : is_trunc n (Ω[m] A))
+    (H2 : is_conn (m.-1) A) : is_trunc (m + n) A :=
+  begin
+    revert A H H2; induction m with m IH: intro A H H2,
+    { rewrite [nat.zero_add], exact H },
+    rewrite [succ_add],
+    apply is_trunc_succ_succ_of_is_trunc_loop,
+    { apply IH,
+      { apply is_trunc_equiv_closed _ !loopn_succ_in },
+      apply is_conn_loop },
+    exact is_conn_of_le _ (zero_le_of_nat m)
+  end
+
+  lemma is_trunc_of_is_set_loopn (m : ℕ) (A : Type*) (H : is_set (Ω[m] A))
+    (H2 : is_conn (m.-1) A) : is_trunc m A :=
+  is_trunc_of_is_trunc_loopn m 0 A H H2
+
 end is_conn
 
 /-

hott/homotopy/homotopy_group.hlean

@@ -32,7 +32,7 @@ namespace is_trunc
     : is_contr (π[k] A) :=
   begin
       have H3 : is_contr (ptrunc k A), from is_conn_of_le A (of_nat_le_of_nat H),
-      have H4 : is_contr (Ω[k](ptrunc k A)), from !is_trunc_loop_of_is_trunc,
+      have H4 : is_contr (Ω[k](ptrunc k A)), from !is_trunc_loopn_of_is_trunc,
       apply is_trunc_equiv_closed_rev,
       { apply equiv_of_pequiv (homotopy_group_pequiv_loop_ptrunc k A)}
   end
@@ -206,6 +206,45 @@ namespace is_trunc
     cases A with A a, exact H k H'
   end
 
+  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 },
+    { 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
+
   definition ab_group_homotopy_group_of_is_conn (n : ℕ) (A : Type*) [H : is_conn 1 A] :
     ab_group (π[n] A) :=
   begin

hott/init/equiv.hlean

@@ -462,3 +462,69 @@ end is_equiv
 
 export [unfold] equiv
 export [unfold] is_equiv
+
+/- properties about squares of functions -/
+namespace eq
+
+  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 hsquare [reducible] (f₁₀ : A₀₀ → A₂₀) (f₁₂ : A₀₂ → A₂₂)
+                                 (f₀₁ : A₀₀ → A₀₂) (f₂₁ : A₂₀ → A₂₂) : Type :=
+  f₂₁ ∘ f₁₀ ~ f₁₂ ∘ f₀₁
+
+  definition hsquare_of_homotopy (p : f₂₁ ∘ f₁₀ ~ f₁₂ ∘ f₀₁) : hsquare f₁₀ f₁₂ f₀₁ f₂₁ :=
+  p
+
+  definition homotopy_of_hsquare (p : hsquare f₁₀ f₁₂ f₀₁ f₂₁) : f₂₁ ∘ f₁₀ ~ f₁₂ ∘ f₀₁ :=
+  p
+
+  definition homotopy_top_of_hsquare {f₂₁ : A₂₀ ≃ A₂₂} (p : hsquare f₁₀ f₁₂ f₀₁ f₂₁) :
+    f₁₀ ~ f₂₁⁻¹ ∘ f₁₂ ∘ f₀₁ :=
+  homotopy_inv_of_homotopy_post _ _ _ p
+
+  definition homotopy_top_of_hsquare' [is_equiv f₂₁] (p : hsquare f₁₀ f₁₂ f₀₁ f₂₁) :
+    f₁₀ ~ f₂₁⁻¹ ∘ f₁₂ ∘ f₀₁ :=
+  homotopy_inv_of_homotopy_post _ _ _ p
+
+  definition hhconcat [unfold_full] (p : hsquare f₁₀ f₁₂ f₀₁ f₂₁) (q : hsquare f₃₀ f₃₂ f₂₁ f₄₁) :
+    hsquare (f₃₀ ∘ f₁₀) (f₃₂ ∘ f₁₂) f₀₁ f₄₁ :=
+  hwhisker_right f₁₀ q ⬝hty hwhisker_left f₃₂ p
+
+  definition hvconcat [unfold_full] (p : hsquare f₁₀ f₁₂ f₀₁ f₂₁) (q : hsquare f₁₂ f₁₄ f₀₃ f₂₃) :
+    hsquare f₁₀ f₁₄ (f₀₃ ∘ f₀₁) (f₂₃ ∘ f₂₁) :=
+  hwhisker_left f₂₃ p ⬝hty hwhisker_right f₀₁ q
+
+  definition hhinverse {f₁₀ : A₀₀ ≃ A₂₀} {f₁₂ : A₀₂ ≃ A₂₂} (p : hsquare f₁₀ f₁₂ f₀₁ f₂₁) :
+    hsquare f₁₀⁻¹ᵉ f₁₂⁻¹ᵉ f₂₁ f₀₁ :=
+  λb, eq_inv_of_eq ((p (f₁₀⁻¹ᵉ b))⁻¹ ⬝ ap f₂₁ (to_right_inv f₁₀ b))
+
+  definition hvinverse {f₀₁ : A₀₀ ≃ A₀₂} {f₂₁ : A₂₀ ≃ A₂₂} (p : hsquare f₁₀ f₁₂ f₀₁ f₂₁) :
+    hsquare f₁₂ f₁₀ f₀₁⁻¹ᵉ f₂₁⁻¹ᵉ :=
+  λa, inv_eq_of_eq (p (f₀₁⁻¹ᵉ a) ⬝ ap f₁₂ (to_right_inv f₀₁ a))⁻¹
+
+  infix ` ⬝htyh `:73 := hhconcat
+  infix ` ⬝htyv `:73 := hvconcat
+  postfix `⁻¹ʰᵗʸʰ`:(max+1) := hhinverse
+  postfix `⁻¹ʰᵗʸᵛ`:(max+1) := hvinverse
+
+  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
+
+end eq

hott/init/nat.hlean

@@ -102,9 +102,10 @@ namespace nat
   protected definition le_trans {n m k : ℕ} (H1 : n ≤ m) : m ≤ k → n ≤ k :=
   le.rec H1 (λp H2, le.step)
 
-  definition le_succ_of_le {n m : ℕ} (H : n ≤ m) : n ≤ succ m := nat.le_trans H !le_succ
+  definition le_succ_of_le {n m : ℕ} (H : n ≤ m) : n ≤ succ m := le.step H
 
-  definition le_of_succ_le {n m : ℕ} (H : succ n ≤ m) : n ≤ m := nat.le_trans !le_succ H
+  definition le_of_succ_le {n m : ℕ} (H : succ n ≤ m) : n ≤ m :=
+  by induction H with H m H'; exact le_succ n; exact le.step H'
 
   protected definition le_of_lt {n m : ℕ} (H : n < m) : n ≤ m := le_of_succ_le H
 

hott/init/path.hlean

@@ -275,20 +275,20 @@ namespace eq
   definition hassoc {A B C D : Type} (h : C → D) (g : B → C) (f : A → B) : (h ∘ g) ∘ f ~ h ∘ (g ∘ f) :=
   λa, idp
 
-  definition homotopy_of_eq {f g : Πx, P x} (H1 : f = g) : f ~ g :=
+  definition homotopy_of_eq [unfold 5] {f g : Πx, P x} (H : f = g) : f ~ g :=
-  H1 ▸ homotopy.refl f
+  λa, ap (λh, h a) H
 
   definition apd10 [unfold 5] {f g : Πx, P x} (H : f = g) : f ~ g :=
-  λx, by induction H; reflexivity
+  λa, ap (λh, h a) H
 
   --the next theorem is useful if you want to write "apply (apd10' a)"
   definition apd10' [unfold 6] {f g : Πx, P x} (a : A) (H : f = g) : f a = g a :=
-  by induction H; reflexivity
+  apd10 H a
 
-  --apd10 is also ap evaluation
+  --apd10 is a special case of ap
   definition apd10_eq_ap_eval {f g : Πx, P x} (H : f = g) (a : A)
     : apd10 H a = ap (λs : Πx, P x, s a) H :=
-  by induction H; reflexivity
+  by reflexivity
 
   definition ap10 [reducible] [unfold 5] {f g : A → B} (H : f = g) : f ~ g := apd10 H
 

hott/init/pathover.hlean

@@ -314,6 +314,10 @@ namespace eq
     (q : f =[p] g) (r : b =[p] b₂) : f b = g b₂ :=
   eq_of_pathover (apo11 q r)
 
+  definition apd02 [unfold 8] (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
+
   /- properties about these "ap"s, transporto and pathover_ap -/
   definition apd_con (f : Πa, B a) (p : a = a₂) (q : a₂ = a₃)
     : apd f (p ⬝ q) = apd f p ⬝o apd f q :=

hott/types/eq.hlean

@@ -83,6 +83,7 @@ namespace eq
   !idp_con⁻¹ ⬝ whisker_left idp r = r ⬝ !idp_con⁻¹ :=
   by induction r;induction q;reflexivity
 
+  -- this should maybe replace whisker_left_idp and whisker_left_idp_con
   definition whisker_left_idp_con {q q' : a₂ = a₃} (r : q = q') :
   whisker_left idp r ⬝ !idp_con = !idp_con ⬝ r :=
   by induction r;induction q;reflexivity
@@ -461,31 +462,36 @@ namespace eq
 
   section
     parameters {A : Type} (a₀ : A) (code : A → Type) (H : is_contr (Σa, code a))
-      (p : (center (Σa, code a)).1 = a₀)
+      (c₀ : code a₀)
-    include p
+    include H c₀
     protected definition encode {a : A} (q : a₀ = a) : code a :=
-    (p ⬝ q) ▸ (center (Σa, code a)).2
+    transport code q c₀
 
     protected definition decode' {a : A} (c : code a) : a₀ = a :=
-    (is_prop.elim ⟨a₀, encode idp⟩ ⟨a, c⟩)..1
+    have ⟨a₀, c₀⟩ = ⟨a, c⟩ :> Σa, code a, from !is_prop.elim,
+    this..1
 
     protected definition decode {a : A} (c : code a) : a₀ = a :=
-    (decode' (encode idp))⁻¹ ⬝ decode' c
+    (decode' c₀)⁻¹ ⬝ decode' c
 
+    open sigma.ops
     definition total_space_method (a : A) : (a₀ = a) ≃ code a :=
     begin
       fapply equiv.MK,
-      { exact encode},
+      { exact encode },
-      { exact decode},
+      { exact decode },
-      { intro c,
+      { intro c, unfold [encode, decode, decode'],
-        unfold [encode, decode, decode'],
+        rewrite [is_prop_elim_self, ▸*, idp_con],
-        induction p, esimp, rewrite [is_prop_elim_self,▸*,+idp_con],
+        apply tr_eq_of_pathover, apply eq_pr2 },
-        apply tr_eq_of_pathover,
-        eapply @sigma.rec_on _ _ (λx, x.2 =[(is_prop.elim ⟨x.1, x.2⟩ ⟨a, c⟩)..1] c)
-          (center (sigma code)),
-        intro a c, 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_method a₀ code H c₀ a₀ idp = c₀ :=
+  begin
+    reflexivity
   end
 
   definition encode_decode_method {A : Type} (a₀ a : A) (code : A → Type) (c₀ : code a₀)
@@ -498,7 +504,7 @@ namespace eq
       { intro p, fapply sigma_eq,
           apply decode, exact p.2,
         apply encode_decode}},
-    { reflexivity}
+    { exact c₀ }
   end
 
 end eq

hott/types/equiv.hlean

@@ -228,6 +228,14 @@ namespace equiv
   definition equiv_eq {f f' : A ≃ B} (p : to_fun f ~ to_fun f') : f = f' :=
   by apply equiv_eq'; apply eq_of_homotopy p
 
+  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 trans_symm (f : A ≃ B) (g : B ≃ C) : (f ⬝e g)⁻¹ᵉ = g⁻¹ᵉ ⬝e f⁻¹ᵉ :> (C ≃ A) :=
   equiv_eq' idp
 
@@ -264,13 +272,30 @@ namespace equiv
 
   definition equiv_pathover {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 : Π(b : B a) (b' : B a') (q : b =[p] b'), f b =[p] g b') : f =[p] g :=
+    (r : to_fun f =[p] to_fun g) : f =[p] g :=
   begin
     fapply pathover_of_fn_pathover_fn,
-    { intro a, apply equiv.sigma_char},
+    { intro a, apply equiv.sigma_char },
-    { fapply sigma_pathover,
+    { apply sigma_pathover _ _ _ r, apply is_prop.elimo }
-        esimp, apply arrow_pathover, exact r,
+  end
-        apply is_prop.elimo}
+
+  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 : Π(b : B a) (b' : B a') (q : b =[p] b'), f b =[p] g b') : f =[p] g :=
+  begin
+    apply equiv_pathover, apply arrow_pathover, exact r
+  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_pathover,
+    change f⁻¹ᶠ⁻¹ᶠ =[p] g⁻¹ᶠ⁻¹ᶠ,
+    apply apo (λ(a: A) (h : C a ≃ B a), h⁻¹ᶠ),
+    apply equiv_pathover,
+    exact r
   end
 
   definition is_contr_equiv (A B : Type) [HA : is_contr A] [HB : is_contr B] : is_contr (A ≃ B) :=

hott/types/lift.hlean

@@ -138,14 +138,27 @@ namespace lift
       apply ua_refl}
   end
 
+  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) },
+    { 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
+
+  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))
+
+  -- is_trunc_lift is defined in init.trunc
+
   definition plift [constructor] (A : pType.{u}) : pType.{max u v} :=
   pointed.MK (lift A) (up pt)
 
   definition plift_functor [constructor] {A B : Type*} (f : A →* B) : plift A →* plift B :=
   pmap.mk (lift_functor f) (ap up (respect_pt f))
 
-  -- is_trunc_lift is defined in init.trunc
-
   definition pup [constructor] {A : Type*} : A →* plift A :=
   pmap.mk up idp
 
@@ -164,15 +177,8 @@ namespace lift
   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) :
+  definition is_trunc_plift [instance] [priority 1450] (A : Type*) (n : ℕ₋₂)
-    fiber (lift_functor f) (up b) ≃ fiber f b :=
+    [H : is_trunc n A] : is_trunc n (plift A) :=
-  begin
+  is_trunc_lift A n
-    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) },
-    { 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

hott/types/nat/basic.hlean

@@ -315,4 +315,5 @@ definition iterate {A : Type} (op : A → A) : ℕ → A → A
  | (succ k) := λ a, op (iterate k a)
 
 notation f `^[`:80 n:0 `]`:0 := iterate f n
+
 end

hott/types/nat/hott.hlean

@@ -137,6 +137,46 @@ namespace nat
     { exact H2 k}
   end
 
+  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
+
   /- 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
@@ -213,14 +253,26 @@ namespace nat
       refine ap (f^[n]) _ ⬝ !iterate_succ⁻¹, exact !to_right_inv⁻¹ }
   end
 
+  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_commute {A : Type} {f g : A → A} (n : ℕ) (h : f ∘ g ~ g ∘ f) :
-    iterate f n ∘ g ~ g ∘ iterate f n :=
+    f^[n] ∘ g ~ g ∘ f^[n] :=
-  by induction n with n IH; reflexivity; exact λx, ap f (IH x) ⬝ !h
+  (iterate_hsquare g h⁻¹ʰᵗʸ n)⁻¹ʰᵗʸ
 
   definition iterate_equiv {A : Type} (f : A ≃ A) (n : ℕ) : A ≃ A :=
   equiv.mk (iterate f n)
            (by induction n with n IH; apply is_equiv_id; exact is_equiv_compose f (iterate f n))
 
+  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
+
   definition iterate_inv {A : Type} (f : A ≃ A) (n : ℕ) :
     (iterate_equiv f n)⁻¹ ~ iterate f⁻¹ n :=
   begin
@@ -235,6 +287,10 @@ namespace nat
   definition iterate_right_inv {A : Type} (f : A ≃ A) (n : ℕ) (a : A) : f^[n] (f⁻¹ᵉ^[n] a) = a :=
   ap (f^[n]) (iterate_inv f n a)⁻¹ ⬝ to_right_inv (iterate_equiv f n) a
 
+  /- the same theorem add_le_add_left but with a proof by structural induction -/
+  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₂
+
 
 
 end nat

hott/types/pi.hlean

@@ -16,36 +16,15 @@ namespace pi
             {D : Πa b, C a b → Type}
             {a a' a'' : A} {b b₁ b₂ : B a} {b' : B a'} {b'' : B a''} {f g : Πa, B a}
 
-  /- Paths -/
+  /- Paths are charactirized in [init/funext] -/
-
-  /-
-    Paths [p : f ≈ g] in a function type [Πx:X, P x] are equivalent to functions taking values
-    in path types, [H : Πx:X, f x ≈ g x], or concisely, [H : f ~ g].
-
-    This equivalence, however, is just the combination of [apd10] and function extensionality
-    [funext], and as such, [eq_of_homotopy]
-
-    Now we show how these things compute.
-  -/
-
-  definition apd10_eq_of_homotopy (h : f ~ g) : apd10 (eq_of_homotopy h) ~ h :=
-  apd10 (right_inv apd10 h)
-
-  definition eq_of_homotopy_eta (p : f = g) : eq_of_homotopy (apd10 p) = p :=
-  left_inv apd10 p
-
-  definition eq_of_homotopy_idp (f : Πa, B a) : eq_of_homotopy (λx : A, refl (f x)) = refl f :=
-  !eq_of_homotopy_eta
 
   /- homotopy.symm is an equivalence -/
+  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 is_equiv_homotopy_symm : is_equiv (homotopy.symm : f ~ g → g ~ f) :=
-  begin
+  adjointify homotopy.symm homotopy.symm homotopy.symm_symm homotopy.symm_symm
-    fapply adjointify homotopy.symm homotopy.symm,
-    { intro p, apply eq_of_homotopy, intro a,
-      unfold homotopy.symm, apply inv_inv },
-    { intro p, apply eq_of_homotopy, intro a,
-      unfold homotopy.symm, apply inv_inv }
-  end
 
   /-
     The identification of the path space of a dependent function space,

hott/types/pointed.hlean

@@ -70,13 +70,13 @@ namespace pointed
     : Σ(p : carrier A = carrier B :> Type), Point A =[p] Point B :=
   by induction p; exact ⟨idp, idpo⟩
 
-  protected definition pType.sigma_char.{u} : pType.{u} ≃ Σ(X : Type.{u}), X :=
+  definition pType.sigma_char.{u} [constructor] : pType.{u} ≃ Σ(X : Type.{u}), X :=
   begin
     fapply equiv.MK,
-    { intro x, induction x with X x, exact ⟨X, x⟩},
+    { intro X, exact ⟨X, pt⟩ },
-    { intro x, induction x with X x, exact pointed.MK X x},
+    { 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 },
-    { intro x, induction x with X x, reflexivity},
+    { intro x, induction x with X x, reflexivity },
   end
 
   definition pType.eta_expand [constructor] (A : Type*) : Type* :=
@@ -168,6 +168,16 @@ namespace pointed
   definition pmap.eta_expand [constructor] {A B : Type*} (f : A →* B) : A →* B :=
   pmap.mk f (respect_pt f)
 
+  definition pmap_eta [constructor] {X Y : Type*} (f : X →* Y) : f ~* pmap.mk f (respect_pt f) :=
+  begin
+    fapply phomotopy.mk,
+    reflexivity,
+    esimp, exact !idp_con
+  end
+
+  definition pmap_eta_eq {A B : Type*} (f : A →* B) : pmap.mk f (respect_pt f) = f :=
+  begin induction f, reflexivity end
+
   definition pmap_equiv_right (A : Type*) (B : Type)
     : (Σ(b : B), A →* (pointed.Mk b)) ≃ (A → B) :=
   begin
@@ -201,7 +211,7 @@ namespace pointed
     we generalize the definition of ap1 to arbitrary paths, so that we can prove properties about it
     using path induction (see for example ap1_gen_con and ap1_gen_con_natural)
   -/
-  definition ap1_gen [reducible] [unfold 6 9 10] {A B : Type} (f : A → B) {a a' : A}
+  definition ap1_gen [reducible] [unfold 8 9 10] {A B : Type} (f : A → B) {a a' : A}
     {b b' : B} (q : f a = b) (q' : f a' = b') (p : a = a') : b = b' :=
   q⁻¹ ⬝ ap f p ⬝ q'
 
@@ -1189,4 +1199,100 @@ namespace pointed
     apply apn_succ_phomotopy_in
   end
 
+  section psquare
+  /-
+    Squares of pointed maps
+
+    We treat expressions of the form
+      psquare f g h k :≡ k ∘* f ~* g ∘* h
+    as squares, where f is the top, g is the bottom, h is the left face and k is the right face.
+    Then the following are operations on squares
+  -/
+
+  variables {A' A₀₀ A₂₀ A₄₀ A₀₂ A₂₂ A₄₂ A₀₄ A₂₄ A₄₄ : Type*}
+            {f₁₀ f₁₀' : A₀₀ →* A₂₀} {f₃₀ : A₂₀ →* A₄₀}
+            {f₀₁ f₀₁' : A₀₀ →* A₀₂} {f₂₁ f₂₁' : A₂₀ →* A₂₂} {f₄₁ : A₄₀ →* A₄₂}
+            {f₁₂ f₁₂' : A₀₂ →* A₂₂} {f₃₂ : A₂₂ →* A₄₂}
+            {f₀₃ : A₀₂ →* A₀₄} {f₂₃ : A₂₂ →* A₂₄} {f₄₃ : A₄₂ →* A₄₄}
+            {f₁₄ : A₀₄ →* A₂₄} {f₃₄ : A₂₄ →* A₄₄}
+
+  definition psquare [reducible] (f₁₀ : A₀₀ →* A₂₀) (f₁₂ : A₀₂ →* A₂₂)
+                                 (f₀₁ : A₀₀ →* A₀₂) (f₂₁ : A₂₀ →* A₂₂) : Type :=
+  f₂₁ ∘* f₁₀ ~* f₁₂ ∘* f₀₁
+
+  definition psquare_of_phomotopy (p : f₂₁ ∘* f₁₀ ~* f₁₂ ∘* f₀₁) : psquare f₁₀ f₁₂ f₀₁ f₂₁ :=
+  p
+
+  definition phomotopy_of_psquare (p : psquare f₁₀ f₁₂ f₀₁ f₂₁) : f₂₁ ∘* f₁₀ ~* f₁₂ ∘* f₀₁ :=
+  p
+
+  definition phdeg_square {f f' : A →* A'} (p : f ~* f') : psquare !pid !pid f f' :=
+  !pcompose_pid ⬝* p⁻¹* ⬝* !pid_pcompose⁻¹*
+  definition pvdeg_square {f f' : A →* A'} (p : f ~* f') : psquare f f' !pid !pid :=
+  !pid_pcompose ⬝* p ⬝* !pcompose_pid⁻¹*
+
+  variables (f₀₁ f₁₀)
+  definition phrefl : psquare !pid !pid f₀₁ f₀₁ := phdeg_square phomotopy.rfl
+  definition pvrefl : psquare f₁₀ f₁₀ !pid !pid := pvdeg_square phomotopy.rfl
+  variables {f₀₁ f₁₀}
+  definition phrfl : psquare !pid !pid f₀₁ f₀₁ := phrefl f₀₁
+  definition pvrfl : psquare f₁₀ f₁₀ !pid !pid := pvrefl f₁₀
+
+  definition phconcat (p : psquare f₁₀ f₁₂ f₀₁ f₂₁) (q : psquare f₃₀ f₃₂ f₂₁ f₄₁) :
+    psquare (f₃₀ ∘* f₁₀) (f₃₂ ∘* f₁₂) f₀₁ f₄₁ :=
+  !passoc⁻¹* ⬝* pwhisker_right f₁₀ q ⬝* !passoc ⬝* pwhisker_left f₃₂ p ⬝* !passoc⁻¹*
+
+  definition pvconcat (p : psquare f₁₀ f₁₂ f₀₁ f₂₁) (q : psquare f₁₂ f₁₄ f₀₃ f₂₃) :
+    psquare f₁₀ f₁₄ (f₀₃ ∘* f₀₁) (f₂₃ ∘* f₂₁) :=
+  !passoc ⬝* pwhisker_left _ p ⬝* !passoc⁻¹* ⬝* pwhisker_right _ q ⬝* !passoc
+
+  definition phinverse {f₁₀ : A₀₀ ≃* A₂₀} {f₁₂ : A₀₂ ≃* A₂₂} (p : psquare f₁₀ f₁₂ f₀₁ f₂₁) :
+    psquare f₁₀⁻¹ᵉ* f₁₂⁻¹ᵉ* f₂₁ f₀₁ :=
+  !pid_pcompose⁻¹* ⬝* pwhisker_right _ (pleft_inv f₁₂)⁻¹* ⬝* !passoc ⬝*
+  pwhisker_left _
+    (!passoc⁻¹* ⬝* pwhisker_right _ p⁻¹* ⬝* !passoc ⬝* pwhisker_left _ !pright_inv ⬝* !pcompose_pid)
+
+  definition pvinverse {f₀₁ : A₀₀ ≃* A₀₂} {f₂₁ : A₂₀ ≃* A₂₂} (p : psquare f₁₀ f₁₂ f₀₁ f₂₁) :
+    psquare f₁₂ f₁₀ f₀₁⁻¹ᵉ* f₂₁⁻¹ᵉ* :=
+  (phinverse p⁻¹*)⁻¹*
+
+  definition phomotopy_hconcat (q : f₀₁' ~* f₀₁) (p : psquare f₁₀ f₁₂ f₀₁ f₂₁) :
+    psquare f₁₀ f₁₂ f₀₁' f₂₁ :=
+  p ⬝* pwhisker_left f₁₂ q⁻¹*
+
+  definition hconcat_phomotopy (p : psquare f₁₀ f₁₂ f₀₁ f₂₁) (q : f₂₁' ~* f₂₁) :
+    psquare f₁₀ f₁₂ f₀₁ f₂₁' :=
+  pwhisker_right f₁₀ q ⬝* p
+
+  definition phomotopy_vconcat (q : f₁₀' ~* f₁₀) (p : psquare f₁₀ f₁₂ f₀₁ f₂₁) :
+    psquare f₁₀' f₁₂ f₀₁ f₂₁ :=
+  pwhisker_left f₂₁ q ⬝* p
+
+  definition vconcat_phomotopy (p : psquare f₁₀ f₁₂ f₀₁ f₂₁) (q : f₁₂' ~* f₁₂) :
+    psquare f₁₀ f₁₂' f₀₁ f₂₁ :=
+  p ⬝* pwhisker_right f₀₁ q⁻¹*
+
+  infix ` ⬝h* `:73 := phconcat
+  infix ` ⬝v* `:73 := pvconcat
+  infixl ` ⬝hp* `:72 := hconcat_phomotopy
+  infixr ` ⬝ph* `:72 := phomotopy_hconcat
+  infixl ` ⬝vp* `:72 := vconcat_phomotopy
+  infixr ` ⬝pv* `:72 := phomotopy_vconcat
+  postfix `⁻¹ʰ*`:(max+1) := phinverse
+  postfix `⁻¹ᵛ*`:(max+1) := pvinverse
+
+  definition pwhisker_tl (f : A →* A₀₀) (q : psquare f₁₀ f₁₂ f₀₁ f₂₁) :
+    psquare (f₁₀ ∘* f) f₁₂ (f₀₁ ∘* f) f₂₁ :=
+  !passoc⁻¹* ⬝* pwhisker_right f q ⬝* !passoc
+
+  definition ap1_psquare (p : psquare f₁₀ f₁₂ f₀₁ f₂₁) :
+    psquare (Ω→ f₁₀) (Ω→ f₁₂) (Ω→ f₀₁) (Ω→ f₂₁) :=
+  !ap1_pcompose⁻¹* ⬝* ap1_phomotopy p ⬝* !ap1_pcompose
+
+  definition apn_psquare (n : ℕ) (p : psquare f₁₀ f₁₂ f₀₁ f₂₁) :
+    psquare (Ω→[n] f₁₀) (Ω→[n] f₁₂) (Ω→[n] f₀₁) (Ω→[n] f₂₁) :=
+  !apn_pcompose⁻¹* ⬝* apn_phomotopy n p ⬝* !apn_pcompose
+
+  end psquare
+
 end pointed

hott/types/pointed2.hlean

@@ -13,125 +13,13 @@ Contains
 -/
 
 
-import algebra.homotopy_group eq2
+import eq2 .unit
 
-open pointed eq unit is_trunc trunc nat group is_equiv equiv sigma function bool
+open pointed eq unit is_trunc trunc nat is_equiv equiv sigma function bool sigma.ops
 
 namespace pointed
   variables {A B C : Type*} {P : A → Type} {p₀ : P pt} {k k' l m n : ppi P p₀}
 
-  section psquare
-  /-
-    Squares of pointed maps
-
-    We treat expressions of the form
-      psquare f g h k :≡ k ∘* f ~* g ∘* h
-    as squares, where f is the top, g is the bottom, h is the left face and k is the right face.
-    Then the following are operations on squares
-  -/
-
-  variables {A' A₀₀ A₂₀ A₄₀ A₀₂ A₂₂ A₄₂ A₀₄ A₂₄ A₄₄ : Type*}
-            {f₁₀ f₁₀' : A₀₀ →* A₂₀} {f₃₀ : A₂₀ →* A₄₀}
-            {f₀₁ f₀₁' : A₀₀ →* A₀₂} {f₂₁ f₂₁' : A₂₀ →* A₂₂} {f₄₁ : A₄₀ →* A₄₂}
-            {f₁₂ f₁₂' : A₀₂ →* A₂₂} {f₃₂ : A₂₂ →* A₄₂}
-            {f₀₃ : A₀₂ →* A₀₄} {f₂₃ : A₂₂ →* A₂₄} {f₄₃ : A₄₂ →* A₄₄}
-            {f₁₄ : A₀₄ →* A₂₄} {f₃₄ : A₂₄ →* A₄₄}
-
-  definition psquare [reducible] (f₁₀ : A₀₀ →* A₂₀) (f₁₂ : A₀₂ →* A₂₂)
-                                 (f₀₁ : A₀₀ →* A₀₂) (f₂₁ : A₂₀ →* A₂₂) : Type :=
-  f₂₁ ∘* f₁₀ ~* f₁₂ ∘* f₀₁
-
-  definition psquare_of_phomotopy (p : f₂₁ ∘* f₁₀ ~* f₁₂ ∘* f₀₁) : psquare f₁₀ f₁₂ f₀₁ f₂₁ :=
-  p
-
-  definition phomotopy_of_psquare (p : psquare f₁₀ f₁₂ f₀₁ f₂₁) : f₂₁ ∘* f₁₀ ~* f₁₂ ∘* f₀₁ :=
-  p
-
-  definition phdeg_square {f f' : A →* A'} (p : f ~* f') : psquare !pid !pid f f' :=
-  !pcompose_pid ⬝* p⁻¹* ⬝* !pid_pcompose⁻¹*
-  definition pvdeg_square {f f' : A →* A'} (p : f ~* f') : psquare f f' !pid !pid :=
-  !pid_pcompose ⬝* p ⬝* !pcompose_pid⁻¹*
-
-  variables (f₀₁ f₁₀)
-  definition phrefl : psquare !pid !pid f₀₁ f₀₁ := phdeg_square phomotopy.rfl
-  definition pvrefl : psquare f₁₀ f₁₀ !pid !pid := pvdeg_square phomotopy.rfl
-  variables {f₀₁ f₁₀}
-  definition phrfl : psquare !pid !pid f₀₁ f₀₁ := phrefl f₀₁
-  definition pvrfl : psquare f₁₀ f₁₀ !pid !pid := pvrefl f₁₀
-
-  definition phconcat (p : psquare f₁₀ f₁₂ f₀₁ f₂₁) (q : psquare f₃₀ f₃₂ f₂₁ f₄₁) :
-    psquare (f₃₀ ∘* f₁₀) (f₃₂ ∘* f₁₂) f₀₁ f₄₁ :=
-  !passoc⁻¹* ⬝* pwhisker_right f₁₀ q ⬝* !passoc ⬝* pwhisker_left f₃₂ p ⬝* !passoc⁻¹*
-
-  definition pvconcat (p : psquare f₁₀ f₁₂ f₀₁ f₂₁) (q : psquare f₁₂ f₁₄ f₀₃ f₂₃) :
-    psquare f₁₀ f₁₄ (f₀₃ ∘* f₀₁) (f₂₃ ∘* f₂₁) :=
-  !passoc ⬝* pwhisker_left _ p ⬝* !passoc⁻¹* ⬝* pwhisker_right _ q ⬝* !passoc
-
-  definition phinverse {f₁₀ : A₀₀ ≃* A₂₀} {f₁₂ : A₀₂ ≃* A₂₂} (p : psquare f₁₀ f₁₂ f₀₁ f₂₁) :
-    psquare f₁₀⁻¹ᵉ* f₁₂⁻¹ᵉ* f₂₁ f₀₁ :=
-  !pid_pcompose⁻¹* ⬝* pwhisker_right _ (pleft_inv f₁₂)⁻¹* ⬝* !passoc ⬝*
-  pwhisker_left _
-    (!passoc⁻¹* ⬝* pwhisker_right _ p⁻¹* ⬝* !passoc ⬝* pwhisker_left _ !pright_inv ⬝* !pcompose_pid)
-
-  definition pvinverse {f₀₁ : A₀₀ ≃* A₀₂} {f₂₁ : A₂₀ ≃* A₂₂} (p : psquare f₁₀ f₁₂ f₀₁ f₂₁) :
-    psquare f₁₂ f₁₀ f₀₁⁻¹ᵉ* f₂₁⁻¹ᵉ* :=
-  (phinverse p⁻¹*)⁻¹*
-
-  definition phomotopy_hconcat (q : f₀₁' ~* f₀₁) (p : psquare f₁₀ f₁₂ f₀₁ f₂₁) :
-    psquare f₁₀ f₁₂ f₀₁' f₂₁ :=
-  p ⬝* pwhisker_left f₁₂ q⁻¹*
-
-  definition hconcat_phomotopy (p : psquare f₁₀ f₁₂ f₀₁ f₂₁) (q : f₂₁' ~* f₂₁) :
-    psquare f₁₀ f₁₂ f₀₁ f₂₁' :=
-  pwhisker_right f₁₀ q ⬝* p
-
-  definition phomotopy_vconcat (q : f₁₀' ~* f₁₀) (p : psquare f₁₀ f₁₂ f₀₁ f₂₁) :
-    psquare f₁₀' f₁₂ f₀₁ f₂₁ :=
-  pwhisker_left f₂₁ q ⬝* p
-
-  definition vconcat_phomotopy (p : psquare f₁₀ f₁₂ f₀₁ f₂₁) (q : f₁₂' ~* f₁₂) :
-    psquare f₁₀ f₁₂' f₀₁ f₂₁ :=
-  p ⬝* pwhisker_right f₀₁ q⁻¹*
-
-  infix ` ⬝h* `:73 := phconcat
-  infix ` ⬝v* `:73 := pvconcat
-  infixl ` ⬝hp* `:72 := hconcat_phomotopy
-  infixr ` ⬝ph* `:72 := phomotopy_hconcat
-  infixl ` ⬝vp* `:72 := vconcat_phomotopy
-  infixr ` ⬝pv* `:72 := phomotopy_vconcat
-  postfix `⁻¹ʰ*`:(max+1) := phinverse
-  postfix `⁻¹ᵛ*`:(max+1) := pvinverse
-
-  definition pwhisker_tl (f : A →* A₀₀) (q : psquare f₁₀ f₁₂ f₀₁ f₂₁) :
-    psquare (f₁₀ ∘* f) f₁₂ (f₀₁ ∘* f) f₂₁ :=
-  !passoc⁻¹* ⬝* pwhisker_right f q ⬝* !passoc
-
-  definition ap1_psquare (p : psquare f₁₀ f₁₂ f₀₁ f₂₁) :
-    psquare (Ω→ f₁₀) (Ω→ f₁₂) (Ω→ f₀₁) (Ω→ f₂₁) :=
-  !ap1_pcompose⁻¹* ⬝* ap1_phomotopy p ⬝* !ap1_pcompose
-
-  definition apn_psquare (n : ℕ) (p : psquare f₁₀ f₁₂ f₀₁ f₂₁) :
-    psquare (Ω→[n] f₁₀) (Ω→[n] f₁₂) (Ω→[n] f₀₁) (Ω→[n] f₂₁) :=
-  !apn_pcompose⁻¹* ⬝* apn_phomotopy n p ⬝* !apn_pcompose
-
-  definition ptrunc_functor_psquare (n : ℕ₋₂) (p : psquare f₁₀ f₁₂ f₀₁ f₂₁) :
-    psquare (ptrunc_functor n f₁₀) (ptrunc_functor n f₁₂)
-            (ptrunc_functor n f₀₁) (ptrunc_functor n f₂₁) :=
-  !ptrunc_functor_pcompose⁻¹* ⬝* ptrunc_functor_phomotopy n p ⬝* !ptrunc_functor_pcompose
-
-  definition homotopy_group_functor_psquare (n : ℕ) (p : psquare f₁₀ f₁₂ f₀₁ f₂₁) :
-        psquare (π→[n] f₁₀) (π→[n] f₁₂) (π→[n] f₀₁) (π→[n] f₂₁) :=
-  !homotopy_group_functor_compose⁻¹* ⬝* homotopy_group_functor_phomotopy n p ⬝*
-  !homotopy_group_functor_compose
-
-  definition homotopy_group_homomorphism_psquare (n : ℕ) [H : is_succ n]
-    (p : psquare f₁₀ f₁₂ f₀₁ f₂₁) : hsquare (π→g[n] f₁₀) (π→g[n] f₁₂) (π→g[n] f₀₁) (π→g[n] f₂₁) :=
-  begin
-    induction H with n, exact to_homotopy (ptrunc_functor_psquare 0 (apn_psquare (succ n) p))
-  end
-
-  end psquare
-
   definition punit_pmap_phomotopy [constructor] {A : Type*} (f : punit →* A) :
     f ~* pconst punit A :=
   !phomotopy_of_is_contr_dom
@@ -181,7 +69,7 @@ namespace pointed
       : sigma_equiv_sigma_right (λp, eq_equiv_eq_symm _ _)
       ... ≃ Σ(p : to_homotopy h = to_homotopy k),
       whisker_right (respect_pt g) (apd10 p pt) ⬝ to_homotopy_pt k = to_homotopy_pt h
-      : sigma_equiv_sigma_right (λp, equiv_eq_closed_left _ (whisker_right _ !whisker_right_ap⁻¹))
+      : by exact sigma_equiv_sigma_right (λp, equiv_eq_closed_left _ (whisker_right _ (!whisker_right_ap⁻¹ᵖ)))
       ... ≃ Σ(p : to_homotopy h ~ to_homotopy k),
       whisker_right (respect_pt g) (p pt) ⬝ to_homotopy_pt k = to_homotopy_pt h
       : sigma_equiv_sigma_left' eq_equiv_homotopy
@@ -974,15 +862,42 @@ namespace pointed
   definition pequiv_eq {f g : A ≃* B} (H : f ~* g) : f = g :=
   (pequiv_eq_equiv f g)⁻¹ᵉ H
 
-  open algebra
+  definition pequiv.sigma_char_equiv [constructor] (X Y : Type*) :
-  definition pequiv_of_isomorphism_of_eq {G₁ G₂ : Group} (p : G₁ = G₂) :
+    (X ≃* Y) ≃ Σ(e : X ≃ Y), e pt = pt :=
-    pequiv_of_isomorphism (isomorphism_of_eq p) = pequiv_of_eq (ap pType_of_Group p) :=
   begin
-    induction p,
+    fapply equiv.MK,
-    apply pequiv_eq,
+    { intro e, exact ⟨equiv_of_pequiv e, respect_pt e⟩ },
-    fapply phomotopy.mk,
+    { intro e, exact pequiv_of_equiv e.1 e.2 },
-    { intro g, reflexivity },
+    { intro e, induction e with e p, fapply sigma_eq,
-    { apply is_prop.elim }
+      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

hott/types/sigma.hlean

@@ -120,6 +120,10 @@ namespace sigma
     sigma_eq (p1 ⬝ p2) (q1 ⬝o q2) = sigma_eq p1 q1 ⬝ sigma_eq p2 q2 :=
   by induction u; induction v; induction w; apply dpair_eq_dpair_con
 
+  definition dpair_eq_dpair_inv {A : Type} {B : A → Type} {a a' : A} {b : B a} {b' : B a'} (p : a = a')
+    (q : b =[p] b') : (dpair_eq_dpair p q)⁻¹ = dpair_eq_dpair p⁻¹ q⁻¹ᵒ :=
+  begin induction q, reflexivity end
+
   local attribute dpair_eq_dpair [reducible]
   definition dpair_eq_dpair_con_idp (p : a = a') (q : b =[p] b') :
     dpair_eq_dpair p q = dpair_eq_dpair p !pathover_tr ⬝
@@ -466,23 +470,21 @@ namespace sigma
 
   /- *** The negative universal property. -/
 
-  protected definition coind_unc (fg : Σ(f : Πa, B a), Πa, C a (f a)) (a : A)
+  protected definition coind_unc [constructor] (fg : Σ(f : Πa, B a), Πa, C a (f a)) (a : A)
     : Σ(b : B a), C a b :=
   ⟨fg.1 a, fg.2 a⟩
 
-  protected definition coind (f : Π a, B a) (g : Π a, C a (f a)) (a : A) : Σ(b : B a), C a b :=
+  protected definition coind [constructor] (f : Π a, B a) (g : Π a, C a (f a)) (a : A) : Σ(b : B a), C a b :=
   sigma.coind_unc ⟨f, g⟩ a
 
-  --is the instance below dangerous?
+  definition is_equiv_coind [constructor] (C : Πa, B a → Type)
-  --in Coq this can be done without function extensionality
-  definition is_equiv_coind [instance] (C : Πa, B a → Type)
     : is_equiv (@sigma.coind_unc _ _ C) :=
   adjointify _ (λ h, ⟨λa, (h a).1, λa, (h a).2⟩)
                (λ h, proof eq_of_homotopy (λu, !sigma.eta) qed)
                (λfg, destruct fg (λ(f : Π (a : A), B a) (g : Π (x : A), C x (f x)), proof idp qed))
 
-  definition sigma_pi_equiv_pi_sigma : (Σ(f : Πa, B a), Πa, C a (f a)) ≃ (Πa, Σb, C a b) :=
+  definition sigma_pi_equiv_pi_sigma [constructor] : (Σ(f : Πa, B a), Πa, C a (f a)) ≃ (Πa, Σb, C a b) :=
-  equiv.mk sigma.coind_unc _
+  equiv.mk sigma.coind_unc !is_equiv_coind
   end
 
   /- Subtypes (sigma types whose second components are props) -/

hott/types/trunc.hlean

@@ -8,10 +8,10 @@ Properties of trunc_index, is_trunc, trunctype, trunc, and the pointed versions
 
 -- NOTE: the fact that (is_trunc n A) is a mere proposition is proved in .prop_trunc
 
-import .pointed ..function algebra.order types.nat.order types.unit
+import .pointed2 ..function algebra.order types.nat.order types.unit types.int.hott
 
 open eq sigma sigma.ops pi function equiv trunctype
-     is_equiv prod pointed nat is_trunc algebra sum unit
+     is_equiv prod pointed nat is_trunc algebra unit
 
   /- basic computation with ℕ₋₂, its operations and its order -/
 namespace trunc_index
@@ -71,6 +71,7 @@ namespace trunc_index
   le.step (trunc_index.le.tr_refl n)
 
   -- the order is total
+  open sum
   protected theorem le_sum_le (n m : ℕ₋₂) : n ≤ m ⊎ m ≤ n :=
   begin
     induction m with m IH,
@@ -185,6 +186,23 @@ namespace trunc_index
   definition of_nat_add_two (n : ℕ₋₂) : of_nat (add_two n) = n.+2 :=
   begin induction n with n IH, reflexivity, exact ap succ IH end
 
+  lemma minus_two_add_plus_two (n : ℕ₋₂) : -2+2+n = n :=
+  by induction n with n p; reflexivity; exact ap succ p
+
+  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
+
   definition of_nat_le_of_nat {n m : ℕ} (H : n ≤ m) : (of_nat n ≤ of_nat m) :=
   begin
     induction H with m H IH,
@@ -218,6 +236,13 @@ namespace trunc_index
     exact le_of_succ_le_succ (le_of_succ_le_succ H)
   end
 
+  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
+
   protected theorem succ_le_of_not_le {n m : ℕ₋₂} (H : ¬ n ≤ m) : m.+1 ≤ n :=
   begin
     cases (le.total n m) with H2 H2,
@@ -238,6 +263,15 @@ namespace trunc_index
     right, intro H2, apply H, exact le_of_succ_le_succ H2
   end
 
+  protected definition pred [unfold 1] (n : ℕ₋₂) : ℕ₋₂ :=
+  begin cases n with n, exact -2, exact n end
+
+  definition trunc_index_equiv_nat [constructor] : ℕ₋₂ ≃ ℕ :=
+  equiv.MK add_two sub_two add_two_sub_two sub_two_add_two
+
+  definition is_set_trunc_index [instance] : is_set ℕ₋₂ :=
+  is_trunc_equiv_closed_rev 0 trunc_index_equiv_nat
+
 end trunc_index open trunc_index
 
 namespace is_trunc
@@ -447,8 +481,7 @@ namespace is_trunc
     apply iff.mp !is_trunc_iff_is_contr_loop H
   end
 
-  -- rename to is_trunc_loopn_of_is_trunc
+  theorem is_trunc_loopn_of_is_trunc (n : ℕ₋₂) (k : ℕ) (A : Type*) [H : is_trunc n A] :
-  theorem is_trunc_loop_of_is_trunc (n : ℕ₋₂) (k : ℕ) (A : Type*) [H : is_trunc n A] :
     is_trunc n (Ω[k] A) :=
   begin
     induction k with k IH,
@@ -463,9 +496,20 @@ namespace is_trunc
     apply is_trunc_eq, apply IH, rewrite [succ_add_nat, add_nat_succ at H], exact H
   end
 
+  lemma is_trunc_loopn_nat (n m : ℕ) (A : Type*) [H : is_trunc (n + m) A] :
+    is_trunc n (Ω[m] A) :=
+  @is_trunc_loopn n m A (transport (λk, is_trunc k _) (of_nat_add_of_nat n m)⁻¹ H)
+
   definition is_set_loopn (n : ℕ) (A : Type*) [is_trunc n A] : is_set (Ω[n] A) :=
-  have is_trunc (0+[ℕ₋₂]n) A, by rewrite [trunc_index.zero_add]; exact _,
+  have is_trunc (0+n) A, by rewrite [zero_add]; exact _,
-  is_trunc_loopn 0 n A
+  is_trunc_loopn_nat 0 n A
+
+  lemma is_trunc_loop_nat (n : ℕ) (A : Type*) [H : is_trunc (n + 1) A] :
+    is_trunc n (Ω A) :=
+  is_trunc_loop A n
+
+  definition is_trunc_of_eq {n m : ℕ₋₂} (p : n = m) {A : Type} (H : is_trunc n A) : is_trunc m A :=
+  transport (λk, is_trunc k A) p H
 
   definition pequiv_punit_of_is_contr [constructor] (A : Type*) (H : is_contr A) : A ≃* punit :=
   pequiv_of_equiv (equiv_unit_of_is_contr A) (@is_prop.elim unit _ _ _)
@@ -623,8 +667,8 @@ namespace trunc
   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},
+    { intro x, induction x with x, induction x with x, exact tr x },
-    { intro x, induction x with x, exact tr (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
@@ -663,6 +707,17 @@ namespace trunc
     induction x with x, esimp, exact ap tr (p x)
   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₂₂}
+
+  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
+
+  end hsquare
+
   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) ∘
@@ -693,6 +748,13 @@ namespace trunc
   definition ptrunc [constructor] (n : ℕ₋₂) (X : Type*) : n-Type* :=
   ptrunctype.mk (trunc n X) _ (tr pt)
 
+  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 is_contr_ptrunc_minus_one (A : Type*) : is_contr (ptrunc -1 A) :=
+  is_contr_of_inhabited_prop pt
+
   /- pointed maps involving ptrunc -/
   definition ptrunc_functor [constructor] {X Y : Type*} (n : ℕ₋₂) (f : X →* Y)
     : ptrunc n X →* ptrunc n Y :=
@@ -708,6 +770,11 @@ namespace trunc
     ptrunc n X →* Y :=
   pmap.mk (trunc.elim f) (respect_pt f)
 
+  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)
+
   /- pointed equivalences involving ptrunc -/
   definition ptrunc_pequiv_ptrunc [constructor] (n : ℕ₋₂) {X Y : Type*} (H : X ≃* Y)
     : ptrunc n X ≃* ptrunc n Y :=
@@ -735,6 +802,10 @@ namespace trunc
     : ptrunc n (ptrunc m A) ≃* ptrunc m (ptrunc n A) :=
   pequiv_of_equiv (trunc_trunc_equiv_trunc_trunc n m A) idp
 
+  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 loop_ptrunc_pequiv [constructor] (n : ℕ₋₂) (A : Type*) :
     Ω (ptrunc (n+1) A) ≃* ptrunc n (Ω A) :=
   pequiv_of_equiv !tr_eq_tr_equiv idp
@@ -756,6 +827,10 @@ namespace trunc
       exact loopn_pequiv_loopn k (pequiv_of_eq (ap (λn, ptrunc n A) !succ_add_nat⁻¹)) }
   end
 
+  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_con {n : ℕ₋₂} {k : ℕ} {A : Type*}
     (p q : Ω[succ k] (ptrunc (n+succ k) A)) :
     loopn_ptrunc_pequiv n (succ k) A (p ⬝ q) =
@@ -870,6 +945,114 @@ namespace trunc
     { esimp, exact !idp_con ⬝ whisker_right _ !ap_compose },
   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
+
+  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 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 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
+
+  section psquare
+  variables {A₀₀ A₂₀ A₀₂ A₂₂ : Type*}
+            {f₁₀ : A₀₀ →* A₂₀} {f₁₂ : A₀₂ →* A₂₂}
+            {f₀₁ : A₀₀ →* A₀₂} {f₂₁ : A₂₀ →* A₂₂}
+
+  definition ptrunc_functor_psquare (n : ℕ₋₂) (p : psquare f₁₀ f₁₂ f₀₁ f₂₁) :
+    psquare (ptrunc_functor n f₁₀) (ptrunc_functor n f₁₂)
+            (ptrunc_functor n f₀₁) (ptrunc_functor n f₂₁) :=
+  !ptrunc_functor_pcompose⁻¹* ⬝* ptrunc_functor_phomotopy n p ⬝* !ptrunc_functor_pcompose
+
+  end psquare
+
+  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)⁻¹ᵉ
+
+  -- The following pointed equivalence can be defined more easily, but now we get the right maps definitionally
+  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
+
+  /- 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 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 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_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 Prop_eq {P Q : Prop} (H : P ↔ Q) : P = Q :=
+  tua (equiv_of_is_prop (iff.mp H) (iff.mpr H))
+
 end trunc open trunc
 
 /- The truncated encode-decode method -/
@@ -950,3 +1133,124 @@ namespace function
   -- a homotopy group.
 
 end function
+
+/- functions between ℤ and ℕ₋₂ -/
+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