diff --git a/hott/init/reserved_notation.hlean b/hott/init/reserved_notation.hlean
index 741c6f9ad..a8f96c8f5 100644
--- a/hott/init/reserved_notation.hlean
+++ b/hott/init/reserved_notation.hlean
@@ -100,3 +100,4 @@ reserve infixr `::`:65
 definition 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/library/init/reserved_notation.lean b/library/init/reserved_notation.lean
index cb024df83..3c17d9d48 100644
--- a/library/init/reserved_notation.lean
+++ b/library/init/reserved_notation.lean
@@ -97,3 +97,4 @@ reserve infixr `::`:65
 definition is_typeof (A : Type) (a : A) : A := a
 
 notation `typeof` t `:` T  := is_typeof T t
+notation `(` t `:` T `)`  := is_typeof T t