diff --git a/hott/homotopy/hopf.hlean b/hott/homotopy/hopf.hlean
index 77ab2b2b8..bfd8894c2 100644
--- a/hott/homotopy/hopf.hlean
+++ b/hott/homotopy/hopf.hlean
@@ -58,7 +58,7 @@ section
   definition hopf [unfold 4] : susp A → Type :=
   susp.elim_type A A (λa, equiv.mk (λx, a * x) !is_equiv_mul_left)
 
-  /- Lemma 8.5.7. The total space is A * A -/
+ /- Lemma 8.5.7. The total space is A * A -/
   open prod prod.ops
 
   protected definition total : sigma (hopf A) ≃ join A A :=
diff --git a/hott/init/equiv.hlean b/hott/init/equiv.hlean
index 7c68fe2d8..5f3dca246 100644
--- a/hott/init/equiv.hlean
+++ b/hott/init/equiv.hlean
@@ -346,11 +346,11 @@ namespace equiv
     : A ≃ B :=
   equiv.mk f (inv_homotopy_closed Heq)
 
-  --rename: eq_equiv_fn_eq_of_is_equiv
+  --rename: eq_equiv_fn_eq_fn_of_is_equiv
   definition eq_equiv_fn_eq [constructor] (f : A → B) [H : is_equiv f] (a b : A) : (a = b) ≃ (f a = f b) :=
   equiv.mk (ap f) !is_equiv_ap
 
-  --rename: eq_equiv_fn_eq
+  --rename: eq_equiv_fn_eq_fn
   definition eq_equiv_fn_eq_of_equiv [constructor] (f : A ≃ B) (a b : A) : (a = b) ≃ (f a = f b) :=
   equiv.mk (ap f) !is_equiv_ap
 
diff --git a/hott/init/path.hlean b/hott/init/path.hlean
index 727d4e48e..63ae94c84 100644
--- a/hott/init/path.hlean
+++ b/hott/init/path.hlean
@@ -470,6 +470,14 @@ namespace eq
     cast (ap P p⁻¹) (cast (ap P p) z) = z :=
   by induction p; reflexivity
 
