diff --git a/src/kernel/level.cpp b/src/kernel/level.cpp
index a78ef3a90..370d1e44e 100644
--- a/src/kernel/level.cpp
+++ b/src/kernel/level.cpp
@@ -33,16 +33,17 @@ 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_meta):
-        level_cell(k, h), m_depth(d), m_has_param(has_param), m_has_meta(has_meta) {}
+    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) {}
 };
 
 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::Meta: case level_kind::Zero:
+    case level_kind::Param: case level_kind::Global: case level_kind::Meta: case level_kind::Zero:
         return false;
     }
     lean_unreachable(); // LCOV_EXCL_LINE
@@ -57,7 +58,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_meta(l)),
+        level_composite(level_kind::Succ, hash(hash(l), 17u), get_depth(l) + 1, has_param(l), has_global(l), has_meta(l)),
         m_l(l),
         m_explicit(is_explicit(l)) {}
 };
@@ -72,8 +73,9 @@ struct level_max_core : public level_composite {
         level_composite(imax ? level_kind::IMax : level_kind::Max,
                         hash(hash(l1), hash(l2)),
                         std::max(get_depth(l1), get_depth(l2)) + 1,
-                        has_param(l1) || has_param(l2),
-                        has_meta(l1) || has_meta(l2)),
+                        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));
     }
