diff --git a/src/kernel/environment.cpp b/src/kernel/environment.cpp
index 8a6a7f8a5..7b324ae66 100644
--- a/src/kernel/environment.cpp
+++ b/src/kernel/environment.cpp
@@ -263,6 +263,10 @@ universe_constraints const & environment_cell::get_ro_ucs() const {
     return get_ro_universes().m_constraints;
 }
 
+optional<int> environment_cell::get_universe_distance(name const & u1, name const & u2) const {
+    return get_ro_ucs().get_distance(u1, u2);
+}
+
 /** \brief Return true iff l1 >= l2 + k by asserted universe constraints. */
 bool environment_cell::is_ge(level const & l1, level const & l2, int k) const {
     if (l1 == l2)
diff --git a/src/kernel/environment.h b/src/kernel/environment.h
index 3e7b72f89..130c00581 100644
--- a/src/kernel/environment.h
+++ b/src/kernel/environment.h
@@ -126,6 +126,13 @@ public:
     */
     bool is_ge(level const & l1, level const & l2) const;
 
+    /**
+       \brief Return the (minimal) distance between two universes.
+       That is, the biggest \c k s.t. <tt>u1 >= u2 + k</tt>.
+       Return none if there is no such \c k.
+    */
+    optional<int> get_universe_distance(name const & u1, name const & u2) const;
+
     /**
        \brief Return universal variable with the given name.
        Throw an exception if variable is not defined in this environment.
diff --git a/src/library/kernel_bindings.cpp b/src/library/kernel_bindings.cpp
index cafb79e21..afecef6e9 100644
--- a/src/library/kernel_bindings.cpp
+++ b/src/library/kernel_bindings.cpp
@@ -1159,6 +1159,16 @@ static int environment_import(lua_State * L) {
     return 0;
 }
 
+static int environment_get_universe_distance(lua_State * L) {
+    ro_shared_environment env(L, 1);
+    auto r = env->get_universe_distance(to_name_ext(L, 2), to_name_ext(L, 3));
+    if (r)
+        lua_pushinteger(L, *r);
+    else
+        lua_pushnil(L);
+    return 1;
+}
+
 static const struct luaL_Reg environment_m[] = {
     {"__gc",           environment_gc}, // never throws
     {"__tostring",     safe_function<environment_tostring>},
@@ -1167,6 +1177,7 @@ static const struct luaL_Reg environment_m[] = {
     {"has_children",   safe_function<environment_has_children>},
     {"parent",         safe_function<environment_parent>},
     {"add_uvar_cnstr", safe_function<environment_add_uvar_cnstr>},
+    {"get_universe_distance", safe_function<environment_get_universe_distance>},
     {"is_ge",          safe_function<environment_is_ge>},
     {"get_uvar",       safe_function<environment_get_uvar>},
     {"add_definition", safe_function<environment_add_definition>},