diff --git a/library/init/lean/elaborator/basic.lean b/library/init/lean/elaborator/basic.lean
index ece67c99b7..fbc474124b 100644
--- a/library/init/lean/elaborator/basic.lean
+++ b/library/init/lean/elaborator/basic.lean
@@ -37,6 +37,7 @@ structure ElabScope :=
 (options   : Options := {})
 (ns        : Name := Name.anonymous) -- current namespace
 (openDecls : List OpenDecl := [])
+(univs     : List Name := [])
 
 namespace ElabScope
 
@@ -388,9 +389,14 @@ namespace Elab
 instance {α} : Inhabited (Elab α) :=
 ⟨fun _ => default _⟩
 
+def getScope : Elab ElabScope :=
+do s ← get; pure s.scopes.head
+
 def getOpenDecls : Elab (List OpenDecl) :=
-do s ← get;
-   pure s.scopes.head.openDecls
+ElabScope.openDecls <$> getScope
+
+def getUniverses : Elab (List Name) :=
+ElabScope.univs <$> getScope
 
 def getNamespace : Elab Name :=
 do s ← get;
diff --git a/library/init/lean/elaborator/command.lean b/library/init/lean/elaborator/command.lean
index 659fc13aa5..949185cd09 100644
--- a/library/init/lean/elaborator/command.lean
+++ b/library/init/lean/elaborator/command.lean
@@ -161,6 +161,24 @@ fun n => do
   else
     elabOpenRenaming body
 
+def addUniverse (idStx : Syntax) : Elab Unit :=
+do
+let id := idStx.getId;
+univs ← getUniverses;
+if univs.elem id then
+  logError idStx ("a universe named '" ++ toString id ++ "' has already been declared in this Scope")
+else
+  modifyScope $ fun scope => { univs := id :: scope.univs, .. scope }
+
+@[builtinCommandElab «universe»] def elabUniverse : CommandElab :=
+fun n => do
+  addUniverse (n.getArg 1)
+
+@[builtinCommandElab «universes»] def elabUniverses : CommandElab :=
+fun n => do
+  let idsStx := n.getArg 1;
+  idsStx.mforArgs addUniverse
+
 /- We just ignore Lean3 notation declaration commands. -/
 @[builtinCommandElab «mixfix»] def elabMixfix : CommandElab := fun _ => pure ()
 @[builtinCommandElab «reserve»] def elabReserve : CommandElab := fun _ => pure ()