diff --git a/doc/export_format.md b/doc/export_format.md
index 3d8de71714..89e0792b89 100644
--- a/doc/export_format.md
+++ b/doc/export_format.md
@@ -57,14 +57,13 @@ The following commands are used to create universe terms in the export file.
 <uidx'> #UM  <uidx_1> <uidx_2>
 <uidx'> #UIM <uidx_1> <uidx_2>
 <uidx'> #UP  <nidx>
-<uidx'> #UG  <nidx>
 ```
 
 In the commands above, `uidx`, `uidx_1` and `uidx_2` denote the unique identifier of existing universe terms,
 `nidx` the unique identifier of existing hierarchical names, and `nidx'` is the identifier for the universe
 term being defined. The command `#US` defines the _successor_ universe for `uidx`, the `#UM` the maximum universe for `uidx_1` and `uidx_2`,
 and `#UIM` is the "impredicative" maximum. It is defined as zero if `uidx_2` evaluates to zero, and `#UM` otherwise.
-The command `#UP` defines the universe parameter with name `nidx`, and `#UG` the global universe with name `nidx`.
+The command `#UP` defines the universe parameter with name `nidx`.
 Here is the sequence of commands for creating the universe term `imax (max 2 l1) l2`.
 ```
 1 #NS 0 l1
@@ -141,15 +140,6 @@ We annotate some commands with comments of the form `-- ...` to make the example
 9 #EA 8 5        -- vector.{1} nat (nat.succ (nat.succ (nat.succ nat.zero)))
 ```
 
-Global universe level declaration
----------------------------------
-
-The command
-```
-#UNI <nidx>
-```
-declares a global universe with name `nidx`.
-
 Definitions and Axioms
 ----------------------
 
diff --git a/library/init/meta/level.lean b/library/init/meta/level.lean
index d47b992dc4..a64ea9b11c 100644
--- a/library/init/meta/level.lean
+++ b/library/init/meta/level.lean
@@ -13,7 +13,6 @@ inductive level
 | max    : level → level → level
 | imax   : level → level → level
 | param  : name → level
-| global : name → level
 | mvar   : name → level
 
 instance : inhabited level :=
diff --git a/src/api/env.cpp b/src/api/env.cpp
index 177427ac5a..f30af087eb 100644
--- a/src/api/env.cpp
+++ b/src/api/env.cpp
@@ -19,14 +19,6 @@ lean_bool lean_env_mk_std(unsigned t, lean_env * r, lean_exception * ex) {
     LEAN_CATCH;
 }
 
-lean_bool lean_env_add_univ(lean_env e, lean_name u, lean_env * r, lean_exception * ex) {
-    LEAN_TRY;
-    check_nonnull(e);
-    check_nonnull(u);
-    *r = of_env(new environment(module::add_universe(to_env_ref(e), to_name_ref(u))));
-    LEAN_CATCH;
-}
-
 lean_bool lean_env_add(lean_env e, lean_cert_decl d, lean_env * r, lean_exception * ex) {
     LEAN_TRY;
     check_nonnull(e);
@@ -51,10 +43,6 @@ unsigned lean_env_trust_level(lean_env e) {
     return e ? to_env_ref(e).trust_lvl() : 0;
 }
 
-lean_bool lean_env_contains_univ(lean_env e, lean_name n) {
-    return e && n && to_env_ref(e).is_universe(to_name_ref(n));
-}
-
 lean_bool lean_env_contains_decl(lean_env e, lean_name n) {
     return e && n && to_env_ref(e).find(to_name_ref(n));
 }
@@ -87,13 +75,3 @@ lean_bool lean_env_for_each_decl(lean_env e, void (*f)(lean_decl), lean_exceptio
     return lean_true;
     LEAN_CATCH;
 }
-
-lean_bool lean_env_for_each_univ(lean_env e, void (*f)(lean_name), lean_exception * ex) {
-    LEAN_TRY;
-    check_nonnull(e);
-    to_env_ref(e).for_each_universe([&](name const & u) {
-            f(of_name(new name(u)));
-        });
-    return lean_true;
-    LEAN_CATCH;
-}
diff --git a/src/api/lean_env.h b/src/api/lean_env.h
index 7c46364fd5..9b269ab784 100644
--- a/src/api/lean_env.h
+++ b/src/api/lean_env.h
@@ -28,9 +28,6 @@ lean_bool lean_env_mk_std(unsigned t, lean_env * r, lean_exception * ex);
 /** Trust all macros implemented in Lean, and do no retype-check imported modules */
 #define LEAN_TRUST_HIGH 100000
 
-/** \brief Add a new global universe with name \c u.
-    \remark exceptions: LEAN_KERNEL_EXCEPTION */
-lean_bool lean_env_add_univ(lean_env e, lean_name u, lean_env * r, lean_exception * ex);
 /** \brief Create a new environment by adding the given certified declaration \c d to the environment \c e.
     \remark exceptions: LEAN_KERNEL_EXCEPTION */
 lean_bool lean_env_add(lean_env e, lean_cert_decl d, lean_env * r, lean_exception * ex);
@@ -47,8 +44,6 @@ void lean_env_del(lean_env e);
 /** \brief Return the trust level of the given environment */
 unsigned lean_env_trust_level(lean_env e);
 
-/** \brief Return true iff \c e contains a global universe with name \c n. */
-lean_bool lean_env_contains_univ(lean_env e, lean_name n);
 /** \brief Return true iff \c e contains a declaration with name \c n. */
 lean_bool lean_env_contains_decl(lean_env e, lean_name n);
 /** \brief Store in \c d the declaration with name \c n in \c e.
@@ -65,9 +60,6 @@ lean_bool lean_env_forget(lean_env e, lean_env * r, lean_exception * ex);
 /** \brief Execute \c f for each declaration in \c env.
     \remark Every declaration passed to \c f must be disposed using \c lean_decl_del. */
 lean_bool lean_env_for_each_decl(lean_env e, void (*f)(lean_decl), lean_exception * ex);
-/** \brief Execute \c f for each global universe in \c env.
-    \remark Every name passed to \c f must be disposed using \c lean_name_del. */
-lean_bool lean_env_for_each_univ(lean_env e, void (*f)(lean_name), lean_exception * ex);
 /*@}*/
 /*@}*/
 
diff --git a/src/api/univ.cpp b/src/api/univ.cpp
index d951cd80b6..c332adce1e 100644
--- a/src/api/univ.cpp
+++ b/src/api/univ.cpp
@@ -97,7 +97,6 @@ lean_univ_kind lean_univ_get_kind(lean_univ u) {
     case level_kind::IMax:     return LEAN_UNIV_IMAX;
     case level_kind::Param:    return LEAN_UNIV_PARAM;
     case level_kind::Meta:     return LEAN_UNIV_META;
-    case level_kind::Global:   break; // TODO(Leo): delete
     }
     lean_unreachable();
 }
