diff --git a/hott/algebra/category/functor.hlean b/hott/algebra/category/functor.hlean
index bd7e7dcbe..d1c40587d 100644
--- a/hott/algebra/category/functor.hlean
+++ b/hott/algebra/category/functor.hlean
@@ -154,7 +154,7 @@ namespace functor
   by (cases F; apply functor_mk_eq'_idp)
 
   definition functor_eq_eta' {F₁ F₂ : C ⇒ D} (p : F₁ = F₂)
-      : functor_eq' (ap to_fun_ob p) (!transport_compose⁻¹ ⬝ apd to_fun_hom p) = p :=
+      : functor_eq' (ap to_fun_ob p) (!tr_compose⁻¹ ⬝ apd to_fun_hom p) = p :=
   begin
     cases p, cases F₁,
     apply concat, rotate_left 1, apply functor_eq'_idp,
diff --git a/hott/init/equiv.hlean b/hott/init/equiv.hlean
index 638f9676d..6d94fed01 100644
--- a/hott/init/equiv.hlean
+++ b/hott/init/equiv.hlean
@@ -177,7 +177,7 @@ namespace is_equiv
       is_equiv_rect f P df (f x)
             = right_inv f (f x) ▸ df (f⁻¹ (f x))   : by esimp
         ... = ap f (left_inv f x) ▸ df (f⁻¹ (f x)) : by rewrite -adj
-        ... = left_inv f x ▸ df (f⁻¹ (f x))        : by rewrite -transport_compose
+        ... = left_inv f x ▸ df (f⁻¹ (f x))        : by rewrite -tr_compose
         ... = df x                                 : by rewrite (apd df (left_inv f x))
 
   end
@@ -295,7 +295,7 @@ namespace equiv
       equiv_rect f P df (f x)
             = right_inv f (f x) ▸ df (f⁻¹ (f x))   : by esimp
         ... = ap f (left_inv f x) ▸ df (f⁻¹ (f x)) : by rewrite -adj
-        ... = left_inv f x ▸ df (f⁻¹ (f x))        : by rewrite -transport_compose
+        ... = left_inv f x ▸ df (f⁻¹ (f x))        : by rewrite -tr_compose
         ... = df x                                 : by rewrite (apd df (left_inv f x))
 
 
diff --git a/hott/init/path.hlean b/hott/init/path.hlean
index d9d122d8e..385f37682 100644
--- a/hott/init/path.hlean
+++ b/hott/init/path.hlean
@@ -509,8 +509,7 @@ namespace eq
   eq.rec_on r !idp_con⁻¹
 
   -- Transporting in a pulled back fibration.
-  -- rename: tr_compose
-  definition transport_compose (P : B → Type) (f : A → B) (p : x = y) (z : P (f x)) :
+  definition tr_compose (P : B → Type) (f : A → B) (p : x = y) (z : P (f x)) :
     transport (P ∘ f) p z  =  transport P (ap f p) z :=
   eq.rec_on p idp
 
@@ -526,7 +525,7 @@ namespace eq
     apd10 (ap (λh : A → B, f ∘ h) p) a = ap f (apd10 p a) :=
   eq.rec_on p idp
 
-  -- A special case of [transport_compose] which seems to come up a lot.
+  -- A special case of [tr_compose] which seems to come up a lot.
   definition tr_eq_cast_ap {P : A → Type} {x y} (p : x = y) (u : P x) : p ▸ u = cast (ap P p) u :=
   eq.rec_on p idp
 
diff --git a/hott/types/pi.hlean b/hott/types/pi.hlean
index 6a23b1169..a5acee324 100644
--- a/hott/types/pi.hlean
+++ b/hott/types/pi.hlean
@@ -175,7 +175,7 @@ namespace pi
           (λ(a : A) (b' : B' (f0⁻¹ a)), transport B (right_inv f0 a) ((f1 (f0⁻¹ a))⁻¹ b')))),
     begin
       intro h, apply eq_of_homotopy, intro a', esimp,
-      rewrite [adj f0 a',-transport_compose,fn_tr_eq_tr_fn _ f1,right_inv (f1 _)],
+      rewrite [adj f0 a',-tr_compose,fn_tr_eq_tr_fn _ f1,right_inv (f1 _)],
       apply apd
     end,
     begin
diff --git a/hott/types/sigma.hlean b/hott/types/sigma.hlean
index e871109bd..f7decb8d3 100644
--- a/hott/types/sigma.hlean
+++ b/hott/types/sigma.hlean
@@ -216,7 +216,7 @@ namespace sigma
     apply (sigma_eq (left_inv f a)),
     apply pathover_of_tr_eq,
     rewrite [▸*,adj f,-(fn_tr_eq_tr_fn (left_inv f a) (λ a, (g a)⁻¹)),
-             ▸*,transport_compose B' f,tr_inv_tr,left_inv]
+             ▸*,tr_compose B' f,tr_inv_tr,left_inv]
   end
 
   definition sigma_equiv_sigma_of_is_equiv [H1 : is_equiv f] [H2 : Π a, is_equiv (g a)]
@@ -237,7 +237,7 @@ namespace sigma
   -- definition ap_sigma_functor_eq (p : u.1 = v.1) (q : u.2 =[p] v.2)
   --   : ap (sigma_functor f g) (sigma_eq p q) =
   --     sigma_eq (ap f p)
-  --      ((transport_compose B' f p (g u.1 u.2))⁻¹ ⬝ (fn_tr_eq_tr_fn p g u.2)⁻¹ ⬝ ap (g v.1) q) :=
+  --      ((tr_compose B' f p (g u.1 u.2))⁻¹ ⬝ (fn_tr_eq_tr_fn p g u.2)⁻¹ ⬝ ap (g v.1) q) :=
   -- by induction u; induction v; apply ap_sigma_functor_eq_dpair
 
   /- definition 3.11.9(i): Summing up a contractible family of types does nothing. -/