diff --git a/examples/ex7.lean b/examples/ex7.lean
index 9a176f435f..a6b54ddcdc 100644
--- a/examples/ex7.lean
+++ b/examples/ex7.lean
@@ -8,13 +8,13 @@ Check x
 Check Type max u m
 Show Type u+3
 Check Type u+3
-Check Type u ⊓ m
-Check Type u ⊓ m ⊓ 3
-Show Type u+1 ⊓ m ⊓ 3
-Check Type u+1 ⊓ m ⊓ 3
+Check Type u ⊔ m
+Check Type u ⊔ m ⊔ 3
+Show Type u+1 ⊔ m ⊔ 3
+Check Type u+1 ⊔ m ⊔ 3
 Show Type u -> Type 5
 Check Type u -> Type 5
-Check Type m ⊓ 3 -> Type u+5
-Show Type m ⊓ 3 -> Type u -> Type 5
-Check Type m ⊓ 3 -> Type u -> Type 5
+Check Type m ⊔ 3 -> Type u+5
+Show Type m ⊔ 3 -> Type u -> Type 5
+Check Type m ⊔ 3 -> Type u -> Type 5
 Show Type u
diff --git a/src/frontend/parser.cpp b/src/frontend/parser.cpp
index c0f15c209c..066c68f0eb 100644
--- a/src/frontend/parser.cpp
+++ b/src/frontend/parser.cpp
@@ -40,7 +40,7 @@ static name g_mixfixc_kwd("Mixfixc");
 // ==========================================
 // Support for parsing levels
 static name g_max_name("max");
-static name g_cup_name("\u2293");
+static name g_cup_name("\u2294");
 static name g_plus_name("+");
 static unsigned g_level_plus_prec = 10;
 static unsigned g_level_cup_prec  = 5;
diff --git a/src/kernel/level.cpp b/src/kernel/level.cpp
index edabd90c98..fcbbdc82fb 100644
--- a/src/kernel/level.cpp
+++ b/src/kernel/level.cpp
@@ -210,7 +210,7 @@ format pp(level const & l) {
     case level_kind::Max: {
         format r = pp(max_level(l, 0));
         for (unsigned i = 1; i < max_size(l); i++) {
-            r += format(" \u2293 ");
+            r += format{space(), format("\u2294"), space()};
             r += pp(max_level(l, i));
         }
         return r;