diff --git a/src/Init/Data.lean b/src/Init/Data.lean
index 91938d7707e1..8aceacd4189d 100644
--- a/src/Init/Data.lean
+++ b/src/Init/Data.lean
@@ -37,3 +37,5 @@ import Init.Data.Cast
 import Init.Data.Sum
 import Init.Data.BEq
 import Init.Data.Subtype
+import Init.Data.ULift
+import Init.Data.PLift
diff --git a/src/Init/Data/PLift.lean b/src/Init/Data/PLift.lean
new file mode 100644
index 000000000000..d03ab7ccda6f
--- /dev/null
+++ b/src/Init/Data/PLift.lean
@@ -0,0 +1,12 @@
+/-
+Copyright (c) 2024 Lean FRO. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Kim Morrison
+-/
+prelude
+import Init.Core
+
+deriving instance DecidableEq for PLift
+
+instance [Subsingleton α] : Subsingleton (PLift α) where
+  allEq := fun ⟨a⟩ ⟨b⟩ => congrArg PLift.up (Subsingleton.elim a b)
diff --git a/src/Init/Data/ULift.lean b/src/Init/Data/ULift.lean
new file mode 100644
index 000000000000..91276ebfea80
--- /dev/null
+++ b/src/Init/Data/ULift.lean
@@ -0,0 +1,12 @@
+/-
+Copyright (c) 2024 Lean FRO. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Kim Morrison
+-/
+prelude
+import Init.Core
+
+deriving instance DecidableEq for ULift
+
+instance [Subsingleton α] : Subsingleton (ULift α) where
+  allEq := fun ⟨a⟩ ⟨b⟩ => congrArg ULift.up (Subsingleton.elim a b)