diff --git a/library/standard.lean b/library/standard.lean
index 6e28175c65..68fdba1c64 100644
--- a/library/standard.lean
+++ b/library/standard.lean
@@ -7,4 +7,4 @@
 
 -- The constructive core of Lean's library.
 
-import logic data tools.tactic
+import type logic data tools.tactic
diff --git a/library/type.lean b/library/type.lean
new file mode 100644
index 0000000000..bdbc8fc664
--- /dev/null
+++ b/library/type.lean
@@ -0,0 +1,7 @@
+-- Copyright (c) 2014 Microsoft Corporation. All rights reserved.
+-- Released under Apache 2.0 license as described in the file LICENSE.
+-- Authors: Leonardo de Moura
+
+definition Type₁ [reducible] := Type.{1}
+definition Type₂ [reducible] := Type.{2}
+definition Type₃ [reducible] := Type.{3}