diff --git a/src/Bootstrap.lean b/src/Bootstrap.lean
index ebdfb2611a..54d9d3bd9f 100644
--- a/src/Bootstrap.lean
+++ b/src/Bootstrap.lean
@@ -3,4 +3,4 @@ Copyright (c) 2020 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
-import Bootstrap.Dynamic
+import Bootstrap.Empty
diff --git a/src/Bootstrap/Empty.lean b/src/Bootstrap/Empty.lean
new file mode 100644
index 0000000000..e69de29bb2
diff --git a/src/Init.lean b/src/Init.lean
index ac79a0116e..40dcc8541c 100644
--- a/src/Init.lean
+++ b/src/Init.lean
@@ -15,6 +15,7 @@ import Init.WFTactics
 import Init.Data
 import Init.System
 import Init.Util
+import Init.Dynamic
 import Init.ShareCommon
 import Init.Meta
 import Init.NotationExtra
diff --git a/src/Bootstrap/Dynamic.lean b/src/Init/Dynamic.lean
similarity index 99%
rename from src/Bootstrap/Dynamic.lean
rename to src/Init/Dynamic.lean
index 8d6d390cf1..ec1cc5b8f4 100644
--- a/src/Bootstrap/Dynamic.lean
+++ b/src/Init/Dynamic.lean
@@ -4,8 +4,9 @@ Released under Apache 2.0 license as described in the file LICENSE.
 
 Authors: Gabriel Ebner
 -/
+prelude
+import Init.Core
 
-namespace Std
 open Lean
 
 -- Implementation detail of TypeName, since classes cannot be opaque
diff --git a/src/Lean/Elab/Deriving/TypeName.lean b/src/Lean/Elab/Deriving/TypeName.lean
index b386cc675e..17a0cc896a 100644
--- a/src/Lean/Elab/Deriving/TypeName.lean
+++ b/src/Lean/Elab/Deriving/TypeName.lean
@@ -14,13 +14,12 @@ private def deriveTypeNameInstance (declNames : Array Name) : CommandElabM Bool
     let cinfo ← getConstInfo declName
     unless cinfo.levelParams.isEmpty do
       throwError m!"{mkConst declName} has universe level parameters"
-    let TypeName := mkIdent `TypeName
     elabCommand <| ← withFreshMacroScope `(
-      unsafe def instImpl : $TypeName @$(mkCIdent declName) := .mk _ $(quote declName)
-      @[implementedBy instImpl] opaque inst : $TypeName @$(mkCIdent declName)
-      instance : $TypeName @$(mkCIdent declName) := inst
+      unsafe def instImpl : TypeName @$(mkCIdent declName) := .mk _ $(quote declName)
+      @[implementedBy instImpl] opaque inst : TypeName @$(mkCIdent declName)
+      instance : TypeName @$(mkCIdent declName) := inst
     )
   return true
 
 initialize
-  registerDerivingHandler `TypeName deriveTypeNameInstance
+  registerDerivingHandler ``TypeName deriveTypeNameInstance
diff --git a/src/Lean/Server/Rpc/Basic.lean b/src/Lean/Server/Rpc/Basic.lean
index 4ca7d32973..7318502a08 100644
--- a/src/Lean/Server/Rpc/Basic.lean
+++ b/src/Lean/Server/Rpc/Basic.lean
@@ -5,7 +5,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Wojciech Nawrocki
 -/
 import Lean.Data.Json
-import Bootstrap.Dynamic
 
 /-! Allows LSP clients to make Remote Procedure Calls to the server.
 
diff --git a/src/Lean/Widget/Basic.lean b/src/Lean/Widget/Basic.lean
index 52c2e442df..4fe67fa7ea 100644
--- a/src/Lean/Widget/Basic.lean
+++ b/src/Lean/Widget/Basic.lean
@@ -18,9 +18,9 @@ functionality is purpose-specific to showing the contents of infoview popups.
 structure InfoWithCtx where
   ctx  : Elab.ContextInfo
   info : Elab.Info
-  deriving Inhabited, Std.TypeName
+  deriving Inhabited, TypeName
 
-deriving instance Std.TypeName for MessageData
+deriving instance TypeName for MessageData
 
 instance : ToJson FVarId := ⟨fun f => toJson f.name⟩
 instance : ToJson MVarId := ⟨fun f => toJson f.name⟩
diff --git a/src/Lean/Widget/InteractiveDiagnostic.lean b/src/Lean/Widget/InteractiveDiagnostic.lean
index cf8f2cb682..01c8078e04 100644
--- a/src/Lean/Widget/InteractiveDiagnostic.lean
+++ b/src/Lean/Widget/InteractiveDiagnostic.lean
@@ -19,7 +19,7 @@ inductive StrictOrLazy (α β : Type) : Type
 structure LazyTraceChildren where
   indent : Nat
   children : Array (WithRpcRef MessageData)
-  deriving Std.TypeName
+  deriving TypeName
 
 inductive MsgEmbed where
   | expr : CodeWithInfos → MsgEmbed
diff --git a/tests/lean/derivingRpcEncoding.lean b/tests/lean/derivingRpcEncoding.lean
index 7008783919..de5eb9233f 100644
--- a/tests/lean/derivingRpcEncoding.lean
+++ b/tests/lean/derivingRpcEncoding.lean
@@ -14,7 +14,7 @@ def test (α : Type) [RpcEncodable α] (a : α) := M.run do
 
 structure FooRef where
   a : Array Nat
-  deriving Inhabited, Std.TypeName
+  deriving Inhabited, TypeName
 
 #check instTypeNameFooRef
 #eval test (WithRpcRef FooRef) default
diff --git a/tests/lean/derivingRpcEncoding.lean.expected.out b/tests/lean/derivingRpcEncoding.lean.expected.out
index c2e356e0ce..df4e315384 100644
--- a/tests/lean/derivingRpcEncoding.lean.expected.out
+++ b/tests/lean/derivingRpcEncoding.lean.expected.out
@@ -1,4 +1,4 @@
-instTypeNameFooRef : Std.TypeName FooRef
+instTypeNameFooRef : TypeName FooRef
 ok: {"p": "0"}
 instRpcEncodableBar : RpcEncodable Bar
 ok: {"fooRef": {"p": "0"}, "fooJson": {"s": ""}}