@@ -91,9 +93,11 @@ level const & imax_rhs(level const & l) { lean_assert(is_imax(l)); return to_max
 
 struct level_param_core : public level_cell {
     name m_id;
-    level_param_core(bool is_param, name const & id):
-        level_cell(is_param ? level_kind::Param : level_kind::Meta, hash(id.hash(), is_param ? 11u : 13u)),
-        m_id(id) {}
+    level_param_core(level_kind k, name const & id):
+        level_cell(k, hash(id.hash(), is_param ? 11u : 13u)),
+        m_id(id) {
+        lean_assert(k == level_kind::Meta || k == level_kind::Param || k == level_kind::Global);
+    }
 };
 
 bool is_param_core(level const & l) { return is_param(l) || is_meta(l); }
@@ -104,6 +108,7 @@ 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; }
 
 void level_cell::dealloc() {
@@ -114,7 +119,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::Meta:
+    case level_kind::Param: case level_kind::Global: case level_kind::Meta:
         delete static_cast<level_param_core*>(this);
         break;
     case level_kind::Zero:
@@ -125,7 +130,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::Meta:
+    case level_kind::Zero: case level_kind::Param: case level_kind::Global: case level_kind::Meta:
         return 1;
     case level_kind::Succ: case level_kind::Max: case level_kind::IMax:
         return to_composite(l).m_depth;
@@ -135,7 +140,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::Zero: case level_kind::Meta: case level_kind::Global:
         return false;
     case level_kind::Param:
         return true;
@@ -145,9 +150,21 @@ 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::Zero: case level_kind::Param: case level_kind::Global:
         return false;
     case level_kind::Meta:
         return true;
@@ -161,7 +178,7 @@ bool is_explicit(level const & l) {
     switch (kind(l)) {
     case level_kind::Zero:
         return true;
-    case level_kind::Param: case level_kind::Meta: case level_kind::Max: case level_kind::IMax:
+    case level_kind::Param: case level_kind::Global: 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;
@@ -197,13 +214,9 @@ level mk_imax(level const & l1, level const & l2) {
         return level(new level_max_core(true,  l1, l2));
 }
 
-level mk_param_univ(name const & n) {
-    return level(new level_param_core(true, n));
-}
-
-level mk_meta_univ(name const & n) {
-    return level(new level_param_core(false, n));
-}
+level mk_param_univ(name const & n) { return level(new level_param_core(level_kind::Param, n)); }
+level mk_global_univ(name const & n) { return level(new level_param_core(level_kind::Global, n)); }
+level mk_meta_univ(name const & n) { return level(new level_param_core(level_kind::Meta, n)); }
 
 level const & mk_level_zero() {
     static level g_zero(new level_cell(level_kind::Zero, 7u));
@@ -232,7 +245,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::Meta:
+    case level_kind::Param: case level_kind::Global: 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)
@@ -240,7 +253,7 @@ bool operator==(level const & l1, level const & l2) {
         break;
     }
     switch (kind(l1)) {
-    case level_kind::Zero: case level_kind::Param: case level_kind::Meta:
+    case level_kind::Zero: case level_kind::Param: case level_kind::Global: case level_kind::Meta:
         lean_unreachable(); // LCOV_EXCL_LINE
     case level_kind::Max: case level_kind::IMax:
         return
@@ -262,7 +275,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::Meta:
+    case level_kind::Zero: case level_kind::Param: case level_kind::Global: case level_kind::Meta:
         return false;
     case level_kind::Succ:
         return true;
@@ -288,7 +301,7 @@ bool is_lt(level const & a, level const & b) {
     switch (kind(a)) {
     case level_kind::Zero:
         return false;
-    case level_kind::Param: case level_kind::Meta:
+    case level_kind::Param: case level_kind::Global: 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)
@@ -312,7 +325,7 @@ public:
                 switch (k) {
                 case level_kind::Zero:
                     break;
-                case level_kind::Param: case level_kind::Meta:
+                case level_kind::Param: case level_kind::Global: case level_kind::Meta:
                     s << to_param_core(l).m_id;
                     break;
                 case level_kind::Max: case level_kind::IMax:
@@ -339,6 +352,8 @@ 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: {
@@ -377,17 +392,11 @@ serializer & operator<<(serializer & s, level const & n) {
     return s;
 }
 
-level read_level(deserializer & d) {
-    return d.get_extension<level_deserializer>(g_level_sd.m_d_extid).read();
-}
+level read_level(deserializer & d) { return d.get_extension<level_deserializer>(g_level_sd.m_d_extid).read(); }
 
-serializer & operator<<(serializer & s, levels const & ls) {
-    return write_list<level>(s, ls);
-}
+serializer & operator<<(serializer & s, levels const & ls) { return write_list<level>(s, ls); }
 
-levels read_levels(deserializer & d) {
-    return read_list<level>(d, read_level);
-}
+levels read_levels(deserializer & d) { return read_list<level>(d, read_level); }
 
 serializer & operator<<(serializer & s, level_cnstr const & c) {
     s << c.first << c.second;
@@ -404,52 +413,22 @@ serializer & operator<<(serializer & s, level_cnstrs const & cs) {
     return write_list<level_cnstr>(s, cs);
 }
 
-level_cnstrs read_level_cnstrs(deserializer & d) {
-    return read_list<level_cnstr>(d, read_level_cnstr);
-}
+level_cnstrs read_level_cnstrs(deserializer & d) { return read_list<level_cnstr>(d, read_level_cnstr); }
 
-bool has_meta(levels const & ls) {
-    for (auto const & l : ls) {
-        if (has_meta(l))
-            return true;
-    }
-    return false;
-}
+bool has_param(levels const & ls) { return std::any_of(ls.begin(), ls.end(), [](level const & l) { return has_param(l); }); }
+bool has_param(level_cnstr const & c) { return has_param(c.first) || has_param(c.second); }
+bool has_param(level_cnstrs const & cs) { return std::any_of(cs.begin(), cs.end(), [](level_cnstr const & c) { return has_param(c); }); }
 
-bool has_param(levels const & ls) {
-    for (auto const & l : ls) {
-        if (has_param(l))
-            return true;
-    }
-    return false;
-}
+bool has_global(levels const & ls) { return std::any_of(ls.begin(), ls.end(), [](level const & l) { return has_global(l); }); }
+bool has_global(level_cnstr const & c) { return has_global(c.first) || has_global(c.second); }
+bool has_global(level_cnstrs const & cs) { return std::any_of(cs.begin(), cs.end(), [](level_cnstr const & c) { return has_global(c); }); }
 
-bool has_param(level_cnstr const & c) {
-    return has_param(c.first) || has_param(c.second);
-}
-
-bool has_param(level_cnstrs const & cs) {
-    for (auto const & c : cs) {
-        if (has_param(c))
-            return true;
-    }
-    return false;
-}
-
-bool has_meta(level_cnstr const & c) {
-    return has_meta(c.first) || has_meta(c.second);
-}
-
-bool has_meta(level_cnstrs const & cs) {
-    for (auto const & c : cs) {
-        if (has_meta(c))
-            return true;
-    }
-    return false;
-}
+bool has_meta(levels const & ls) { return std::any_of(ls.begin(), ls.end(), [](level const & l) { return has_meta(l); }); }
+bool has_meta(level_cnstr const & c) { return has_meta(c.first) || has_meta(c.second); }
+bool has_meta(level_cnstrs const & cs) { return std::any_of(cs.begin(), cs.end(), [](level_cnstr const & c) { return has_meta(c); }); }
 
 static optional<name> get_undef_param(level const & l, param_names const & ps) {
-    if (!has_meta(l))
+    if (!has_param(l))
         return optional<name>();
     switch (l.kind()) {
     case level_kind::Succ:
@@ -464,7 +443,7 @@ static optional<name> get_undef_param(level const & l, param_names const & ps) {
             return optional<name>(param_id(l));
         else
             return optional<name>();
-    case level_kind::Zero: case level_kind::Meta:
+    case level_kind::Zero: case level_kind::Meta: case level_kind::Global:
         lean_unreachable(); // LCOV_EXCL_LINE
     }
     lean_unreachable(); // LCOV_EXCL_LINE
@@ -505,7 +484,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::Zero: case level_kind::Param: case level_kind::Meta: case level_kind::Global:
         return l;
     }
     lean_unreachable(); // LCOV_EXCL_LINE
@@ -553,7 +532,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::Param: case level_kind::Global:
             out << param_id(l); break;
         case level_kind::Meta:
             out << "?" << meta_id(l); break;
@@ -601,7 +580,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::Param: case level_kind::Global:
             return format(param_id(l));
         case level_kind::Meta:
             return format{format("?"), format(meta_id(l))};
diff --git a/src/kernel/level.h b/src/kernel/level.h
index 6ad09fd7f..e2f7e9b83 100644
--- a/src/kernel/level.h
+++ b/src/kernel/level.h
@@ -31,11 +31,12 @@ 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, Meta };
+enum class level_kind { Zero, Succ, Max, IMax, Param, Global, Meta };
 
 /**
    \brief Universe level.
@@ -82,6 +83,7 @@ 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 An arbitrary (monotonic) total order on universe level terms. */
@@ -89,12 +91,13 @@ bool is_lt(level const & l1, level const & l2);
 
 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_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; }
-inline bool is_imax(level const & l)  { return kind(l) == level_kind::IMax; }
+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; }
+inline bool is_imax(level const & l)   { return kind(l) == level_kind::IMax; }
 
 unsigned get_depth(level const & l);
 
@@ -104,6 +107,7 @@ 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);
 /**
    \brief Return true iff \c l is an explicit level.
@@ -115,9 +119,12 @@ bool is_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);
 
+
 /**
    \brief Return a new level expression based on <tt>l == succ(arg)</tt>, where \c arg is replaced with
    \c new_arg.
@@ -145,6 +152,7 @@ bool is_trivial(level const & lhs, level const & rhs);
 typedef list<level> levels;
 
 bool has_meta(levels const & ls);
+bool has_global(levels const & ls);
 bool has_param(levels const & ls);
 
 /**
@@ -156,6 +164,8 @@ typedef list<level_cnstr> level_cnstrs;
 
 bool has_param(level_cnstr const & c);
 bool has_param(level_cnstrs const & cs);
+bool has_global(level_cnstr const & c);
+bool has_global(level_cnstrs const & cs);
 bool has_meta(level_cnstr const & c);
 bool has_meta(level_cnstrs const & cs);
 
diff --git a/src/library/expr_lt.cpp b/src/library/expr_lt.cpp
index 53327ebf9..4d7013c19 100644
--- a/src/library/expr_lt.cpp
+++ b/src/library/expr_lt.cpp
@@ -20,6 +20,7 @@ bool is_lt(level const & a, level const & b, bool use_hash) {
     case level_kind::Zero:       return true;
     case level_kind::Succ:       return is_lt(succ_of(a), succ_of(b), use_hash);
     case level_kind::Param:      return param_id(a) < param_id(b);
+    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:
         if (max_lhs(a) != max_lhs(b))