diff --git a/doc/lean/test_single.sh b/doc/lean/test_single.sh
index 0bd2a0fac..1de2a952b 100755
--- a/doc/lean/test_single.sh
+++ b/doc/lean/test_single.sh
@@ -6,7 +6,7 @@ if [ $# -ne 2 ]; then
 fi
 ulimit -s unlimited
 LEAN=$1
-export LEAN_PATH=.:../../library/standard
+export LEAN_PATH=.:../../library
 f=$2
 i=0
 in_code_block=0
diff --git a/library/Makefile b/library/Makefile
new file mode 100644
index 000000000..a1afdf7fe
--- /dev/null
+++ b/library/Makefile
@@ -0,0 +1 @@
+include Makefile.common
diff --git a/library/standard/data/bool.lean b/library/data/bool.lean
similarity index 100%
rename from library/standard/data/bool.lean
rename to library/data/bool.lean
diff --git a/library/standard/data/data.md b/library/data/data.md
similarity index 100%
rename from library/standard/data/data.md
rename to library/data/data.md
diff --git a/library/standard/data/default.lean b/library/data/default.lean
similarity index 100%
rename from library/standard/data/default.lean
rename to library/data/default.lean
diff --git a/library/standard/data/empty.lean b/library/data/empty.lean
similarity index 100%
rename from library/standard/data/empty.lean
rename to library/data/empty.lean
diff --git a/library/standard/data/int/basic.lean b/library/data/int/basic.lean
similarity index 100%
rename from library/standard/data/int/basic.lean
rename to library/data/int/basic.lean
diff --git a/library/standard/data/int/default.lean b/library/data/int/default.lean
similarity index 100%
rename from library/standard/data/int/default.lean
rename to library/data/int/default.lean
diff --git a/library/standard/data/int/int.md b/library/data/int/int.md
similarity index 100%
rename from library/standard/data/int/int.md
rename to library/data/int/int.md
diff --git a/library/standard/data/int/order.lean b/library/data/int/order.lean
similarity index 100%
rename from library/standard/data/int/order.lean
rename to library/data/int/order.lean
diff --git a/library/standard/data/list/basic.lean b/library/data/list/basic.lean
similarity index 100%
rename from library/standard/data/list/basic.lean
rename to library/data/list/basic.lean
diff --git a/library/standard/data/list/default.lean b/library/data/list/default.lean
similarity index 100%
rename from library/standard/data/list/default.lean
rename to library/data/list/default.lean
diff --git a/library/standard/data/list/list.md b/library/data/list/list.md
similarity index 100%
rename from library/standard/data/list/list.md
rename to library/data/list/list.md
diff --git a/library/standard/data/nat/basic.lean b/library/data/nat/basic.lean
similarity index 100%
rename from library/standard/data/nat/basic.lean
rename to library/data/nat/basic.lean
diff --git a/library/standard/data/nat/default.lean b/library/data/nat/default.lean
similarity index 100%
rename from library/standard/data/nat/default.lean
rename to library/data/nat/default.lean
diff --git a/library/standard/data/nat/div.lean b/library/data/nat/div.lean
similarity index 100%
rename from library/standard/data/nat/div.lean
rename to library/data/nat/div.lean
diff --git a/library/standard/data/nat/nat.md b/library/data/nat/nat.md
similarity index 100%
rename from library/standard/data/nat/nat.md
rename to library/data/nat/nat.md
diff --git a/library/standard/data/nat/order.lean b/library/data/nat/order.lean
similarity index 100%
rename from library/standard/data/nat/order.lean
rename to library/data/nat/order.lean
diff --git a/library/standard/data/nat/sub.lean b/library/data/nat/sub.lean
similarity index 100%
rename from library/standard/data/nat/sub.lean
rename to library/data/nat/sub.lean
diff --git a/library/standard/data/num.lean b/library/data/num.lean
similarity index 100%
rename from library/standard/data/num.lean
rename to library/data/num.lean
diff --git a/library/standard/data/option.lean b/library/data/option.lean
similarity index 100%
rename from library/standard/data/option.lean
rename to library/data/option.lean
diff --git a/library/standard/data/prod.lean b/library/data/prod.lean
similarity index 100%
rename from library/standard/data/prod.lean
rename to library/data/prod.lean
diff --git a/library/standard/data/quotient/aux.lean b/library/data/quotient/aux.lean
similarity index 100%
rename from library/standard/data/quotient/aux.lean
rename to library/data/quotient/aux.lean
diff --git a/library/standard/data/quotient/basic.lean b/library/data/quotient/basic.lean
similarity index 100%
rename from library/standard/data/quotient/basic.lean
rename to library/data/quotient/basic.lean
diff --git a/library/standard/data/quotient/classical.lean b/library/data/quotient/classical.lean
similarity index 100%
rename from library/standard/data/quotient/classical.lean
rename to library/data/quotient/classical.lean
diff --git a/library/standard/data/quotient/default.lean b/library/data/quotient/default.lean
similarity index 100%
rename from library/standard/data/quotient/default.lean
rename to library/data/quotient/default.lean
diff --git a/library/standard/data/quotient/quotient.md b/library/data/quotient/quotient.md
similarity index 100%
rename from library/standard/data/quotient/quotient.md
rename to library/data/quotient/quotient.md
diff --git a/library/standard/data/set.lean b/library/data/set.lean
similarity index 100%
rename from library/standard/data/set.lean
rename to library/data/set.lean
diff --git a/library/standard/data/sigma.lean b/library/data/sigma.lean
similarity index 100%
rename from library/standard/data/sigma.lean
rename to library/data/sigma.lean
diff --git a/library/standard/data/string.lean b/library/data/string.lean
similarity index 100%
rename from library/standard/data/string.lean
rename to library/data/string.lean
diff --git a/library/standard/data/subtype.lean b/library/data/subtype.lean
similarity index 100%
rename from library/standard/data/subtype.lean
rename to library/data/subtype.lean
diff --git a/library/standard/data/sum.lean b/library/data/sum.lean
similarity index 100%
rename from library/standard/data/sum.lean
rename to library/data/sum.lean
diff --git a/library/standard/data/unit.lean b/library/data/unit.lean
similarity index 100%
rename from library/standard/data/unit.lean
rename to library/data/unit.lean
diff --git a/library/standard/general_notation.lean b/library/general_notation.lean
similarity index 100%
rename from library/standard/general_notation.lean
rename to library/general_notation.lean
diff --git a/library/standard/hott/equiv.lean b/library/hott/equiv.lean
similarity index 100%
rename from library/standard/hott/equiv.lean
rename to library/hott/equiv.lean
diff --git a/library/standard/hott/fibrant.lean b/library/hott/fibrant.lean
similarity index 100%
rename from library/standard/hott/fibrant.lean
rename to library/hott/fibrant.lean
diff --git a/library/standard/hott/funext.lean b/library/hott/funext.lean
similarity index 100%
rename from library/standard/hott/funext.lean
rename to library/hott/funext.lean
diff --git a/library/standard/hott/hott.md b/library/hott/hott.md
similarity index 100%
rename from library/standard/hott/hott.md
rename to library/hott/hott.md
diff --git a/library/standard/hott/path.lean b/library/hott/path.lean
similarity index 100%
rename from library/standard/hott/path.lean
rename to library/hott/path.lean
diff --git a/library/standard/hott/trunc.lean b/library/hott/trunc.lean
similarity index 100%
rename from library/standard/hott/trunc.lean
rename to library/hott/trunc.lean
diff --git a/library/standard/logic/axioms/axioms.md b/library/logic/axioms/axioms.md
similarity index 100%
rename from library/standard/logic/axioms/axioms.md
rename to library/logic/axioms/axioms.md
diff --git a/library/standard/logic/axioms/classical.lean b/library/logic/axioms/classical.lean
similarity index 100%
rename from library/standard/logic/axioms/classical.lean
rename to library/logic/axioms/classical.lean
diff --git a/library/standard/logic/axioms/default.lean b/library/logic/axioms/default.lean
similarity index 100%
rename from library/standard/logic/axioms/default.lean
rename to library/logic/axioms/default.lean
diff --git a/library/standard/logic/axioms/examples/diaconescu.lean b/library/logic/axioms/examples/diaconescu.lean
similarity index 100%
rename from library/standard/logic/axioms/examples/diaconescu.lean
rename to library/logic/axioms/examples/diaconescu.lean
diff --git a/library/standard/logic/axioms/examples/examples.md b/library/logic/axioms/examples/examples.md
similarity index 100%
rename from library/standard/logic/axioms/examples/examples.md
rename to library/logic/axioms/examples/examples.md
diff --git a/library/standard/logic/axioms/funext.lean b/library/logic/axioms/funext.lean
similarity index 100%
rename from library/standard/logic/axioms/funext.lean
rename to library/logic/axioms/funext.lean
diff --git a/library/standard/logic/axioms/hilbert.lean b/library/logic/axioms/hilbert.lean
similarity index 100%
rename from library/standard/logic/axioms/hilbert.lean
rename to library/logic/axioms/hilbert.lean
diff --git a/library/standard/logic/axioms/piext.lean b/library/logic/axioms/piext.lean
similarity index 100%
rename from library/standard/logic/axioms/piext.lean
rename to library/logic/axioms/piext.lean
diff --git a/library/standard/logic/axioms/prop_decidable.lean b/library/logic/axioms/prop_decidable.lean
similarity index 100%
rename from library/standard/logic/axioms/prop_decidable.lean
rename to library/logic/axioms/prop_decidable.lean
diff --git a/library/standard/logic/classes/classes.md b/library/logic/classes/classes.md
similarity index 100%
rename from library/standard/logic/classes/classes.md
rename to library/logic/classes/classes.md
diff --git a/library/standard/logic/classes/decidable.lean b/library/logic/classes/decidable.lean
similarity index 100%
rename from library/standard/logic/classes/decidable.lean
rename to library/logic/classes/decidable.lean
diff --git a/library/standard/logic/classes/inhabited.lean b/library/logic/classes/inhabited.lean
similarity index 100%
rename from library/standard/logic/classes/inhabited.lean
rename to library/logic/classes/inhabited.lean
diff --git a/library/standard/logic/classes/nonempty.lean b/library/logic/classes/nonempty.lean
similarity index 100%
rename from library/standard/logic/classes/nonempty.lean
rename to library/logic/classes/nonempty.lean
diff --git a/library/standard/logic/connectives/basic.lean b/library/logic/connectives/basic.lean
similarity index 100%
rename from library/standard/logic/connectives/basic.lean
rename to library/logic/connectives/basic.lean
diff --git a/library/standard/logic/connectives/cast.lean b/library/logic/connectives/cast.lean
similarity index 100%
rename from library/standard/logic/connectives/cast.lean
rename to library/logic/connectives/cast.lean
diff --git a/library/standard/logic/connectives/connectives.md b/library/logic/connectives/connectives.md
similarity index 100%
rename from library/standard/logic/connectives/connectives.md
rename to library/logic/connectives/connectives.md
diff --git a/library/standard/logic/connectives/eq.lean b/library/logic/connectives/eq.lean
similarity index 100%
rename from library/standard/logic/connectives/eq.lean
rename to library/logic/connectives/eq.lean
diff --git a/library/standard/logic/connectives/examples/examples.md b/library/logic/connectives/examples/examples.md
similarity index 100%
rename from library/standard/logic/connectives/examples/examples.md
rename to library/logic/connectives/examples/examples.md
diff --git a/library/standard/logic/connectives/examples/instances_test.lean b/library/logic/connectives/examples/instances_test.lean
similarity index 100%
rename from library/standard/logic/connectives/examples/instances_test.lean
rename to library/logic/connectives/examples/instances_test.lean
diff --git a/library/standard/logic/connectives/identities.lean b/library/logic/connectives/identities.lean
similarity index 100%
rename from library/standard/logic/connectives/identities.lean
rename to library/logic/connectives/identities.lean
diff --git a/library/standard/logic/connectives/if.lean b/library/logic/connectives/if.lean
similarity index 100%
rename from library/standard/logic/connectives/if.lean
rename to library/logic/connectives/if.lean
diff --git a/library/standard/logic/connectives/instances.lean b/library/logic/connectives/instances.lean
similarity index 100%
rename from library/standard/logic/connectives/instances.lean
rename to library/logic/connectives/instances.lean
diff --git a/library/standard/logic/connectives/prop.lean b/library/logic/connectives/prop.lean
similarity index 100%
rename from library/standard/logic/connectives/prop.lean
rename to library/logic/connectives/prop.lean
diff --git a/library/standard/logic/connectives/quantifiers.lean b/library/logic/connectives/quantifiers.lean
similarity index 100%
rename from library/standard/logic/connectives/quantifiers.lean
rename to library/logic/connectives/quantifiers.lean
diff --git a/library/standard/logic/default.lean b/library/logic/default.lean
similarity index 100%
rename from library/standard/logic/default.lean
rename to library/logic/default.lean
diff --git a/library/standard/logic/examples/examples.md b/library/logic/examples/examples.md
similarity index 100%
rename from library/standard/logic/examples/examples.md
rename to library/logic/examples/examples.md
diff --git a/library/standard/logic/examples/nuprl_examples.lean b/library/logic/examples/nuprl_examples.lean
similarity index 100%
rename from library/standard/logic/examples/nuprl_examples.lean
rename to library/logic/examples/nuprl_examples.lean
diff --git a/library/standard/logic/logic.md b/library/logic/logic.md
similarity index 100%
rename from library/standard/logic/logic.md
rename to library/logic/logic.md
diff --git a/library/standard/standard.lean b/library/standard.lean
similarity index 100%
rename from library/standard/standard.lean
rename to library/standard.lean
diff --git a/library/standard/standard.md b/library/standard.md
similarity index 100%
rename from library/standard/standard.md
rename to library/standard.md
diff --git a/library/standard/Makefile b/library/standard/Makefile
deleted file mode 100644
index 0a42375f1..000000000
--- a/library/standard/Makefile
+++ /dev/null
@@ -1 +0,0 @@
-include ../Makefile.common
diff --git a/library/standard/struc/binary.lean b/library/struc/binary.lean
similarity index 100%
rename from library/standard/struc/binary.lean
rename to library/struc/binary.lean
diff --git a/library/standard/struc/function.lean b/library/struc/function.lean
similarity index 100%
rename from library/standard/struc/function.lean
rename to library/struc/function.lean
diff --git a/library/standard/struc/relation.lean b/library/struc/relation.lean
similarity index 100%
rename from library/standard/struc/relation.lean
rename to library/struc/relation.lean
diff --git a/library/standard/struc/struc.md b/library/struc/struc.md
similarity index 100%
rename from library/standard/struc/struc.md
rename to library/struc/struc.md
diff --git a/library/standard/struc/wf.lean b/library/struc/wf.lean
similarity index 100%
rename from library/standard/struc/wf.lean
rename to library/struc/wf.lean
diff --git a/library/standard/tools/fake_simplifier.lean b/library/tools/fake_simplifier.lean
similarity index 100%
rename from library/standard/tools/fake_simplifier.lean
rename to library/tools/fake_simplifier.lean
diff --git a/library/standard/tools/helper_tactics.lean b/library/tools/helper_tactics.lean
similarity index 100%
rename from library/standard/tools/helper_tactics.lean
rename to library/tools/helper_tactics.lean
diff --git a/library/standard/tools/tactic.lean b/library/tools/tactic.lean
similarity index 100%
rename from library/standard/tools/tactic.lean
rename to library/tools/tactic.lean
diff --git a/library/standard/tools/tools.md b/library/tools/tools.md
similarity index 100%
rename from library/standard/tools/tools.md
rename to library/tools/tools.md
diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index b91d8ea7c..d1f3df49a 100644
--- a/src/CMakeLists.txt
+++ b/src/CMakeLists.txt
@@ -311,9 +311,9 @@ if((${CYGWIN} EQUAL "1") OR (NOT (${CMAKE_SYSTEM_NAME} MATCHES "Windows")))
   # Only build libraries if we are NOT cross compiling
   add_custom_target(
     standard_lib ALL
-    COMMAND make -j ${PROCESSOR_COUNT} LEAN_PATH=.:${LEAN_SOURCE_DIR}/../library/standard LEAN="${CMAKE_SOURCE_DIR}/../bin/lean"
+    COMMAND make -j ${PROCESSOR_COUNT} LEAN_PATH=.:${LEAN_SOURCE_DIR}/../library LEAN="${CMAKE_SOURCE_DIR}/../bin/lean"
     DEPENDS ${CMAKE_BINARY_DIR}/shell/lean
-    WORKING_DIRECTORY ${LEAN_SOURCE_DIR}/../library/standard
+    WORKING_DIRECTORY ${LEAN_SOURCE_DIR}/../library
     )
 endif()
 
diff --git a/src/shell/lean.cpp b/src/shell/lean.cpp
index 752929678..9d24f8856 100644
--- a/src/shell/lean.cpp
+++ b/src/shell/lean.cpp
@@ -21,7 +21,6 @@ Author: Leonardo de Moura
 #include "kernel/kernel_exception.h"
 #include "kernel/formatter.h"
 #include "library/standard_kernel.h"
-#include "library/hott_kernel.h"
 #include "library/module.h"
 #include "library/io_state_stream.h"
 #include "library/definition_cache.h"
@@ -43,7 +42,6 @@ using lean::io_state;
 using lean::io_state_stream;
 using lean::regular;
 using lean::mk_environment;
-using lean::mk_hott_environment;
 using lean::set_environment;
 using lean::set_io_state;
 using lean::definition_cache;
@@ -81,7 +79,6 @@ static void display_help(std::ostream & out) {
     std::cout << "  --trust=num -t    trust level (default: 0) \n";
     std::cout << "  --quiet -q        do not print verbose messages\n";
     std::cout << "  --server          start Lean in 'server' mode\n";
-    std::cout << "  --hott            use Homotopy Type Theory kernel and libraries\n";
     std::cout << "  --threads=num -j  number of threads used to process lean files\n";
     std::cout << "  --deps            just print dependencies of a Lean input\n";
     std::cout << "  --flycheck        print structured error message for flycheck\n";
@@ -119,7 +116,6 @@ static struct option g_long_options[] = {
     {"trust",       required_argument, 0, 't'},
     {"server",      no_argument,       0, 'S'},
     {"quiet",       no_argument,       0, 'q'},
-    {"hott",        no_argument,       0, 'H'},
     {"threads",     required_argument, 0, 'j'},
     {"cache",       required_argument, 0, 'c'},
     {"deps",        no_argument,       0, 'D'},
@@ -133,13 +129,11 @@ static struct option g_long_options[] = {
 };
 
 #if defined(LEAN_USE_BOOST)
-static char const * g_opt_str = "PFDHSqlupgvhj:012k:012s:012t:012o:c:i:";
+static char const * g_opt_str = "PFDSqlupgvhj:012k:012s:012t:012o:c:i:";
 #else
-static char const * g_opt_str = "PFDHSqlupgvhj:012k:012t:012o:c:i:";
+static char const * g_opt_str = "PFDSqlupgvhj:012k:012t:012o:c:i:";
 #endif
 
-enum class lean_mode { Standard, HoTT };
-
 class simple_pos_info_provider : public pos_info_provider {
     char const * m_fname;
 public:
@@ -160,7 +154,6 @@ int main(int argc, char ** argv) {
     bool only_deps       = false;
     bool flycheck        = false;
     bool permissive      = false;
-    lean_mode mode       = lean_mode::Standard;
     unsigned num_threads = 1;
     bool use_cache       = false;
     bool gen_index       = false;
@@ -176,10 +169,6 @@ int main(int argc, char ** argv) {
         case 'j':
             num_threads = atoi(optarg);
             break;
-        case 'H':
-            mode = lean_mode::HoTT;
-            lean::init_lean_path("hott");
-            break;
         case 'S':
             server = true;
             break;
@@ -240,7 +229,7 @@ int main(int argc, char ** argv) {
         }
     }
 
-    environment env = mode == lean_mode::Standard ? mk_environment(trust_lvl) : mk_hott_environment(trust_lvl);
+    environment env = mk_environment(trust_lvl);
     io_state ios(lean::mk_pretty_formatter_factory());
     if (quiet)
         ios.set_option("verbose", false);
diff --git a/src/util/lean_path.cpp b/src/util/lean_path.cpp
index 1d960abb5..b7cb8df2e 100644
--- a/src/util/lean_path.cpp
+++ b/src/util/lean_path.cpp
@@ -107,13 +107,13 @@ std::string get_path(std::string f) {
 
 static std::string              g_lean_path;
 static std::vector<std::string> g_lean_path_vector;
-void init_lean_path(char const * kernel_instance_name) {
+void init_lean_path() {
     char * r = getenv("LEAN_PATH");
     if (r == nullptr) {
         g_lean_path  = ".";
         std::string exe_path = get_path(get_exe_location());
         g_lean_path += g_path_sep;
-        g_lean_path += exe_path + g_sep + ".." + g_sep + "library" + g_sep + kernel_instance_name;
+        g_lean_path += exe_path + g_sep + ".." + g_sep + "library";
     } else {
         g_lean_path = r;
     }
@@ -134,7 +134,7 @@ void init_lean_path(char const * kernel_instance_name) {
 }
 
 struct init_lean_path_fn {
-    init_lean_path_fn() { init_lean_path("standard"); }
+    init_lean_path_fn() { init_lean_path(); }
 };
 static init_lean_path_fn g_init_lean_path_fn;
 static std::string       g_sep_str(1, g_sep);
diff --git a/src/util/lean_path.h b/src/util/lean_path.h
index 40a246e1b..077477002 100644
--- a/src/util/lean_path.h
+++ b/src/util/lean_path.h
@@ -16,8 +16,8 @@ public:
     file_not_found_exception(std::string const & fname);
 };
 
-/** \brief Initialize the lean_path for the given kernel instance */
-void init_lean_path(char const * kernel_instance_name);
+/** \brief Initialize the lean_path */
+void init_lean_path();
 /** \brief Return the LEAN_PATH string */
 char const * get_lean_path();
 /**
diff --git a/tests/lean/interactive/test_single.sh b/tests/lean/interactive/test_single.sh
index a739e0690..09d76c9db 100755
--- a/tests/lean/interactive/test_single.sh
+++ b/tests/lean/interactive/test_single.sh
@@ -5,7 +5,7 @@ if [ $# -ne 3 -a $# -ne 2 ]; then
 fi
 ulimit -s unlimited
 LEAN=$1
-export LEAN_PATH=../../../library/standard:.
+export LEAN_PATH=../../../library:.
 if [ $# -ne 3 ]; then
     INTERACTIVE=no
 else
diff --git a/tests/lean/run/test_single.sh b/tests/lean/run/test_single.sh
index 4e1e6e05c..1339f11d6 100755
--- a/tests/lean/run/test_single.sh
+++ b/tests/lean/run/test_single.sh
@@ -5,7 +5,7 @@ if [ $# -ne 2 ]; then
 fi
 ulimit -s 8192
 LEAN=$1
-export LEAN_PATH=../../../library/standard:.
+export LEAN_PATH=../../../library:.
 f=$2
 echo "-- testing $f"
 if $LEAN $f; then
diff --git a/tests/lean/slow/test_single.sh b/tests/lean/slow/test_single.sh
index 4e1e6e05c..1339f11d6 100755
--- a/tests/lean/slow/test_single.sh
+++ b/tests/lean/slow/test_single.sh
@@ -5,7 +5,7 @@ if [ $# -ne 2 ]; then
 fi
 ulimit -s 8192
 LEAN=$1
-export LEAN_PATH=../../../library/standard:.
+export LEAN_PATH=../../../library:.
 f=$2
 echo "-- testing $f"
 if $LEAN $f; then
diff --git a/tests/lean/test.sh b/tests/lean/test.sh
index 63a2f5c8b..0a54f2f9d 100755
--- a/tests/lean/test.sh
+++ b/tests/lean/test.sh
@@ -5,7 +5,7 @@ if [ $# -ne 2 -a $# -ne 1 ]; then
 fi
 ulimit -s 8192
 LEAN=$1
-export LEAN_PATH=../../library/standard:.
+export LEAN_PATH=../../library:.
 if [ $# -ne 2 ]; then
     INTERACTIVE=no
 else
diff --git a/tests/lean/test_single.sh b/tests/lean/test_single.sh
index 2d1b73206..c5215958f 100755
--- a/tests/lean/test_single.sh
+++ b/tests/lean/test_single.sh
@@ -5,7 +5,7 @@ if [ $# -ne 3 -a $# -ne 2 ]; then
 fi
 ulimit -s 8192
 LEAN=$1
-export LEAN_PATH=../../library/standard:.
+export LEAN_PATH=../../library:.
 if [ $# -ne 3 ]; then
     INTERACTIVE=no
 else