diff --git a/hott/core.hlean b/hott/core.hlean
new file mode 100644
index 000000000..42d8c5706
--- /dev/null
+++ b/hott/core.hlean
@@ -0,0 +1,11 @@
+/-
+Copyright (c) 2015 Floris van Doorn. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Module: core
+Authors: Floris van Doorn
+
+The core of the HoTT library
+-/
+
+import types
diff --git a/hott/hott.md b/hott/hott.md
index e1d4270de..69b975cf8 100644
--- a/hott/hott.md
+++ b/hott/hott.md
@@ -14,6 +14,8 @@ Lean's homotopy type theory kernel is a version of Martin-Löf Type Theory with:
 * a non-cumulative hierarchy of universes, `Type 0`, `Type 1`, ... 
 * inductively defined types
 
+Note that there is no proof-irrelevant or impredicative universe.
+
 By default, the univalence axiom is declared on initialization.
 
 See also the [standard library](../library/library.md).
diff --git a/hott/types/default.hlean b/hott/types/default.hlean
new file mode 100644
index 000000000..d4947f6d3
--- /dev/null
+++ b/hott/types/default.hlean
@@ -0,0 +1,11 @@
+/-
+Copyright (c) 2015 Floris van Doorn. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Module: types.default
+Authors: Floris van Doorn
+
+The core of the HoTT library
+-/
+
+import .sigma .prod .pi .equiv .fiber .eq .trunc .arrow .pointed
diff --git a/hott/types/types.md b/hott/types/types.md
index 8fa5fbaa9..099d84cde 100644
--- a/hott/types/types.md
+++ b/hott/types/types.md
@@ -12,4 +12,4 @@ Various datatypes.
 * [fiber](fiber.hlean)
 * [equiv](equiv.hlean)
 * [pointed](pointed.hlean)
-* [W](W.hlean)
\ No newline at end of file
+* [W](W.hlean) (not loaded by default)
\ No newline at end of file