diff --git a/hott/init/path.hlean b/hott/init/path.hlean
index 6b98187dc5..d1dfac72e7 100644
--- a/hott/init/path.hlean
+++ b/hott/init/path.hlean
@@ -498,6 +498,7 @@ namespace eq
 
   -- Transporting in a pulled back fibration.
   -- TODO: P can probably be implicit
+  -- rename: tr_compose
   definition transport_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
diff --git a/hott/init/reserved_notation.hlean b/hott/init/reserved_notation.hlean
index ed6198e231..2207e12f8e 100644
--- a/hott/init/reserved_notation.hlean
+++ b/hott/init/reserved_notation.hlean
@@ -97,7 +97,7 @@ reserve infixl `++`:65
 reserve infixr `::`:65
 
 -- Yet another trick to anotate an expression with a type
-definition is_typeof (A : Type) (a : A) : A := a
+abbreviation is_typeof (A : Type) (a : A) : A := a
 
 notation `typeof` t `:` T  := is_typeof T t
 notation `(` t `:` T `)`  := is_typeof T t
diff --git a/hott/types/sigma.hlean b/hott/types/sigma.hlean
index 8bdaa1b11b..f71c5c9fba 100644
--- a/hott/types/sigma.hlean
+++ b/hott/types/sigma.hlean
@@ -321,7 +321,7 @@ namespace sigma
 
   section
   definition is_equiv_sigma_rec [instance] (C : (Σa, B a) → Type)
-    : is_equiv (@sigma.rec _ _ C) :=
+    : is_equiv (sigma.rec : (Πa b, C ⟨a, b⟩) → Πab, C ab) :=
   adjointify _ (λ g a b, g ⟨a, b⟩)
                (λ g, proof eq_of_homotopy (λu, destruct u (λa b, idp)) qed)
                (λ f, refl f)
diff --git a/library/init/reserved_notation.lean b/library/init/reserved_notation.lean
index d72424a811..c511cb0e63 100644
--- a/library/init/reserved_notation.lean
+++ b/library/init/reserved_notation.lean
@@ -94,7 +94,7 @@ reserve infixl `++`:65
 reserve infixr `::`:65
 
 -- Yet another trick to anotate an expression with a type
-definition is_typeof (A : Type) (a : A) : A := a
+abbreviation is_typeof (A : Type) (a : A) : A := a
 
 notation `typeof` t `:` T  := is_typeof T t
 notation `(` t `:` T `)`  := is_typeof T t