diff --git a/src/frontends/lean/decl_cmds.cpp b/src/frontends/lean/decl_cmds.cpp
index eab0a0c601..300a63cd11 100644
--- a/src/frontends/lean/decl_cmds.cpp
+++ b/src/frontends/lean/decl_cmds.cpp
@@ -38,11 +38,11 @@ void update_univ_parameters(parser & p, buffer<name> & lp_names, name_set const
 
 static environment declare_universe(parser & p, environment env, name const & n, bool local) {
     if (local) {
-        p.add_local_level(n, mk_param_univ(n), local);
+        p.add_local_level(n, mk_univ_param(n), local);
     } else if (in_section(env)) {
-        p.add_local_level(n, mk_param_univ(n), false);
+        p.add_local_level(n, mk_univ_param(n), false);
     } else {
-        p.add_local_level(n, mk_param_univ(n), true);
+        p.add_local_level(n, mk_univ_param(n), true);
     }
     return env;
 }
@@ -147,7 +147,7 @@ static environment declare_var(parser & p, environment env,
 /** \brief If we are in a section, then add the new local levels to it. */
 static void update_local_levels(parser & p, level_param_names const & new_ls, bool is_variable) {
     for (auto const & l : new_ls)
-        p.add_local_level(l, mk_param_univ(l), is_variable);
+        p.add_local_level(l, mk_univ_param(l), is_variable);
 }
 
 optional<binder_info> parse_binder_info(parser & p, variable_kind k) {
diff --git a/src/frontends/lean/decl_util.cpp b/src/frontends/lean/decl_util.cpp
index 9e9bc4341c..8202d178ef 100644
--- a/src/frontends/lean/decl_util.cpp
+++ b/src/frontends/lean/decl_util.cpp
@@ -35,7 +35,7 @@ bool parse_univ_params(parser & p, buffer<name> & lp_names) {
             auto pos0 = p.pos();
             name l = p.check_atomic_id_next("invalid declaration, identifier expected");
             lp_names.push_back(l);
-            p.add_local_level(l, mk_param_univ(l));
+            p.add_local_level(l, mk_univ_param(l));
             if (p.pos() == pos0) break;
         }
         p.next();
diff --git a/src/frontends/lean/elaborator.cpp b/src/frontends/lean/elaborator.cpp
index 98f8b7b35a..56a02ad10a 100644
--- a/src/frontends/lean/elaborator.cpp
+++ b/src/frontends/lean/elaborator.cpp
@@ -2060,7 +2060,7 @@ expr elaborator::visit_app(expr const & e, optional<expr> const & expected_type)
 
 static level ground_uvars(level const & l) {
     return replace(l, [] (level const & l) {
-        if (is_meta(l)) {
+        if (is_mvar(l)) {
             return some_level(mk_level_zero());
         } else {
             return none_level();
@@ -3943,7 +3943,7 @@ struct sanitize_param_names_fn : public replace_visitor {
             m_idx++;
             if (!m_L.contains(new_n)) {
                 m_new_param_names.push_back(new_n);
-                return mk_param_univ(new_n);
+                return mk_univ_param(new_n);
             }
         }
     }
@@ -3951,7 +3951,7 @@ struct sanitize_param_names_fn : public replace_visitor {
     level sanitize(level const & l) {
         name p("u");
         return replace(l, [&](level const & l) -> optional<level> {
-                if (is_meta(l)) {
+                if (is_mvar(l)) {
                     if (is_metavar_decl_ref(l) && m_ctx.is_assigned(l)) {
                         return some_level(sanitize(*m_ctx.get_assignment(l)));
                     } else {
diff --git a/src/frontends/lean/inductive_cmds.cpp b/src/frontends/lean/inductive_cmds.cpp
index 211be44fb4..b09943cc97 100644
--- a/src/frontends/lean/inductive_cmds.cpp
+++ b/src/frontends/lean/inductive_cmds.cpp
@@ -447,7 +447,7 @@ class inductive_cmd_fn {
             new_ind_type = elab.elaborate(replace_locals(new_ind_type, params_no_inds, new_params));
             new_ind_type = normalize(new_ind_type);
             level l = get_datatype_result_level(new_ind_type);
-            if (is_meta(l)) {
+            if (is_mvar(l)) {
                 if (m_explicit_levels)
                     throw_error("resultant universe must be provided, when using explicit universe levels");
                 new_ind_type = update_result_sort(new_ind_type, m_u_meta);
@@ -457,7 +457,7 @@ class inductive_cmd_fn {
                 result_level = l;
                 first = false;
             } else {
-                if (!is_meta(l) && result_level != l) {
+                if (!is_mvar(l) && result_level != l) {
                     throw_error("mutually inductive types must live in the same universe");
                 }
             }
diff --git a/src/frontends/lean/pp.cpp b/src/frontends/lean/pp.cpp
index 21eed99c2d..41fff21f3f 100644
--- a/src/frontends/lean/pp.cpp
+++ b/src/frontends/lean/pp.cpp
@@ -252,15 +252,15 @@ name pretty_fn::mk_local_name(name const & n, name const & suggested) {
 }
 
 level pretty_fn::purify(level const & l) {
-    if (!m_universes || !m_purify_metavars || !has_meta(l))
+    if (!m_universes || !m_purify_metavars || !has_mvar(l))
         return l;
     return replace(l, [&](level const & l) {
-            if (!has_meta(l))
+            if (!has_mvar(l))
                 return some_level(l);
             if (is_metavar_decl_ref(l))
-                return some_level(mk_meta_univ(mk_metavar_name(meta_id(l), "l")));
-            if (is_meta(l) && !is_idx_metauniv(l))
-                return some_level(mk_meta_univ(mk_metavar_name(meta_id(l))));
+                return some_level(mk_univ_mvar(mk_metavar_name(mvar_id(l), "l")));
+            if (is_mvar(l) && !is_idx_metauniv(l))
+                return some_level(mk_univ_mvar(mk_metavar_name(mvar_id(l))));
             return none_level();
         });
 }
@@ -358,7 +358,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)) {
+    if (is_explicit(l) || is_param(l) || is_mvar(l)) {
         return pp_level(l);
     } else {
         return paren(pp_level(l));
@@ -388,7 +388,7 @@ format pretty_fn::pp_meta(level const & l) {
         } else if (is_metavar_decl_ref(l)) {
             return format((sstream() << "?l_" << get_metavar_decl_ref_suffix(l)).str());
         } else {
-            return compose(format("?"), format(meta_id(l)));
+            return compose(format("?"), format(mvar_id(l)));
         }
     } else {
         return format("?");
@@ -405,7 +405,7 @@ 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::Meta:
+        case level_kind::MVar:
             return pp_meta(l);
         case level_kind::Succ: {
             auto p = to_offset(l);
diff --git a/src/frontends/lean/structure_cmd.cpp b/src/frontends/lean/structure_cmd.cpp
index 348d3ebc4f..3bf3174450 100644
--- a/src/frontends/lean/structure_cmd.cpp
+++ b/src/frontends/lean/structure_cmd.cpp
@@ -779,7 +779,7 @@ struct structure_cmd_fn {
     void add_locals() {
         if (m_explicit_universe_params) {
             for (name const & l : m_level_names)
-                m_p.add_local_level(l, mk_param_univ(l));
+                m_p.add_local_level(l, mk_univ_param(l));
         }
         for (expr const & param : m_params)
             m_p.add_local(param);
diff --git a/src/frontends/lean/util.cpp b/src/frontends/lean/util.cpp
index 091b0c8387..e33645e3bf 100644
--- a/src/frontends/lean/util.cpp
+++ b/src/frontends/lean/util.cpp
@@ -97,7 +97,7 @@ levels collect_local_nonvar_levels(parser & p, level_param_names const & ls) {
     buffer<level> section_ls_buffer;
     for (name const & l : ls) {
         if (p.is_local_level(l) && !p.is_local_level_variable(l))
-            section_ls_buffer.push_back(mk_param_univ(l));
+            section_ls_buffer.push_back(mk_univ_param(l));
         else
             break;
     }
diff --git a/src/kernel/expr.cpp b/src/kernel/expr.cpp
index 2f28a38624..73d1d9a8a7 100644
--- a/src/kernel/expr.cpp
+++ b/src/kernel/expr.cpp
@@ -367,7 +367,7 @@ expr mk_fvar(name const & n) {
 expr mk_const(name const & n, levels const & ls) {
     inc(n.raw()); inc(ls.raw());
     expr r(mk_cnstr(static_cast<unsigned>(expr_kind::Const), n.raw(), ls.raw(), expr_scalar_size(expr_kind::Const)));
-    set_scalar<expr_kind::Const>(r, hash(n.hash(), hash(ls)), false, has_meta(ls), false, has_param(ls));
+    set_scalar<expr_kind::Const>(r, hash(n.hash(), hash(ls)), false, has_mvar(ls), false, has_param(ls));
     return r;
 }
 
@@ -389,7 +389,7 @@ expr mk_app(expr const & f, expr const & a) {
 expr mk_sort(level const & l) {
     inc(l.raw());
     expr r(mk_cnstr(static_cast<unsigned>(expr_kind::Sort), l.raw(), expr_scalar_size(expr_kind::Sort)));
-    set_scalar<expr_kind::Sort>(r, hash(l), false, has_meta(l), false, has_param(l));
+    set_scalar<expr_kind::Sort>(r, hash(l), false, has_mvar(l), false, has_param(l));
     return r;
 }
 
diff --git a/src/kernel/inductive.cpp b/src/kernel/inductive.cpp
index 8e3f685a40..695022402c 100644
--- a/src/kernel/inductive.cpp
+++ b/src/kernel/inductive.cpp
@@ -204,7 +204,7 @@ public:
                 u = name("u").append_after(i);
                 i++;
             }
-            m_elim_level = mk_param_univ(u);
+            m_elim_level = mk_univ_param(u);
         }
         std::cout << ">> elim_level: " << m_elim_level << "\n";
     }
diff --git a/src/kernel/inductive/inductive.cpp b/src/kernel/inductive/inductive.cpp
index 87132a5e8d..0627e9e66e 100644
--- a/src/kernel/inductive/inductive.cpp
+++ b/src/kernel/inductive/inductive.cpp
@@ -512,7 +512,7 @@ struct add_inductive_fn {
                 l = name("l").append_after(i);
                 i++;
             }
-            m_elim_level = mk_param_univ(l);
+            m_elim_level = mk_univ_param(l);
         }
     }
 
diff --git a/src/kernel/level.cpp b/src/kernel/level.cpp
index 65c19d883b..7cf96c910e 100644
--- a/src/kernel/level.cpp
+++ b/src/kernel/level.cpp
@@ -31,12 +31,12 @@ inline static void set_level_scalar_fields(object * lvl, unsigned num_objs, unsi
 inline static unsigned get_hash(object * lvl, unsigned num_objs) { return cnstr_scalar<unsigned>(lvl, num_objs*sizeof(object*)); }
 inline static unsigned get_depth(object * lvl, unsigned num_objs) { return cnstr_scalar<unsigned>(lvl, num_objs*sizeof(object*) + sizeof(unsigned)); }
 inline static bool get_has_param(object * lvl, unsigned num_objs) { return cnstr_scalar<unsigned char>(lvl, num_objs*sizeof(object*) + 2*sizeof(unsigned)); }
-inline static bool get_has_meta(object * lvl, unsigned num_objs) { return cnstr_scalar<unsigned char>(lvl, num_objs*sizeof(object*) + 2*sizeof(unsigned) + sizeof(unsigned char)); }
+inline static bool get_has_mvar(object * lvl, unsigned num_objs) { return cnstr_scalar<unsigned char>(lvl, num_objs*sizeof(object*) + 2*sizeof(unsigned) + sizeof(unsigned char)); }
 
 level mk_succ(level const & l) {
     inc(l.raw());
     level r(mk_cnstr(static_cast<unsigned>(level_kind::Succ), l.raw(), g_level_num_scalars));
-    set_level_scalar_fields(r.raw(), 1, hash(hash(l), 17u), get_depth(l)+1, has_param(l), has_meta(l));
+    set_level_scalar_fields(r.raw(), 1, hash(hash(l), 17u), get_depth(l)+1, has_param(l), has_mvar(l));
     return r;
 }
 
@@ -47,25 +47,25 @@ level mk_max_imax(level_kind k, level const & l1, level const & l2) {
                             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_mvar(l1) || has_mvar(l2));
     return level(r);
 }
 
-level mk_param_univ(name const & n) {
+level mk_univ_param(name const & n) {
     inc(n.raw());
     return level(mk_cnstr(static_cast<unsigned>(level_kind::Param), n.raw()));
 }
 
-level mk_meta_univ(name const & n) {
+level mk_univ_mvar(name const & n) {
     inc(n.raw());
-    return level(mk_cnstr(static_cast<unsigned>(level_kind::Meta), n.raw()));
+    return level(mk_cnstr(static_cast<unsigned>(level_kind::MVar), n.raw()));
 }
 
 unsigned level::hash() const {
     switch (kind()) {
     case level_kind::Zero:
         return 31;
-    case level_kind::Param: case level_kind::Meta:
+    case level_kind::Param: case level_kind::MVar:
         return level_id(*this).hash();
     case level_kind::Succ:
         return get_hash(raw(), 1);
@@ -77,7 +77,7 @@ unsigned level::hash() const {
 
 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::MVar:
         return 1;
     case level_kind::Succ:
         return get_depth(l.raw(), 1);
@@ -89,7 +89,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::MVar:
         return false;
     case level_kind::Param:
         return true;
@@ -101,16 +101,16 @@ bool has_param(level const & l) {
     lean_unreachable(); // LCOV_EXCL_LINE
 }
 
-bool has_meta(level const & l) {
+bool has_mvar(level const & l) {
     switch (kind(l)) {
     case level_kind::Zero: case level_kind::Param:
         return false;
-    case level_kind::Meta:
+    case level_kind::MVar:
         return true;
     case level_kind::Succ:
-        return get_has_meta(l.raw(), 1);
+        return get_has_mvar(l.raw(), 1);
     case level_kind::Max: case level_kind::IMax:
-        return get_has_meta(l.raw(), 2);
+        return get_has_mvar(l.raw(), 2);
     }
     lean_unreachable(); // LCOV_EXCL_LINE
 }
@@ -120,7 +120,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::MVar: case level_kind::Max: case level_kind::IMax:
         return false;
     case level_kind::Succ:
         return is_explicit(succ_of(l));
@@ -194,7 +194,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::MVar:
         return level_id(l1) == level_id(l2);
     case level_kind::Max: case level_kind::IMax: case level_kind::Succ:
         if (get_depth(l1) != get_depth(l2))
@@ -202,7 +202,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::MVar:
         lean_unreachable(); // LCOV_EXCL_LINE
     case level_kind::Max: case level_kind::IMax:
         return
@@ -216,7 +216,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::MVar:
         return false;
     case level_kind::Succ:
         return true;
@@ -243,7 +243,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::Meta:
+    case level_kind::Param: case level_kind::MVar:
         return level_id(a) < level_id(b);
     case level_kind::Max: case level_kind::IMax:
         if (level_lhs(a) != level_lhs(b))
@@ -268,7 +268,7 @@ 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_meta(levels const & ls) { return std::any_of(ls.begin(), ls.end(), [](level const & l) { return has_meta(l); }); }
+bool has_mvar(levels const & ls) { return std::any_of(ls.begin(), ls.end(), [](level const & l) { return has_mvar(l); }); }
 
 void for_each_level_fn::apply(level const & l) {
     if (!m_f(l))
@@ -279,7 +279,7 @@ void for_each_level_fn::apply(level const & l) {
     case level_kind::Max: case level_kind::IMax:
         apply(level_lhs(l)); apply(level_rhs(l)); break;
     case level_kind::Zero: case level_kind::Param:
-    case level_kind::Meta:
+    case level_kind::MVar:
         break;
     }
 }
@@ -296,7 +296,7 @@ level replace_level_fn::apply(level const & l) {
         level l2 = apply(level_rhs(l));
         return update_max(l, l1, l2);
     }
-    case level_kind::Zero: case level_kind::Param: case level_kind::Meta:
+    case level_kind::Zero: case level_kind::Param: case level_kind::MVar:
         return l;
     }
     lean_unreachable(); // LCOV_EXCL_LINE
@@ -365,7 +365,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)) {
+    if (is_explicit(l) || is_param(l) || is_mvar(l)) {
         print(out, l);
     } else {
         out << "(";
@@ -384,8 +384,8 @@ static void print(std::ostream & out, level l) {
             lean_unreachable(); // LCOV_EXCL_LINE
         case level_kind::Param:
             out << param_id(l); break;
-        case level_kind::Meta:
-            out << "?" << meta_id(l); break;
+        case level_kind::MVar:
+            out << "?" << mvar_id(l); break;
         case level_kind::Succ:
             out << "succ "; print_child(out, succ_of(l)); break;
         case level_kind::Max: case level_kind::IMax:
@@ -415,7 +415,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)) {
+    if (is_explicit(l) || is_param(l) || is_mvar(l)) {
         return pp(l, unicode, indent);
     } else {
         return paren(pp(l, unicode, indent));
@@ -432,8 +432,8 @@ format pp(level l, bool unicode, unsigned indent) {
             lean_unreachable(); // LCOV_EXCL_LINE
         case level_kind::Param:
             return format(param_id(l));
-        case level_kind::Meta:
-            return format("?") + format(meta_id(l));
+        case level_kind::MVar:
+            return format("?") + format(mvar_id(l));
         case level_kind::Succ: {
             auto p    = to_offset(l);
             auto fmt1 = pp_child(p.first, unicode, indent);
@@ -482,7 +482,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::Meta:
+        case level_kind::Param: case level_kind::MVar:
             return level_id(l1) < level_id(l2);
         case level_kind::Max: case level_kind::IMax:
             if (level_lhs(l1) != level_lhs(l2))
@@ -537,7 +537,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::Meta:
+    case level_kind::MVar:
         return l;
     case level_kind::IMax: {
         auto l1 = normalize(imax_lhs(r));
@@ -627,7 +627,7 @@ bool is_geq(level const & l1, level const & l2) {
 levels param_names_to_levels(level_param_names const & ps) {
     buffer<level> ls;
     for (auto const & p : ps)
-        ls.push_back(mk_param_univ(p));
+        ls.push_back(mk_univ_param(p));
     return levels(ls);
 }
 
diff --git a/src/kernel/level.h b/src/kernel/level.h
index d4552c96b2..241baef605 100644
--- a/src/kernel/level.h
+++ b/src/kernel/level.h
@@ -18,30 +18,24 @@ namespace lean {
 class environment;
 struct level_cell;
 /**
-   \brief Universe level kinds.
+inductive level
+| zero   : level
+| succ   : level → level
+| max    : level → level → level
+| imax   : level → level → level
+| param  : name → level
+| mvar   : name → level
 
-   - Zero         : It is also Prop level if env.impredicative() is true
-   - Succ(l)      : successor level
-   - Max(l1, l2)  : maximum of two levels
-   - IMax(l1, l2) : IMax(x, zero)    = zero             for all x
-                    IMax(x, succ(y)) = Max(x, succ(y))  for all x, y
-
-                    We use IMax to handle Pi-types, and Max for Sigma-types.
-                    Their definitions "mirror" the typing rules for Pi and Sigma.
-
-   - Param(n)     : A parameter. In Lean, we have universe polymorphic definitions.
-   - 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.
+We level.imax to handle Pi-types.
 */
-enum class level_kind { Zero, Succ, Max, IMax, Param, Meta };
+enum class level_kind { Zero, Succ, Max, IMax, Param, MVar };
 
 /** \brief Universe level. */
 class level : public object_ref {
     friend level mk_succ(level const & l);
     friend level mk_max_imax(level_kind k, level const & l1, level const & l2);
-    friend level mk_param_univ(name const & n);
-    friend level mk_meta_univ(name const & n);
+    friend level mk_univ_param(name const & n);
+    friend level mk_univ_mvar(name const & n);
     explicit level(object * o):object_ref(o) { inc(o); }
     explicit level(object_ref && o):object_ref(o) {}
 public:
@@ -64,7 +58,7 @@ public:
     bool is_max() const { return kind() == level_kind::Max; }
     bool is_imax() const { return kind() == level_kind::IMax; }
     bool is_param() const { return kind() == level_kind::Param; }
-    bool is_meta() const { return kind() == level_kind::Meta; }
+    bool is_mvar() const { return kind() == level_kind::MVar; }
 
     friend inline level const & max_lhs(level const & l) { lean_assert(l.is_max()); return static_cast<level const &>(cnstr_obj_ref(l, 0)); }
     friend inline level const & max_rhs(level const & l) { lean_assert(l.is_max()); return static_cast<level const &>(cnstr_obj_ref(l, 1)); }
@@ -74,8 +68,8 @@ public:
     friend inline level const & level_rhs(level const & l) { lean_assert(l.is_max() || l.is_imax()); return static_cast<level const &>(cnstr_obj_ref(l, 1)); }
     friend inline level const & succ_of(level const & l) { lean_assert(l.is_succ()); return static_cast<level const &>(cnstr_obj_ref(l, 0)); }
     friend inline name const & param_id(level const & l) { lean_assert(l.is_param()); return static_cast<name const &>(cnstr_obj_ref(l, 0)); }
-    friend inline name const & meta_id(level const & l)  { lean_assert(l.is_meta()); return static_cast<name const &>(cnstr_obj_ref(l, 0)); }
-    friend inline name const & level_id(level const & l) { lean_assert(l.is_param() || l.is_meta()); return static_cast<name const &>(cnstr_obj_ref(l, 0)); }
+    friend inline name const & mvar_id(level const & l)  { lean_assert(l.is_mvar()); return static_cast<name const &>(cnstr_obj_ref(l, 0)); }
+    friend inline name const & level_id(level const & l) { lean_assert(l.is_param() || l.is_mvar()); return static_cast<name const &>(cnstr_obj_ref(l, 0)); }
 };
 
 typedef list_ref<level> levels;
@@ -103,8 +97,8 @@ inline level mk_imax_core(level const & l1, level const & l2) { return mk_max_im
 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_meta_univ(name const & n);
+level mk_univ_param(name const & n);
+level mk_univ_mvar(name const & n);
 
 /** \brief Convert (succ^k l) into (l, k). If l is not a succ, then return (l, 0) */
 pair<level, unsigned> to_offset(level l);
@@ -113,7 +107,7 @@ 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 l.is_zero(); }
 inline bool is_param(level const & l)  { return l.is_param(); }
-inline bool is_meta(level const & l)   { return l.is_meta(); }
+inline bool is_mvar(level const & l)   { return l.is_mvar(); }
 inline bool is_succ(level const & l)   { return l.is_succ(); }
 inline bool is_max(level const & l)    { return l.is_max(); }
 inline bool is_imax(level const & l)   { return l.is_imax(); }
@@ -130,7 +124,7 @@ bool is_explicit(level const & l);
     \pre is_explicit(l) */
 unsigned to_explicit(level const & l);
 /** \brief Return true iff \c l contains placeholder (aka meta parameters). */
-bool has_meta(level const & l);
+bool has_mvar(level const & l);
 /** \brief Return true iff \c l contains parameters */
 bool has_param(level const & l);
 
@@ -158,7 +152,7 @@ bool is_geq_core(level l1, level l2);
 
 bool is_geq(level const & l1, level const & l2);
 
-bool has_meta(levels const & ls);
+bool has_mvar(levels const & ls);
 bool has_param(levels const & ls);
 
 /** \brief An arbitrary (monotonic) total order on universe level terms. */
diff --git a/src/kernel/quot.cpp b/src/kernel/quot.cpp
index 936f313771..1bf85b3546 100644
--- a/src/kernel/quot.cpp
+++ b/src/kernel/quot.cpp
@@ -30,7 +30,7 @@ static void check_eq_type(environment const & env) {
         throw exception("failed to initialize quot module, unexpected number of universe params at 'eq' type");
     local_ctx lctx;
     name_generator g;
-    level u = mk_param_univ(head(decl->m_level_params));
+    level u = mk_univ_param(head(decl->m_level_params));
     expr alpha = lctx.mk_local_decl(g, "α", mk_sort(u), mk_implicit_binder_info());
     expr expected_eq_type = lctx.mk_pi(alpha, mk_arrow(alpha, mk_arrow(alpha, mk_Prop())));
     if (decl->m_type != expected_eq_type)
@@ -50,7 +50,7 @@ environment quot_declare(environment const & env) {
     name u_name("u");
     local_ctx lctx;
     name_generator g;
-    level u         = mk_param_univ(u_name);
+    level u         = mk_univ_param(u_name);
     expr Sort_u     = mk_sort(u);
     expr alpha      = lctx.mk_local_decl(g, "α", Sort_u, mk_implicit_binder_info());
     expr r          = lctx.mk_local_decl(g, "r", mk_arrow(alpha, mk_arrow(alpha, mk_Prop())));
@@ -68,7 +68,7 @@ environment quot_declare(environment const & env) {
     quot_r          = mk_app(mk_constant(*quot_consts::g_quot, {u}), alpha, r);
     a               = lctx.mk_local_decl(g, "a", alpha);
     name v_name("v");
-    level v         = mk_param_univ(v_name);
+    level v         = mk_univ_param(v_name);
     expr Sort_v     = mk_sort(v);
     expr beta       = lctx.mk_local_decl(g, "β", Sort_v, mk_implicit_binder_info());
     expr f          = lctx.mk_local_decl(g, "f", mk_arrow(alpha, beta));
diff --git a/src/library/aux_definition.cpp b/src/library/aux_definition.cpp
index ce2eaed109..3116ab3485 100644
--- a/src/library/aux_definition.cpp
+++ b/src/library/aux_definition.cpp
@@ -18,14 +18,14 @@ namespace lean {
 level closure_helper::collect(level const & l) {
     lean_assert(!m_finalized_collection);
     return replace(l, [&](level const & l) {
-            if (is_meta(l)) {
-                name const & id = meta_id(l);
+            if (is_mvar(l)) {
+                name const & id = mvar_id(l);
                 if (auto r = m_univ_meta_to_param.find(id)) {
                     return some_level(*r);
                 } else {
                     name n      = m_prefix.append_after(m_next_idx);
                     m_next_idx++;
-                    level new_r = mk_param_univ(n);
+                    level new_r = mk_univ_param(n);
                     m_univ_meta_to_param.insert(id, new_r);
                     m_univ_meta_to_param_inv.insert(n, l);
                     m_level_params.push_back(n);
@@ -129,7 +129,7 @@ void closure_helper::get_level_closure(buffer<level> & ls) {
         if (level const * l = m_univ_meta_to_param_inv.find(n))
             ls.push_back(*l);
         else
-            ls.push_back(mk_param_univ(n));
+            ls.push_back(mk_univ_param(n));
     }
 }
 
diff --git a/src/library/constructions/brec_on.cpp b/src/library/constructions/brec_on.cpp
index 790e654904..ec1897f509 100644
--- a/src/library/constructions/brec_on.cpp
+++ b/src/library/constructions/brec_on.cpp
@@ -53,7 +53,7 @@ static environment mk_below(environment const & env, name const & n, bool ibelow
     unsigned ntypeformers  = 1;
     level_param_names lps  = rec_decl.get_univ_params();
     bool is_reflexive      = is_reflexive_datatype(tc, n);
-    level  lvl             = mk_param_univ(head(lps));
+    level  lvl             = mk_univ_param(head(lps));
     levels lvls            = param_names_to_levels(tail(lps));
     level_param_names blvls; // universe level parameters of ibelow/below
     level  rlvl;  // universe level of the resultant type
@@ -179,7 +179,7 @@ static environment mk_brec_on(environment const & env, name const & n, bool ind)
     unsigned ntypeformers  = 1;
     level_param_names lps  = rec_decl.get_univ_params();
     bool is_reflexive      = is_reflexive_datatype(tc, n);
-    level  lvl             = mk_param_univ(head(lps));
+    level  lvl             = mk_univ_param(head(lps));
     levels lvls            = param_names_to_levels(tail(lps));
     level rlvl;
     level_param_names blps;
diff --git a/src/library/constructions/injective.cpp b/src/library/constructions/injective.cpp
index 646c23cab1..6abf9d9a2f 100644
--- a/src/library/constructions/injective.cpp
+++ b/src/library/constructions/injective.cpp
@@ -212,7 +212,7 @@ environment mk_injective_arrow(environment const & env, name const & ir_name) {
     type_context_old tctx(env);
 
     name P_lp_name = mk_fresh_lp_name(d.get_univ_params());
-    expr P = tctx.push_local(name("P"), mk_sort(mk_param_univ(P_lp_name)), mk_strict_implicit_binder_info());
+    expr P = tctx.push_local(name("P"), mk_sort(mk_univ_param(P_lp_name)), mk_strict_implicit_binder_info());
 
     expr ty = d.get_type();
     buffer<expr> args;
diff --git a/src/library/constructions/no_confusion.cpp b/src/library/constructions/no_confusion.cpp
index fcfe9ac08c..77afcb21b6 100644
--- a/src/library/constructions/no_confusion.cpp
+++ b/src/library/constructions/no_confusion.cpp
@@ -36,7 +36,7 @@ optional<environment> mk_no_confusion_type(environment const & env, name const &
     declaration ind_decl   = env.get(n);
     declaration cases_decl = env.get(name(n, "cases_on"));
     level_param_names lps  = cases_decl.get_univ_params();
-    level  plvl            = mk_param_univ(head(lps));
+    level  plvl            = mk_univ_param(head(lps));
     levels ilvls           = param_names_to_levels(tail(lps));
     level rlvl             = plvl;
     expr ind_type          = instantiate_type_univ_params(ind_decl, ilvls);
diff --git a/src/library/expr_lt.cpp b/src/library/expr_lt.cpp
index 1c94e65ad6..f331ab65fc 100644
--- a/src/library/expr_lt.cpp
+++ b/src/library/expr_lt.cpp
@@ -89,8 +89,8 @@ 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::Meta:
-        return meta_id(a) < meta_id(b);
+    case level_kind::MVar:
+        return mvar_id(a) < mvar_id(b);
     case level_kind::Max:
         if (is_lt_no_level_params(max_lhs(a), max_lhs(b)))
             return true;
diff --git a/src/library/idx_metavar.cpp b/src/library/idx_metavar.cpp
index 7807db10c7..36e160aac7 100644
--- a/src/library/idx_metavar.cpp
+++ b/src/library/idx_metavar.cpp
@@ -26,7 +26,7 @@ void finalize_idx_metavar() {
 }
 
 level mk_idx_metauniv(unsigned i) {
-    return mk_meta_univ(name(*g_tmp_prefix, i));
+    return mk_univ_mvar(name(*g_tmp_prefix, i));
 }
 
 expr mk_idx_metavar(unsigned i, expr const & type) {
@@ -34,15 +34,15 @@ expr mk_idx_metavar(unsigned i, expr const & type) {
 }
 
 bool is_idx_metauniv(level const & l) {
-    if (!is_meta(l))
+    if (!is_mvar(l))
         return false;
-    name const & n = meta_id(l);
+    name const & n = mvar_id(l);
     return !n.is_atomic() && n.is_numeral() && n.get_prefix() == *g_tmp_prefix;
 }
 
 unsigned to_meta_idx(level const & l) {
     lean_assert(is_idx_metauniv(l));
-    return meta_id(l).get_numeral().get_small_value();
+    return mvar_id(l).get_numeral().get_small_value();
 }
 
 bool is_idx_metavar(expr const & e) {
@@ -58,12 +58,12 @@ unsigned to_meta_idx(expr const & e) {
 }
 
 bool has_idx_metauniv(level const & l) {
-    if (!has_meta(l))
+    if (!has_mvar(l))
         return false;
     bool found = false;
     for_each(l, [&](level const & l) {
             if (found) return false;
-            if (!has_meta(l)) return false;
+            if (!has_mvar(l)) return false;
             if (is_idx_metauniv(l))
                 found = true;
             return true;
@@ -111,13 +111,13 @@ struct to_idx_metavars_fn : public replace_visitor {
         m_mctx(mctx), m_new_us(new_us), m_new_ms(new_ms) {}
 
     level visit(level const & l) {
-        if (!has_meta(l)) return l;
+        if (!has_mvar(l)) return l;
         return replace(l, [&](level const & l) {
-                if (is_meta(l) && !is_idx_metauniv(l)) {
-                    if (auto it = m_lvl_cache.find(meta_id(l)))
+                if (is_mvar(l) && !is_idx_metauniv(l)) {
+                    if (auto it = m_lvl_cache.find(mvar_id(l)))
                         return some_level(*it);
                     level new_l = mk_idx_metauniv(m_new_us.size());
-                    m_lvl_cache.insert(meta_id(l), new_l);
+                    m_lvl_cache.insert(mvar_id(l), new_l);
                     m_new_us.push_back(new_l);
                     return some_level(new_l);
                 }
diff --git a/src/library/inductive_compiler/mutual.cpp b/src/library/inductive_compiler/mutual.cpp
index a9908009a9..8ef8e08f07 100644
--- a/src/library/inductive_compiler/mutual.cpp
+++ b/src/library/inductive_compiler/mutual.cpp
@@ -721,7 +721,7 @@ class add_mutual_inductive_decl_fn {
 
         level_param_names rec_lp_names = rec_decl.get_univ_params();
         bool elim_to_prop = rec_decl.get_num_univ_params() == m_basic_decl.get_lp_names().size();
-        m_elim_level      = elim_to_prop ? mk_level_zero() : mk_param_univ(head(rec_lp_names));
+        m_elim_level      = elim_to_prop ? mk_level_zero() : mk_univ_param(head(rec_lp_names));
 
         levels rec_levels = param_names_to_levels(rec_lp_names);
         expr rec_const = mk_constant(rec_name, rec_levels);
diff --git a/src/library/max_sharing.cpp b/src/library/max_sharing.cpp
index 9650052818..b66551bf89 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::Meta:
+        case level_kind::MVar:
             res = l;
             break;
         case level_kind::Succ:
diff --git a/src/library/metavar_context.cpp b/src/library/metavar_context.cpp
index 264848e6ad..d5617ac755 100644
--- a/src/library/metavar_context.cpp
+++ b/src/library/metavar_context.cpp
@@ -19,7 +19,7 @@ static expr mk_meta_ref(name const & n) {
 }
 
 bool is_metavar_decl_ref(level const & u) {
-    return is_meta(u) && is_prefix_of(*g_meta_prefix, meta_id(u));
+    return is_mvar(u) && is_prefix_of(*g_meta_prefix, mvar_id(u));
 }
 
 bool is_metavar_decl_ref(expr const & e) {
@@ -28,7 +28,7 @@ bool is_metavar_decl_ref(expr const & e) {
 
 name get_metavar_decl_ref_suffix(level const & u) {
     lean_assert(is_metavar_decl_ref(u));
-    return meta_id(u).replace_prefix(*g_meta_prefix, name());
+    return mvar_id(u).replace_prefix(*g_meta_prefix, name());
 }
 
 name get_metavar_decl_ref_suffix(expr const & e) {
@@ -43,7 +43,7 @@ static name mk_meta_decl_name() {
 
 level metavar_context::mk_univ_metavar_decl() {
     // TODO(Leo): should use name_generator
-    return mk_meta_univ(mk_meta_decl_name());
+    return mk_univ_mvar(mk_meta_decl_name());
 }
 
 expr metavar_context::mk_metavar_decl(name const & user_name, local_context const & lctx, expr const & type) {
@@ -83,7 +83,7 @@ expr metavar_context::get_local(expr const & mvar, name const & n) const {
 }
 
 void metavar_context::assign(level const & u, level const & l) {
-    m_uassignment.insert(meta_id(u), l);
+    m_uassignment.insert(mvar_id(u), l);
 }
 
 void metavar_context::assign(expr const & e, expr const & v) {
@@ -97,7 +97,7 @@ void metavar_context::assign(expr const & e, local_context const & lctx, list<ex
 
 optional<level> metavar_context::get_assignment(level const & l) const {
     lean_assert(is_metavar_decl_ref(l));
-    if (auto v = m_uassignment.find(meta_id(l)))
+    if (auto v = m_uassignment.find(mvar_id(l)))
         return some_level(*v);
     else
         return none_level();
diff --git a/src/library/metavar_context.h b/src/library/metavar_context.h
index b71c6c9d89..5d02c9c35d 100644
--- a/src/library/metavar_context.h
+++ b/src/library/metavar_context.h
@@ -75,7 +75,7 @@ public:
 
     bool is_assigned(level const & l) const {
         lean_assert(is_metavar_decl_ref(l));
-        return m_uassignment.contains(meta_id(l));
+        return m_uassignment.contains(mvar_id(l));
     }
 
     bool is_assigned(expr const & m) const {
diff --git a/src/library/metavar_util.h b/src/library/metavar_util.h
index 8820abaa9a..a51c2e24e3 100644
--- a/src/library/metavar_util.h
+++ b/src/library/metavar_util.h
@@ -28,11 +28,11 @@ bool in_tmp_mode() const;
 
 template<typename CTX>
 bool has_assigned(CTX const & ctx, level const & l) {
-    if (!has_meta(l))
+    if (!has_mvar(l))
         return false;
     bool found = false;
     for_each(l, [&](level const & l) {
-            if (!has_meta(l))
+            if (!has_mvar(l))
                 return false; // stop search
             if (found)
                 return false;  // stop search
@@ -82,7 +82,7 @@ level instantiate_mvars(CTX & ctx, level const & l) {
     if (!has_assigned(ctx, l))
         return l;
     return replace(l, [&](level const & l) {
-            if (!has_meta(l)) {
+            if (!has_mvar(l)) {
                 return some_level(l);
             } else if (ctx.is_mvar(l)) {
                 if (auto v1 = ctx.get_assignment(l)) {
diff --git a/src/library/placeholder.cpp b/src/library/placeholder.cpp
index 8446b44305..98078c4515 100644
--- a/src/library/placeholder.cpp
+++ b/src/library/placeholder.cpp
@@ -36,8 +36,8 @@ static unsigned next_placeholder_id() {
     g_placeholder_id++;
     return r;
 }
-level mk_level_placeholder() { return mk_param_univ(name(*g_placeholder_name, next_placeholder_id())); }
-level mk_level_one_placeholder() { return mk_param_univ(*g_placeholder_one_name); }
+level mk_level_placeholder() { return mk_univ_param(name(*g_placeholder_name, next_placeholder_id())); }
+level mk_level_one_placeholder() { return mk_univ_param(*g_placeholder_one_name); }
 static name const & to_prefix(expr_placeholder_kind k) {
     switch (k) {
     case expr_placeholder_kind::Implicit:       return *g_implicit_placeholder_name;
diff --git a/src/library/tactic/tactic_state.cpp b/src/library/tactic/tactic_state.cpp
index 3197002657..20ae108518 100644
--- a/src/library/tactic/tactic_state.cpp
+++ b/src/library/tactic/tactic_state.cpp
@@ -655,7 +655,7 @@ vm_obj tactic_mk_meta_var(vm_obj const & t, vm_obj const & s0) {
 vm_obj tactic_get_univ_assignment(vm_obj const & u, vm_obj const & s0) {
     tactic_state const & s   = tactic::to_state(s0);
     metavar_context mctx     = s.mctx();
-    if (!is_meta(to_level(u))) {
+    if (!is_mvar(to_level(u))) {
         return tactic::mk_exception("get_univ_assignment tactic failed, argument is not an universe metavariable", s);
     } else if (auto r = mctx.get_assignment(to_level(u))) {
         return tactic::mk_success(to_obj(*r), s);
diff --git a/src/library/type_context.cpp b/src/library/type_context.cpp
index c0b7e965d7..59ab891b5f 100644
--- a/src/library/type_context.cpp
+++ b/src/library/type_context.cpp
@@ -1452,7 +1452,7 @@ static bool is_max_like(level const & l) {
     such that l_i's do not contain m.
     If the result is true, then all l_i's are stored in rest. */
 static bool generalized_check_meta(level const & m, level const & rhs, bool & found_m, buffer<level> & rest) {
-    lean_assert(is_meta(m));
+    lean_assert(is_mvar(m));
     if (is_max(rhs)) {
         return
             generalized_check_meta(m, max_lhs(rhs), found_m, rest) &&
@@ -1475,7 +1475,7 @@ static bool generalized_check_meta(level const & m, level const & rhs, bool & fo
             ?u := max v ?w
 */
 bool type_context_old::solve_u_eq_max_u_v(level const & lhs, level const & rhs) {
-    lean_assert(is_meta(lhs));
+    lean_assert(is_mvar(lhs));
     lean_assert(occurs(lhs, rhs));
     buffer<level> rest;
     bool found_lhs = false;
@@ -1559,7 +1559,7 @@ lbool type_context_old::is_def_eq_core(level const & l1, level const & l2, bool
     case level_kind::Succ:
         return is_def_eq_core(succ_of(l1), succ_of(l2), partial);
     case level_kind::Param:
-    case level_kind::Meta:
+    case level_kind::MVar:
         /* This can happen, for example, when we are in tmp_mode, but l1 and l2 are not tmp universe metavariables. */
         return l_false;
     case level_kind::Zero:
@@ -3885,7 +3885,7 @@ expr type_context_old::preprocess_class(expr const & type,
         return type;
     buffer<level> C_levels;
     for (level const & l : const_levels(C)) {
-        if (has_meta(l)) {
+        if (has_mvar(l)) {
             level new_uvar = mk_tmp_univ_mvar();
             u_replacements.emplace_back(l, new_uvar);
             C_levels.push_back(new_uvar);
diff --git a/src/library/util.cpp b/src/library/util.cpp
index 2050fde3e9..a83805fc27 100644
--- a/src/library/util.cpp
+++ b/src/library/util.cpp
@@ -133,7 +133,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::Meta:
+    case level_kind::Zero: case level_kind::Param: case level_kind::MVar:
         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 e908673086..2ea437b61f 100644
--- a/src/library/vm/vm_level.cpp
+++ b/src/library/vm/vm_level.cpp
@@ -53,11 +53,11 @@ vm_obj level_imax(vm_obj const & o1, vm_obj const & o2) {
 }
 
 vm_obj level_param(vm_obj const & n) {
-    return to_obj(mk_param_univ(to_name(n)));
+    return to_obj(mk_univ_param(to_name(n)));
 }
 
 vm_obj level_mvar(vm_obj const & n) {
-    return to_obj(mk_meta_univ(to_name(n)));
+    return to_obj(mk_univ_mvar(to_name(n)));
 }
 
 unsigned level_cases_on(vm_obj const & o, buffer<vm_obj> & data) {
@@ -79,8 +79,8 @@ 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::Meta:
-        data.push_back(to_obj(meta_id(l)));
+    case level_kind::MVar:
+        data.push_back(to_obj(mvar_id(l)));
         break;
     }
     return static_cast<unsigned>(l.kind());
diff --git a/src/tests/kernel/level.cpp b/src/tests/kernel/level.cpp
index 43bae6ef40..1c67a083f4 100644
--- a/src/tests/kernel/level.cpp
+++ b/src/tests/kernel/level.cpp
@@ -36,7 +36,7 @@ static void tst1() {
     lean_assert(mk_imax(two, zero) == zero);
     check_serializer(two);
     check_serializer(one);
-    level p = mk_param_univ("p");
+    level p = mk_univ_param("p");
     lean_assert(mk_imax(p, zero) == zero);
     lean_assert(mk_max(zero, p) == p);
     lean_assert(mk_max(p, zero) == p);
@@ -45,16 +45,16 @@ static void tst1() {
     check_serializer(mk_imax(p, one));
     check_serializer(mk_imax(one, p));
     check_serializer(mk_imax(mk_succ(p), p));
-    std::cout << pp(mk_max(p, mk_max(mk_succ(mk_param_univ("a")), one))) << "\n";
+    std::cout << pp(mk_max(p, mk_max(mk_succ(mk_univ_param("a")), one))) << "\n";
 }
 
 static void tst2() {
     level zero;
     level one = mk_succ(zero);
     level two = mk_succ(one);
-    level p1 = mk_param_univ("p1");
-    level p2 = mk_param_univ("p2");
-    level m1 = mk_meta_univ("m1");
+    level p1 = mk_univ_param("p1");
+    level p2 = mk_univ_param("p2");
+    level m1 = mk_univ_mvar("m1");
     lean_assert(is_equivalent(mk_succ(p2), mk_max(p2, mk_succ(p2))));
     lean_assert(is_equivalent(mk_max(p1, p2), mk_max(p2, p1)));
     lean_assert(!is_equivalent(mk_imax(p1, p2), mk_imax(p2, p1)));