From 60ae9f627ca2b6b3f0dd9e15b09857e625cff308 Mon Sep 17 00:00:00 2001
From: Floris van Doorn <fpv@andrew.cmu.edu>
Date: Thu, 9 Apr 2015 22:14:19 -0400
Subject: [PATCH] feat(hott): add core.hlean and types/default.hlean

---
 hott/core.hlean          | 11 +++++++++++
 hott/hott.md             |  2 ++
 hott/types/default.hlean | 11 +++++++++++
 hott/types/types.md      |  2 +-
 4 files changed, 25 insertions(+), 1 deletion(-)
 create mode 100644 hott/core.hlean
 create mode 100644 hott/types/default.hlean

diff --git a/hott/core.hlean b/hott/core.hlean
new file mode 100644
index 0000000000..42d8c57067
--- /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 e1d4270de9..69b975cf81 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 0000000000..d4947f6d32
--- /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 8fa5fbaa94..099d84cdec 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