fix(reserved_notation): make is_typeof an abbreviation

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

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

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)

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