diff --git a/src/checker/simple_pp.cpp b/src/checker/simple_pp.cpp
index 15d285bcc7..27bd090cc0 100644
--- a/src/checker/simple_pp.cpp
+++ b/src/checker/simple_pp.cpp
@@ -82,7 +82,6 @@ struct simple_pp_fn {
                                             pp_level(imax_lhs(l)).maybe_paren(1),
                                             pp_level(imax_rhs(l)).maybe_paren(1)}), 0);
             case level_kind::Param: return pp_name(param_id(l));
-            case level_kind::Global: return pp_name(global_id(l));
             case level_kind::Meta: return pp_meta(meta_id(l));
         }
         lean_unreachable();
diff --git a/src/checker/text_import.cpp b/src/checker/text_import.cpp
index d3f2e5c117..97b637519a 100644
--- a/src/checker/text_import.cpp
+++ b/src/checker/text_import.cpp
@@ -154,9 +154,6 @@ struct text_importer {
             } else if (kind == "#UP") {
                 unsigned i1; in >> i1;
                 m_level[idx] = mk_param_univ(m_name.at(i1));
-            } else if (kind == "#UG") {
-                unsigned i1; in >> i1;
-                m_level[idx] = mk_global_univ(m_name.at(i1));
             } else if (kind == "#EV") {
                 unsigned v; in >> v;
                 m_expr[idx] = mk_var(v);
diff --git a/src/frontends/lean/parser.cpp b/src/frontends/lean/parser.cpp
index c0eca28aa4..56d80f0a74 100644
--- a/src/frontends/lean/parser.cpp
+++ b/src/frontends/lean/parser.cpp
@@ -520,8 +520,6 @@ void parser::clear_expr_locals() {
 }
 
 void parser::add_local_level(name const & n, level const & l, bool is_variable) {
-    if (m_env.is_universe(n))
-        throw exception(sstream() << "invalid universe declaration, '" << n << "' shadows a global universe");
     if (m_local_level_decls.contains(n))
         throw exception(sstream() << "invalid universe declaration, '" << n << "' shadows a local universe");
     m_local_level_decls.insert(n, l);
diff --git a/src/frontends/lean/parser_state.cpp b/src/frontends/lean/parser_state.cpp
index b14e3cae14..3403524352 100644
--- a/src/frontends/lean/parser_state.cpp
+++ b/src/frontends/lean/parser_state.cpp
@@ -355,8 +355,6 @@ void parser_state::clear_expr_locals() {
 
 void parser_state::add_local_level(name const & n, level const & l, bool is_variable) {
     ensure_exclusive_context();
-    if (env().is_universe(n))
-        throw exception(sstream() << "invalid universe declaration, '" << n << "' shadows a global universe");
     if (m_context->m_local_level_decls.contains(n))
         throw exception(sstream() << "invalid universe declaration, '" << n << "' shadows a local universe");
     m_context->m_local_level_decls.insert(n, l);
diff --git a/src/frontends/lean/pp.cpp b/src/frontends/lean/pp.cpp
index 7f27e38f46..d614f8a2b0 100644
--- a/src/frontends/lean/pp.cpp
+++ b/src/frontends/lean/pp.cpp
@@ -341,7 +341,7 @@ void pretty_fn::set_options(options const & o) {
 }
 
 format pretty_fn::pp_child(level const & l) {
-    if (is_explicit(l) || is_param(l) || is_meta(l) || is_global(l)) {
+    if (is_explicit(l) || is_param(l) || is_meta(l)) {
         return pp_level(l);
     } else {
         return paren(pp_level(l));
@@ -388,8 +388,6 @@ format pretty_fn::pp_level(level const & l) {
             lean_unreachable(); // LCOV_EXCL_LINE
         case level_kind::Param:
             return format(param_id(l));
-        case level_kind::Global:
-            return format(global_id(l));
         case level_kind::Meta:
             return pp_meta(l);
         case level_kind::Succ: {
diff --git a/src/kernel/environment.cpp b/src/kernel/environment.cpp
index abcf8b7e4d..52358661ea 100644
--- a/src/kernel/environment.cpp
+++ b/src/kernel/environment.cpp
@@ -68,8 +68,8 @@ bool environment_id::is_descendant(environment_id const & id) const {
     return false;
 }
 
-environment::environment(header const & h, environment_id const & ancestor, declarations const & d, name_set const & g, extensions const & exts):
-    m_header(h), m_id(environment_id::mk_descendant(ancestor)), m_declarations(d), m_global_levels(g), m_extensions(exts) {}
+environment::environment(header const & h, environment_id const & ancestor, declarations const & d, extensions const & exts):
+    m_header(h), m_id(environment_id::mk_descendant(ancestor)), m_declarations(d), m_extensions(exts) {}
 
 environment::environment(unsigned trust_lvl):
     environment(trust_lvl, mk_id_normalizer_extension())
@@ -104,24 +104,7 @@ environment environment::add(certified_declaration const & d) const {
     name const & n = d.get_declaration().get_name();
     if (find(n))
         throw_already_declared(*this, n);
-    return environment(m_header, m_id, insert(m_declarations, n, d.get_declaration()), m_global_levels, m_extensions);
-}
-
-environment environment::add_universe(name const & n) const {
-    if (m_global_levels.contains(n))
-        throw_kernel_exception(*this,
-                               "invalid global universe level declaration, environment already contains a universe level with the given name");
-    return environment(m_header, m_id, m_declarations, insert(m_global_levels, n), m_extensions);
-}
-
-environment environment::remove_universe(name const & n) const {
-    if (!m_global_levels.contains(n))
-        throw_kernel_exception(*this, "no universe of the given name");
-    return environment(m_header, m_id, m_declarations, erase(m_global_levels, n), m_extensions);
-}
-
-bool environment::is_universe(name const & n) const {
-    return m_global_levels.contains(n);
+    return environment(m_header, m_id, insert(m_declarations, n, d.get_declaration()), m_extensions);
 }
 
 environment environment::replace(certified_declaration const & t) const {
@@ -139,11 +122,11 @@ environment environment::replace(certified_declaration const & t) const {
         throw_kernel_exception(*this, "invalid replacement of axiom with theorem, the 'replace' operation can only be used when the axiom and theorem have the same type");
     if (ax->get_univ_params() != t.get_declaration().get_univ_params())
         throw_kernel_exception(*this, "invalid replacement of axiom with theorem, the 'replace' operation can only be used when the axiom and theorem have the same universe parameters");
-    return environment(m_header, m_id, insert(m_declarations, n, t.get_declaration()), m_global_levels, m_extensions);
+    return environment(m_header, m_id, insert(m_declarations, n, t.get_declaration()), m_extensions);
 }
 
 environment environment::forget() const {
-    return environment(m_header, environment_id(), m_declarations, m_global_levels, m_extensions);
+    return environment(m_header, environment_id(), m_declarations, m_extensions);
 }
 
 class extension_manager {
@@ -201,17 +184,13 @@ environment environment::update(unsigned id, std::shared_ptr<environment_extensi
     if (id >= new_exts->size())
         new_exts->resize(id+1);
     (*new_exts)[id] = ext;
-    return environment(m_header, m_id, m_declarations, m_global_levels, new_exts);
+    return environment(m_header, m_id, m_declarations, new_exts);
 }
 
 void environment::for_each_declaration(std::function<void(declaration const & d)> const & f) const {
     m_declarations.for_each([&](name const &, declaration const & d) { return f(d); });
 }
 
-void environment::for_each_universe(std::function<void(name const & n)> const & f) const {
-    m_global_levels.for_each([&](name const & n) { return f(n); });
-}
-
 class environment_check_task : public task<bool> {
     environment m_env;
 public:
diff --git a/src/kernel/environment.h b/src/kernel/environment.h
index 528825ec7c..6787b20d7c 100644
--- a/src/kernel/environment.h
+++ b/src/kernel/environment.h
@@ -102,10 +102,9 @@ class environment {
     header         m_header;
     environment_id m_id;
     declarations   m_declarations;
-    name_set       m_global_levels;
     extensions     m_extensions;
 
-    environment(header const & h, environment_id const & id, declarations const & d, name_set const & global_levels, extensions const & ext);
+    environment(header const & h, environment_id const & id, declarations const & d, extensions const & ext);
 
 public:
     environment(unsigned trust_lvl = 0);
@@ -134,21 +133,6 @@ public:
     /** \brief Return declaration with name \c n. Throws and exception if declaration does not exist in this environment. */
     declaration get(name const & n) const;
 
-    /**
-        \brief Add a new global universe level with name \c n
-        This method throws an exception if the environment already contains a level named \c n.
-    */
-    environment add_universe(name const & n) const;
-
-    /**
-        \brief Remove global universe level with name \c n
-        This method throws an exception if the environment does not contain a level named \c n.
-    */
-    environment remove_universe(name const & n) const;
-
-    /** \brief Return true iff the environment has a universe level named \c n. */
-    bool is_universe(name const & n) const;
-
     /**
        \brief Extends the current environment with the given (certified) declaration
        This method throws an exception if:
@@ -194,14 +178,10 @@ public:
     /** \brief Apply the function \c f to each declaration */
     void for_each_declaration(std::function<void(declaration const & d)> const & f) const;
 
-    /** \brief Apply the function \c f to each universe */
-    void for_each_universe(std::function<void(name const & u)> const & f) const;
-
     /** \brief Return true iff declarations and extensions of e1 and e2 are pointer equal */
     friend bool is_eqp(environment const & e1, environment const & e2) {
         return
             is_eqp(e1.m_declarations, e2.m_declarations) &&
-            is_eqp(e1.m_global_levels, e2.m_global_levels) &&
             e1.m_extensions.get() == e2.m_extensions.get();
     }
 
diff --git a/src/kernel/level.cpp b/src/kernel/level.cpp
index 5431bd834b..63de546641 100644
--- a/src/kernel/level.cpp
+++ b/src/kernel/level.cpp
@@ -37,17 +37,16 @@ struct level_cell {
 struct level_composite : public level_cell {
     unsigned   m_depth;
     unsigned   m_has_param:1;
-    unsigned   m_has_global:1;
     unsigned   m_has_meta:1;
-    level_composite(level_kind k, unsigned h, unsigned d, bool has_param, bool has_global, bool has_meta):
-        level_cell(k, h), m_depth(d), m_has_param(has_param), m_has_global(has_global), m_has_meta(has_meta) {}
+    level_composite(level_kind k, unsigned h, unsigned d, bool has_param, bool has_meta):
+        level_cell(k, h), m_depth(d), m_has_param(has_param), m_has_meta(has_meta) {}
 };
 
 bool is_composite(level const & l) {
     switch (kind(l)) {
     case level_kind::Succ: case level_kind::Max: case level_kind::IMax:
         return true;
-    case level_kind::Param: case level_kind::Global: case level_kind::Meta: case level_kind::Zero:
+    case level_kind::Param: case level_kind::Meta: case level_kind::Zero:
         return false;
     }
     lean_unreachable(); // LCOV_EXCL_LINE
@@ -62,7 +61,7 @@ struct level_succ : public level_composite {
     level m_l;
     bool  m_explicit;
     level_succ(level const & l):
-        level_composite(level_kind::Succ, hash(hash(l), 17u), get_depth(l) + 1, has_param(l), has_global(l), has_meta(l)),
+        level_composite(level_kind::Succ, hash(hash(l), 17u), get_depth(l) + 1, has_param(l), has_meta(l)),
         m_l(l),
         m_explicit(is_explicit(l)) {}
 };
@@ -78,7 +77,6 @@ struct level_max_core : public level_composite {
                         hash(hash(l1), hash(l2)),
                         std::max(get_depth(l1), get_depth(l2)) + 1,
                         has_param(l1)  || has_param(l2),
-                        has_global(l1) || has_global(l2),
                         has_meta(l1)   || has_meta(l2)),
         m_lhs(l1), m_rhs(l2) {
         lean_assert(!is_explicit(l1) || !is_explicit(l2));
@@ -100,11 +98,11 @@ struct level_param_core : public level_cell {
     level_param_core(level_kind k, name const & id):
         level_cell(k, hash(id.hash(), static_cast<unsigned>(k))),
         m_id(id) {
-        lean_assert(k == level_kind::Meta || k == level_kind::Param || k == level_kind::Global);
+        lean_assert(k == level_kind::Meta || k == level_kind::Param);
     }
 };
 
-bool is_param_core(level const & l) { return is_param(l) || is_global(l) || is_meta(l); }
+bool is_param_core(level const & l) { return is_param(l) || is_meta(l); }
 
 static level_param_core const & to_param_core(level const & l) {
     lean_assert(is_param_core(l));
@@ -112,10 +110,9 @@ static level_param_core const & to_param_core(level const & l) {
 }
 
 name const & param_id(level const & l) { lean_assert(is_param(l)); return to_param_core(l).m_id; }
-name const & global_id(level const & l)  { lean_assert(is_global(l));  return to_param_core(l).m_id; }
 name const & meta_id(level const & l)  { lean_assert(is_meta(l));  return to_param_core(l).m_id; }
 name const & level_id(level const & l) {
-    lean_assert(is_param(l) || is_global(l) || is_meta(l));
+    lean_assert(is_param(l) || is_meta(l));
     return to_param_core(l).m_id;
 }
 
@@ -127,7 +124,7 @@ void level_cell::dealloc() {
     case level_kind::Max: case level_kind::IMax:
         delete static_cast<level_max_core*>(this);
         break;
-    case level_kind::Param: case level_kind::Global: case level_kind::Meta:
+    case level_kind::Param: case level_kind::Meta:
         delete static_cast<level_param_core*>(this);
         break;
     case level_kind::Zero:
@@ -138,7 +135,7 @@ void level_cell::dealloc() {
 
 unsigned get_depth(level const & l) {
     switch (kind(l)) {
-    case level_kind::Zero: case level_kind::Param: case level_kind::Global: case level_kind::Meta:
+    case level_kind::Zero: case level_kind::Param: case level_kind::Meta:
         return 1;
     case level_kind::Succ: case level_kind::Max: case level_kind::IMax:
         return to_composite(l).m_depth;
@@ -148,7 +145,7 @@ unsigned get_depth(level const & l) {
 
 bool has_param(level const & l) {
     switch (kind(l)) {
-    case level_kind::Zero: case level_kind::Meta: case level_kind::Global:
+    case level_kind::Zero: case level_kind::Meta:
         return false;
     case level_kind::Param:
         return true;
@@ -158,21 +155,9 @@ bool has_param(level const & l) {
     lean_unreachable(); // LCOV_EXCL_LINE
 }
 
-bool has_global(level const & l) {
-    switch (kind(l)) {
-    case level_kind::Zero: case level_kind::Param: case level_kind::Meta:
-        return false;
-    case level_kind::Global:
-        return true;
-    case level_kind::Succ: case level_kind::Max: case level_kind::IMax:
-        return to_composite(l).m_has_param;
-    }
-    lean_unreachable(); // LCOV_EXCL_LINE
-}
-
 bool has_meta(level const & l) {
     switch (kind(l)) {
-    case level_kind::Zero: case level_kind::Param: case level_kind::Global:
+    case level_kind::Zero: case level_kind::Param:
         return false;
     case level_kind::Meta:
         return true;
@@ -186,7 +171,7 @@ bool is_explicit(level const & l) {
     switch (kind(l)) {
     case level_kind::Zero:
         return true;
-    case level_kind::Param: case level_kind::Global: case level_kind::Meta: case level_kind::Max: case level_kind::IMax:
+    case level_kind::Param: case level_kind::Meta: case level_kind::Max: case level_kind::IMax:
         return false;
     case level_kind::Succ:
         return to_level_succ(l).m_explicit;
@@ -252,7 +237,6 @@ level mk_imax(level const & l1, level const & l2) {
 }
 
 level mk_param_univ(name const & n)  { return cache(level(new level_param_core(level_kind::Param, n))); }
-level mk_global_univ(name const & n) { return cache(level(new level_param_core(level_kind::Global, n))); }
 level mk_meta_univ(name const & n)   { return cache(level(new level_param_core(level_kind::Meta, n))); }
 
 static level * g_level_zero = nullptr;
@@ -308,7 +292,7 @@ bool operator==(level const & l1, level const & l2) {
     switch (kind(l1)) {
     case level_kind::Zero:
         return true;
-    case level_kind::Param: case level_kind::Global: case level_kind::Meta:
+    case level_kind::Param: case level_kind::Meta:
         return to_param_core(l1).m_id == to_param_core(l2).m_id;
     case level_kind::Max: case level_kind::IMax: case level_kind::Succ:
         if (to_composite(l1).m_depth != to_composite(l2).m_depth)
@@ -316,7 +300,7 @@ bool operator==(level const & l1, level const & l2) {
         break;
     }
     switch (kind(l1)) {
-    case level_kind::Zero: case level_kind::Param: case level_kind::Global: case level_kind::Meta:
+    case level_kind::Zero: case level_kind::Param: case level_kind::Meta:
         lean_unreachable(); // LCOV_EXCL_LINE
     case level_kind::Max: case level_kind::IMax:
         return
@@ -338,7 +322,7 @@ bool operator==(level const & l1, level const & l2) {
 
 bool is_not_zero(level const & l) {
     switch (kind(l)) {
-    case level_kind::Zero: case level_kind::Param: case level_kind::Global: case level_kind::Meta:
+    case level_kind::Zero: case level_kind::Param: case level_kind::Meta:
         return false;
     case level_kind::Succ:
         return true;
@@ -366,7 +350,7 @@ bool is_lt(level const & a, level const & b, bool use_hash) {
     switch (kind(a)) {
     case level_kind::Zero:
         lean_unreachable(); // LCOV_EXCL_LINE
-    case level_kind::Param: case level_kind::Global: case level_kind::Meta:
+    case level_kind::Param: case level_kind::Meta:
         return to_param_core(a).m_id < to_param_core(b).m_id;
     case level_kind::Max: case level_kind::IMax:
         if (to_max_core(a).m_lhs != to_max_core(b).m_lhs)
@@ -391,7 +375,6 @@ bool is_lt(levels const & as, levels const & bs, bool use_hash) {
 }
 
 bool has_param(levels const & ls) { return std::any_of(ls.begin(), ls.end(), [](level const & l) { return has_param(l); }); }
-bool has_global(levels const & ls) { return std::any_of(ls.begin(), ls.end(), [](level const & l) { return has_global(l); }); }
 bool has_meta(levels const & ls) { return std::any_of(ls.begin(), ls.end(), [](level const & l) { return has_meta(l); }); }
 
 void for_each_level_fn::apply(level const & l) {
@@ -401,7 +384,8 @@ void for_each_level_fn::apply(level const & l) {
     case level_kind::Succ:                          apply(succ_of(l)); break;
     case level_kind::Max: case level_kind::IMax:    apply(to_max_core(l).m_lhs); apply(to_max_core(l).m_rhs); break;
     case level_kind::Zero: case level_kind::Param:
-    case level_kind::Meta: case level_kind::Global: break;
+    case level_kind::Meta:
+        break;
     }
 }
 
@@ -414,7 +398,7 @@ level replace_level_fn::apply(level const & l) {
         return update_succ(l, apply(succ_of(l)));
     case level_kind::Max: case level_kind::IMax:
         return update_max(l, apply(to_max_core(l).m_lhs), apply(to_max_core(l).m_rhs));
-    case level_kind::Zero: case level_kind::Param: case level_kind::Meta: case level_kind::Global:
+    case level_kind::Zero: case level_kind::Param: case level_kind::Meta:
         return l;
     }
     lean_unreachable(); // LCOV_EXCL_LINE
@@ -442,18 +426,6 @@ optional<name> get_undef_param(level const & l, level_param_names const & ps) {
     return r;
 }
 
-optional<name> get_undef_global(level const & l, environment const & env) {
-    optional<name> r;
-    for_each(l, [&](level const & l) {
-            if (!has_global(l) || r)
-                return false;
-            if (is_global(l) && !env.is_universe(global_id(l)))
-                r = global_id(l);
-            return true;
-        });
-    return r;
-}
-
 level update_succ(level const & l, level const & new_arg) {
     if (is_eqp(succ_of(l), new_arg))
         return l;
@@ -495,7 +467,7 @@ level instantiate(level const & l, level_param_names const & ps, levels const &
 static void print(std::ostream & out, level l);
 
 static void print_child(std::ostream & out, level const & l) {
-    if (is_explicit(l) || is_param(l) || is_meta(l) || is_global(l)) {
+    if (is_explicit(l) || is_param(l) || is_meta(l)) {
         print(out, l);
     } else {
         out << "(";
@@ -512,7 +484,7 @@ static void print(std::ostream & out, level l) {
         switch (kind(l)) {
         case level_kind::Zero:
             lean_unreachable(); // LCOV_EXCL_LINE
-        case level_kind::Param: case level_kind::Global:
+        case level_kind::Param:
             out << to_param_core(l).m_id; break;
         case level_kind::Meta:
             out << "?" << meta_id(l); break;
@@ -545,7 +517,7 @@ std::ostream & operator<<(std::ostream & out, level const & l) {
 format pp(level l, bool unicode, unsigned indent);
 
 static format pp_child(level const & l, bool unicode, unsigned indent) {
-    if (is_explicit(l) || is_param(l) || is_meta(l) || is_global(l)) {
+    if (is_explicit(l) || is_param(l) || is_meta(l)) {
         return pp(l, unicode, indent);
     } else {
         return paren(pp(l, unicode, indent));
@@ -560,7 +532,7 @@ format pp(level l, bool unicode, unsigned indent) {
         switch (kind(l)) {
         case level_kind::Zero:
             lean_unreachable(); // LCOV_EXCL_LINE
-        case level_kind::Param: case level_kind::Global:
+        case level_kind::Param:
             return format(to_param_core(l).m_id);
         case level_kind::Meta:
             return format("?") + format(meta_id(l));
@@ -611,7 +583,7 @@ static bool is_norm_lt(level const & a, level const & b) {
         switch (kind(l1)) {
         case level_kind::Zero: case level_kind::Succ:
             lean_unreachable(); // LCOV_EXCL_LINE
-        case level_kind::Param: case level_kind::Global: case level_kind::Meta:
+        case level_kind::Param: case level_kind::Meta:
             return to_param_core(l1).m_id < to_param_core(l2).m_id;
         case level_kind::Max: case level_kind::IMax:
             if (to_max_core(l1).m_lhs != to_max_core(l2).m_lhs)
@@ -666,7 +638,7 @@ level normalize(level const & l) {
     case level_kind::Succ:
         lean_unreachable(); // LCOV_EXCL_LINE
     case level_kind::Zero:   case level_kind::Param:
-    case level_kind::Global: case level_kind::Meta:
+    case level_kind::Meta:
         return l;
     case level_kind::IMax: {
         auto l1 = normalize(imax_lhs(r));
diff --git a/src/kernel/level.h b/src/kernel/level.h
index c6dd70fcae..5d9f3983d8 100644
--- a/src/kernel/level.h
+++ b/src/kernel/level.h
@@ -30,12 +30,11 @@ struct level_cell;
                     Their definitions "mirror" the typing rules for Pi and Sigma.
 
    - Param(n)     : A parameter. In Lean, we have universe polymorphic definitions.
-   - Global(n)    : A global level.
    - Meta(n)      : Placeholder. It is the equivalent of a metavariable for universe levels.
                     The elaborator is responsible for replacing Meta with level expressions
                     that do not contain Meta.
 */
-enum class level_kind { Zero, Succ, Max, IMax, Param, Global, Meta };
+enum class level_kind { Zero, Succ, Max, IMax, Param, Meta };
 
 /**
    \brief Universe level.
@@ -90,7 +89,6 @@ level mk_max(level const & l1, level const & l2);
 level mk_imax(level const & l1, level const & l2);
 level mk_succ(level const & l);
 level mk_param_univ(name const & n);
-level mk_global_univ(name const & n);
 level mk_meta_univ(name const & n);
 
 /** \brief Convert (succ^k l) into (l, k). If l is not a succ, then return (l, 0) */
@@ -100,7 +98,6 @@ inline unsigned hash(level const & l) { return l.hash(); }
 inline level_kind kind(level const & l) { return l.kind(); }
 inline bool is_zero(level const & l)   { return kind(l) == level_kind::Zero; }
 inline bool is_param(level const & l)  { return kind(l) == level_kind::Param; }
-inline bool is_global(level const & l) { return kind(l) == level_kind::Global; }
 inline bool is_meta(level const & l)   { return kind(l) == level_kind::Meta; }
 inline bool is_succ(level const & l)   { return kind(l) == level_kind::Succ; }
 inline bool is_max(level const & l)    { return kind(l) == level_kind::Max; }
@@ -115,7 +112,6 @@ level const & imax_lhs(level const & l);
 level const & imax_rhs(level const & l);
 level const & succ_of(level const & l);
 name const & param_id(level const & l);
-name const & global_id(level const & l);
 name const & meta_id(level const & l);
 name const & level_id(level const & l);
 /**
@@ -131,8 +127,6 @@ bool is_explicit(level const & l);
 unsigned to_explicit(level const & l);
 /** \brief Return true iff \c l contains placeholder (aka meta parameters). */
 bool has_meta(level const & l);
-/** \brief Return true iff \c l contains globals */
-bool has_global(level const & l);
 /** \brief Return true iff \c l contains parameters */
 bool has_param(level const & l);
 
@@ -160,7 +154,7 @@ bool is_equivalent(level const & lhs, level const & rhs);
 level normalize(level const & l);
 
 /**
-   \brief If the result is true, then forall assignments \c A that assigns all parameters, globals and metavariables occuring
+   \brief If the result is true, then forall assignments \c A that assigns all parameters and metavariables occuring
    in \c l1 and \l2, we have that the universe level l1[A] is bigger or equal to l2[A].
 
    \remark This function assumes l1 and l2 are normalized
@@ -173,7 +167,6 @@ bool is_geq(level const & l1, level const & l2);
 typedef list<level> levels;
 
 bool has_meta(levels const & ls);
-bool has_global(levels const & ls);
 bool has_param(levels const & ls);
 
 /** \brief An arbitrary (monotonic) total order on universe level terms. */
@@ -206,9 +199,6 @@ bool occurs(level const & u, level const & l);
 
 typedef list<name> level_param_names;
 
-/** \brief If \c l contains a global that is not in \c env, then return it. Otherwise, return none. */
-optional<name> get_undef_global(level const & l, environment const & env);
-
 /** \brief If \c l contains a parameter that is not in \c ps, then return it. Otherwise, return none. */
 optional<name> get_undef_param(level const & l, level_param_names const & ps);
 
@@ -222,7 +212,7 @@ level instantiate(level const & l, level_param_names const & ps, levels const &
 std::ostream & operator<<(std::ostream & out, level const & l);
 
 /**
-   \brief If the result is true, then forall assignments \c A that assigns all parameters, globals and metavariables occuring
+   \brief If the result is true, then forall assignments \c A that assigns all parameters and metavariables occuring
    in \c l, l[A] != zero.
 */
 bool is_not_zero(level const & l);
diff --git a/src/kernel/type_checker.cpp b/src/kernel/type_checker.cpp
index d4a5a3d312..d5a80d320f 100644
--- a/src/kernel/type_checker.cpp
+++ b/src/kernel/type_checker.cpp
@@ -66,8 +66,6 @@ expr type_checker::ensure_pi_core(expr e, expr const & s) {
 }
 
 void type_checker::check_level(level const & l, expr const & s) {
-    if (auto n1 = get_undef_global(l, m_env))
-        throw_kernel_exception(m_env, sstream() << "invalid reference to undefined global universe level '" << *n1 << "'", s);
     if (m_params) {
         if (auto n2 = get_undef_param(l, *m_params))
             throw_kernel_exception(m_env, sstream() << "invalid reference to undefined universe level parameter '"
diff --git a/src/library/aliases.cpp b/src/library/aliases.cpp
index 0a2f65f6f9..59a05137a5 100644
--- a/src/library/aliases.cpp
+++ b/src/library/aliases.cpp
@@ -168,13 +168,7 @@ optional<expr> get_local_ref(environment const & env, name const & n) {
         return none_expr();
 }
 
-static void check_no_shadow(environment const & env, name const & a) {
-    if (env.is_universe(a))
-        throw exception(sstream() << "universe level alias '" << a << "' shadows existing global universe level");
-}
-
 environment add_level_alias(environment const & env, name const & a, name const & l) {
-    check_no_shadow(env, a);
     aliases_ext ext = get_extension(env);
     ext.add_level_alias(a, l);
     return update(env, ext);
@@ -206,16 +200,6 @@ environment add_aliases(environment const & env, name const & prefix, name const
                     ext.add_expr_alias(a, d.get_name(), overwrite);
             }
         });
-    env.for_each_universe([&](name const & u) {
-            if (is_prefix_of(prefix, u) && !is_exception(u, prefix, num_exceptions, exceptions)) {
-                name a = u.replace_prefix(prefix, new_prefix);
-                if (env.is_universe(a))
-                    throw exception(sstream() << "universe level alias '" << a << "' shadows existing global universe level");
-                if (!(is_protected(env, u) && a.is_atomic()) &&
-                    !a.is_anonymous())
-                    ext.add_level_alias(a, u);
-            }
-        });
     return update(env, ext);
 }
 
diff --git a/src/library/aliases.h b/src/library/aliases.h
index 7fe71efdae..3cf92cb585 100644
--- a/src/library/aliases.h
+++ b/src/library/aliases.h
@@ -40,10 +40,6 @@ optional<name> get_level_alias(environment const & env, name const & n);
    \brief Create an alias for each declaration named <tt>prefix.rest</tt>.
    The alias for <tt>prefix.rest</tt> is <tt>new_prefix.rest</tt>.
 
-   The command will also create aliases for universe level declarations.
-   However, an error is thrown if the universe level shadows existing aliases and/or declarations.
-   We don't have "choice" construct for universe levels.
-
    \remark \c new_prefix may be the anonymous name.
 */
 environment add_aliases(environment const & env, name const & prefix, name const & new_prefix,
diff --git a/src/library/export.cpp b/src/library/export.cpp
index 59492aeca0..61d00e2e6f 100644
--- a/src/library/export.cpp
+++ b/src/library/export.cpp
@@ -83,11 +83,6 @@ class exporter {
             i = static_cast<unsigned>(m_level2idx.size());
             m_out << i << " #UP " << n << "\n";
             break;
-        case level_kind::Global:
-            n = export_name(global_id(l));
-            i = static_cast<unsigned>(m_level2idx.size());
-            m_out << i << " #UG " << n << "\n";
-            break;
         case level_kind::Meta:
             throw exception("invalid 'export', universe meta-variables cannot be exported");
         }
@@ -288,13 +283,6 @@ class exporter {
             });
     }
 
-    void export_global_universes() {
-        m_env.for_each_universe([&](name const & u) {
-                unsigned n = export_name(u);
-                m_out << "#UNI " << n << "\n";
-            });
-    }
-
     void export_quotient() {
         if (m_quotient_exported) return;
         m_quotient_exported = true;
@@ -344,7 +332,6 @@ public:
     void operator()() {
         m_name2idx[{}] = 0;
         m_level2idx[{}] = 0;
-        export_global_universes();
         if (has_quotient(m_env))
             export_quotient();
         export_declarations();
diff --git a/src/library/expr_lt.cpp b/src/library/expr_lt.cpp
index aa0228e5c2..d74eadfe53 100644
--- a/src/library/expr_lt.cpp
+++ b/src/library/expr_lt.cpp
@@ -78,8 +78,6 @@ bool is_lt_no_level_params(level const & a, level const & b) {
         lean_unreachable(); // LCOV_EXCL_LINE
     case level_kind::Param:
         return false;
-    case level_kind::Global:
-        return global_id(a) < global_id(b);
     case level_kind::Meta:
         return meta_id(a) < meta_id(b);
     case level_kind::Max:
diff --git a/src/library/kernel_serializer.cpp b/src/library/kernel_serializer.cpp
index 0e4f43d5c7..ff830f059b 100644
--- a/src/library/kernel_serializer.cpp
+++ b/src/library/kernel_serializer.cpp
@@ -24,7 +24,6 @@ public:
                 switch (k) {
                 case level_kind::Zero:     break;
                 case level_kind::Param:    s << param_id(l);   break;
-                case level_kind::Global:   s << global_id(l);  break;
                 case level_kind::Meta:     s << meta_id(l);    break;
                 case level_kind::Max:      write(max_lhs(l));  write(max_rhs(l)); break;
                 case level_kind::IMax:     write(imax_lhs(l)); write(imax_rhs(l)); break;
@@ -46,8 +45,6 @@ public:
                     return mk_level_zero();
                 case level_kind::Param:
                     return mk_param_univ(read_name(d));
-                case level_kind::Global:
-                    return mk_global_univ(read_name(d));
                 case level_kind::Meta:
                     return mk_meta_univ(read_name(d));
                 case level_kind::Max: {
diff --git a/src/library/max_sharing.cpp b/src/library/max_sharing.cpp
index c047bb6612..b3b34c7d2b 100644
--- a/src/library/max_sharing.cpp
+++ b/src/library/max_sharing.cpp
@@ -29,7 +29,7 @@ struct max_sharing_fn::imp {
         level res;
         switch (l.kind()) {
         case level_kind::Zero:   case level_kind::Param:
-        case level_kind::Global: case level_kind::Meta:
+        case level_kind::Meta:
             res = l;
             break;
         case level_kind::Succ:
diff --git a/src/library/module.cpp b/src/library/module.cpp
index d2852ebecb..86537ec4b9 100644
--- a/src/library/module.cpp
+++ b/src/library/module.cpp
@@ -296,27 +296,6 @@ struct import_helper {
     }
 };
 
-struct glvl_modification : public modification {
-    LEAN_MODIFICATION("glvl")
-
-    name m_name;
-
-    glvl_modification() {}
-    glvl_modification(name const & name) : m_name(name) {}
-
-    void perform(environment & env) const override {
-        env = env.add_universe(m_name);
-    }
-
-    void serialize(serializer & s) const override {
-        s << m_name;
-    }
-
-    static std::shared_ptr<modification const> deserialize(deserializer & d) {
-        return std::make_shared<glvl_modification>(read_name(d));
-    }
-};
-
 struct decl_modification : public modification {
     LEAN_MODIFICATION("decl")
 
@@ -425,12 +404,6 @@ environment add_and_perform(environment const & env, std::shared_ptr<modificatio
     return update(new_env, ext);
 }
 
-environment add_universe(environment const & env, name const & l) {
-    module_ext ext = get_extension(env);
-    ext.m_module_univs = cons(l, ext.m_module_univs);
-    return add_and_perform(update(env, ext), std::make_shared<glvl_modification>(l));
-}
-
 environment update_module_defs(environment const & env, declaration const & d) {
     if (d.is_definition() && !d.is_theorem()) {
         module_ext ext = get_extension(env);
@@ -725,7 +698,6 @@ module_loader mk_dummy_loader() {
 void initialize_module() {
     g_ext            = new module_ext_reg();
     g_object_readers = new object_readers();
-    glvl_modification::init();
     decl_modification::init();
     inductive_modification::init();
     quot_modification::init();
@@ -737,7 +709,6 @@ void finalize_module() {
     pos_info_mod::finalize();
     inductive_modification::finalize();
     decl_modification::finalize();
-    glvl_modification::finalize();
     delete g_object_readers;
     delete g_ext;
 }
diff --git a/src/library/module.h b/src/library/module.h
index 6a81d1332a..5c5d7cf818 100644
--- a/src/library/module.h
+++ b/src/library/module.h
@@ -132,9 +132,6 @@ namespace module {
 environment add(environment const & env, std::shared_ptr<modification const> const & modif);
 environment add_and_perform(environment const & env, std::shared_ptr<modification const> const & modif);
 
-/** \brief Add the global universe declaration to the environment, and mark it to be exported. */
-environment add_universe(environment const & env, name const & l);
-
 /** \brief Add the given declaration to the environment, and mark it to be exported. */
 environment add(environment const & env, certified_declaration const & d);
 
diff --git a/src/library/type_context.cpp b/src/library/type_context.cpp
index a27d5cba32..4713b6fcca 100644
--- a/src/library/type_context.cpp
+++ b/src/library/type_context.cpp
@@ -1455,8 +1455,6 @@ lbool type_context::is_def_eq_core(level const & l1, level const & l2, bool part
     case level_kind::Succ:
         return is_def_eq_core(succ_of(l1), succ_of(l2), partial);
     case level_kind::Param:
-    case level_kind::Global:
-        return l_false;
     case level_kind::Meta:
         /* This can happen, for example, when we are in tmp_mode, but l1 and l2 are not tmp universe metavariables. */
         return l_false;
diff --git a/src/library/util.cpp b/src/library/util.cpp
index 6940af1f5c..b34338b15c 100644
--- a/src/library/util.cpp
+++ b/src/library/util.cpp
@@ -99,7 +99,7 @@ optional<expr> unfold_app(environment const & env, expr const & e) {
 
 optional<level> dec_level(level const & l) {
     switch (kind(l)) {
-    case level_kind::Zero: case level_kind::Param: case level_kind::Global: case level_kind::Meta:
+    case level_kind::Zero: case level_kind::Param: case level_kind::Meta:
         return none_level();
     case level_kind::Succ:
         return some_level(succ_of(l));
diff --git a/src/library/vm/vm_level.cpp b/src/library/vm/vm_level.cpp
index 70e27856a9..251083259c 100644
--- a/src/library/vm/vm_level.cpp
+++ b/src/library/vm/vm_level.cpp
@@ -58,10 +58,6 @@ vm_obj level_param(vm_obj const & n) {
     return to_obj(mk_param_univ(to_name(n)));
 }
 
-vm_obj level_global(vm_obj const & n) {
-    return to_obj(mk_global_univ(to_name(n)));
-}
-
 vm_obj level_mvar(vm_obj const & n) {
     return to_obj(mk_meta_univ(to_name(n)));
 }
@@ -85,9 +81,6 @@ unsigned level_cases_on(vm_obj const & o, buffer<vm_obj> & data) {
     case level_kind::Param:
         data.push_back(to_obj(param_id(l)));
         break;
-    case level_kind::Global:
-        data.push_back(to_obj(global_id(l)));
-        break;
     case level_kind::Meta:
         data.push_back(to_obj(meta_id(l)));
         break;
@@ -159,7 +152,6 @@ void initialize_vm_level() {
     DECLARE_VM_BUILTIN(name({"level", "max"}),              level_max);
     DECLARE_VM_BUILTIN(name({"level", "imax"}),             level_imax);
     DECLARE_VM_BUILTIN(name({"level", "param"}),            level_param);
-    DECLARE_VM_BUILTIN(name({"level", "global"}),           level_global);
     DECLARE_VM_BUILTIN(name({"level", "mvar"}),             level_mvar);
     DECLARE_VM_BUILTIN(name({"level", "has_decidable_eq"}), level_has_decidable_eq);
     DECLARE_VM_BUILTIN(name({"level", "lt"}),               level_lt);