+  definition fn_tr_eq_tr_fn {P Q : A → Type} {x y : A} (p : x = y) (f : Πx, P x → Q x) (z : P x) :
+    f y (p ▸ z) = p ▸ f x z :=
+  by induction p; reflexivity
+
+  definition fn_cast_eq_cast_fn {A : Type} {P Q : A → Type} {x y : A} (p : x = y)
+    (f : Πx, P x → Q x) (z : P x) : f y (cast (ap P p) z) = cast (ap Q p) (f x z) :=
+  by induction p; reflexivity
+
   definition con_con_tr {P : A → Type}
       {x y z w : A} (p : x = y) (q : y = z) (r : z = w) (u : P x) :
     ap (λe, e ▸ u) (con.assoc' p q r) ⬝ (con_tr (p ⬝ q) r u) ⬝
@@ -495,7 +503,6 @@ namespace eq
     : apdt f p⁻¹ = (eq_inv_tr_of_tr_eq (apdt f p))⁻¹ :=
   by cases p; apply idp
 
-
   -- Dependent transport in a doubly dependent type.
   -- This is a special case of transporto in init.pathover
   definition transportD [unfold 6] {P : A → Type} (Q : Πa, P a → Type)
@@ -544,14 +551,6 @@ namespace eq
     ap (transport P p) s  ⬝  transport2 P r w = transport2 P r z  ⬝  ap (transport P q) s :=
   by induction r; exact !idp_con⁻¹
 
-  definition fn_tr_eq_tr_fn {P Q : A → Type} {x y : A} (p : x = y) (f : Πx, P x → Q x) (z : P x) :
-    f y (p ▸ z) = p ▸ f x z :=
-  by induction p; reflexivity
-
-  definition fn_cast_eq_cast_fn {A : Type} {P Q : A → Type} {x y : A} (p : x = y)
-    (f : Πx, P x → Q x) (z : P x) : f y (cast (ap P p) z) = cast (ap Q p) (f x z) :=
-  by induction p; reflexivity
-
   /- Transporting in particular fibrations -/
 
   /-
diff --git a/hott/init/pathover.hlean b/hott/init/pathover.hlean
index 8a2e02b6e..c7b531b11 100644
--- a/hott/init/pathover.hlean
+++ b/hott/init/pathover.hlean
@@ -25,6 +25,9 @@ namespace eq
   definition idpo [reducible] [constructor] : b =[refl a] b :=
   pathover.idpatho b
 
+  definition idpatho [reducible] [constructor] (b : B a) : b =[refl a] b :=
+  pathover.idpatho b
+
   /- equivalences with equality using transport -/
   definition pathover_of_tr_eq [unfold 5 8] (r : p ▸ b = b₂) : b =[p] b₂ :=
   by cases p; cases r; constructor
diff --git a/hott/types/eq.hlean b/hott/types/eq.hlean
index ad06226a2..d0a4f1602 100644
--- a/hott/types/eq.hlean
+++ b/hott/types/eq.hlean
@@ -218,7 +218,7 @@ namespace eq
 
   /- [is_equiv_ap] is in init.equiv  -/
 
-  definition equiv_ap (f : A → B) [H : is_equiv f] (a₁ a₂ : A)
+  definition equiv_ap [constructor] (f : A → B) [H : is_equiv f] (a₁ a₂ : A)
     : (a₁ = a₂) ≃ (f a₁ = f a₂) :=
   equiv.mk (ap f) _
 
diff --git a/hott/types/pointed.hlean b/hott/types/pointed.hlean
index 73feb5d0e..d88745974 100644
--- a/hott/types/pointed.hlean
+++ b/hott/types/pointed.hlean
@@ -77,6 +77,9 @@ namespace pointed
     { intro x, induction x with X x, reflexivity},
   end
 
+  definition pType.eta_expand [constructor] (A : Type*) : Type* :=
+  pointed.MK A pt
+
   definition add_point [constructor] (A : Type) : Type* :=
   pointed.Mk (none : option A)
   postfix `₊`:(max+1) := add_point
@@ -156,6 +159,9 @@ namespace pointed
     all_goals reflexivity
   end
 
+  definition pmap.eta_expand [constructor] {A B : Type*} (f : A →* B) : A →* B :=
+  pmap.mk f (pmap.resp_pt f)
+
   definition pmap_eq (r : Πa, f a = g a) (s : respect_pt f = (r pt) ⬝ respect_pt g) : f = g :=
   begin
     cases f with f p, cases g with g q,
@@ -343,6 +349,9 @@ namespace pointed
     all_goals reflexivity
   end
 
+  definition phomotopy.eta_expand [constructor] {A B : Type*} {f g : A →* B} (p : f ~* g) : f ~* g :=
+  phomotopy.mk p (phomotopy.homotopy_pt p)
+
   definition is_trunc_pmap [instance] (n : ℕ₋₂) (A B : Type*) [is_trunc n B] :
     is_trunc n (A →* B) :=
   is_trunc_equiv_closed_rev _ !pmap.sigma_char
@@ -638,6 +647,9 @@ namespace pointed
     {a₁ a₂ : A} (p : a₁ = a₂) : pequiv_of_eq (ap C p) ∘* f a₁ ~* f a₂ ∘* pequiv_of_eq (ap B p) :=
   pcast_commute f p
 
+  definition pequiv.eta_expand [constructor] {A B : Type*} (f : A ≃* B) : A ≃* B :=
+  pequiv.mk f _ (pequiv.resp_pt f)
+
   /-
     the theorem pequiv_eq, which gives a condition for two pointed equivalences are equal
     is in types.equiv to avoid circular imports
@@ -936,7 +948,7 @@ namespace pointed
 
   variable {A}
 
-  theorem loopn_succ_in_con {n : ℕ} (p q : Ω[succ (succ n)] A) :
+  definition loopn_succ_in_con {n : ℕ} (p q : Ω[succ (succ n)] A) :
     loopn_succ_in A (succ n) (p ⬝ q) =
     loopn_succ_in A (succ n) p ⬝ loopn_succ_in A (succ n) q :=
   !loop_pequiv_loop_con
@@ -1006,7 +1018,7 @@ namespace pointed
   phomotopy.mk (λa, respect_pt f) (idp_con _)⁻¹
 
   definition pconst_pcompose [constructor] (f : A →* B) : pconst B C ∘* f ~* pconst A C :=
-  phomotopy.mk (λa, rfl) (ap_constant _ _)⁻¹
+  phomotopy.mk (λa, rfl) (ap_constant _ _)⁻
 
   definition ppcompose_right [constructor] (f : A →* B) : ppmap B C →* ppmap A C :=
   begin
diff --git a/hott/types/prod.hlean b/hott/types/prod.hlean
index cf9ea9cf8..a997fa9a9 100644
--- a/hott/types/prod.hlean
+++ b/hott/types/prod.hlean
@@ -154,9 +154,11 @@ namespace prod
   definition prod_equiv_prod [constructor] (f : A ≃ A') (g : B ≃ B') : A × B ≃ A' × B' :=
   equiv.mk (prod_functor f g) _
 
+  -- rename
   definition prod_equiv_prod_left [constructor] (g : B ≃ B') : A × B ≃ A × B' :=
   prod_equiv_prod equiv.rfl g
 
+  -- rename
   definition prod_equiv_prod_right [constructor] (f : A ≃ A') : A × B ≃ A' × B :=
   prod_equiv_prod f equiv.rfl