diff --git a/Cubical/Data/Bool/Properties.agda b/Cubical/Data/Bool/Properties.agda
index 512cf59e4a..902a889449 100644
--- a/Cubical/Data/Bool/Properties.agda
+++ b/Cubical/Data/Bool/Properties.agda
@@ -24,7 +24,6 @@ open import Cubical.Data.Unit using (Unit; isPropUnit)
 open import Cubical.HITs.PropositionalTruncation hiding (rec)
 
 open import Cubical.Relation.Nullary
-open import Cubical.Relation.Nullary.DecidableEq
 
 private
   variable
diff --git a/Cubical/Data/DescendingList/Examples.agda b/Cubical/Data/DescendingList/Examples.agda
index 45a4efb214..a2f2a2aae8 100644
--- a/Cubical/Data/DescendingList/Examples.agda
+++ b/Cubical/Data/DescendingList/Examples.agda
@@ -19,7 +19,6 @@ open import Cubical.Data.Empty as ⊥
 open import Cubical.Data.Nat
 
 open import Cubical.Relation.Nullary
-open import Cubical.Relation.Nullary.DecidableEq
 
 open import Cubical.HITs.FiniteMultiset
 
diff --git a/Cubical/Data/DescendingList/Properties.agda b/Cubical/Data/DescendingList/Properties.agda
index b1f4e8eceb..3669d5e6d4 100644
--- a/Cubical/Data/DescendingList/Properties.agda
+++ b/Cubical/Data/DescendingList/Properties.agda
@@ -20,7 +20,6 @@ open import Cubical.Data.Unit
 open import Cubical.Data.List using (List ; [] ; _∷_)
 
 open import Cubical.Relation.Nullary
-open import Cubical.Relation.Nullary.DecidableEq
 
 open import Cubical.HITs.FiniteMultiset as FMSet hiding ([_])
 
diff --git a/Cubical/Data/DescendingList/Strict/Properties.agda b/Cubical/Data/DescendingList/Strict/Properties.agda
index f61950b8b3..d60cc36d03 100644
--- a/Cubical/Data/DescendingList/Strict/Properties.agda
+++ b/Cubical/Data/DescendingList/Strict/Properties.agda
@@ -17,7 +17,6 @@ open import Cubical.Data.DescendingList.Strict A _>_
 open import Cubical.HITs.ListedFiniteSet as LFSet renaming (_∈_ to _∈ʰ_)
 
 import Cubical.Data.Empty as ⊥
-open import Cubical.Relation.Nullary.DecidableEq
 
 open import Cubical.Relation.Nullary using (Dec; Discrete) renaming (¬_ to Type¬_)
 
diff --git a/Cubical/Data/Fin/LehmerCode.agda b/Cubical/Data/Fin/LehmerCode.agda
index afcce53ed6..1f2da9db8b 100644
--- a/Cubical/Data/Fin/LehmerCode.agda
+++ b/Cubical/Data/Fin/LehmerCode.agda
@@ -18,7 +18,6 @@ open import Cubical.Functions.Embedding
 open import Cubical.Functions.Surjection
 
 open import Cubical.Relation.Nullary
-open import Cubical.Relation.Nullary.DecidableEq
 
 open import Cubical.Data.Unit as ⊤
 open import Cubical.Data.Empty as ⊥
diff --git a/Cubical/Data/Fin/Properties.agda b/Cubical/Data/Fin/Properties.agda
index 954b0c37bd..b57b4ec979 100644
--- a/Cubical/Data/Fin/Properties.agda
+++ b/Cubical/Data/Fin/Properties.agda
@@ -26,7 +26,6 @@ open import Cubical.Data.Sigma
 open import Cubical.Data.FinData.Base renaming (Fin to FinData) hiding (¬Fin0 ; toℕ)
 
 open import Cubical.Relation.Nullary
-open import Cubical.Relation.Nullary.DecidableEq
 
 open import Cubical.Induction.WellFounded
 
diff --git a/Cubical/Data/FinSet/Properties.agda b/Cubical/Data/FinSet/Properties.agda
index 666681064e..d547146053 100644
--- a/Cubical/Data/FinSet/Properties.agda
+++ b/Cubical/Data/FinSet/Properties.agda
@@ -23,7 +23,6 @@ open import Cubical.Data.SumFin
 open import Cubical.Data.FinSet.Base
 
 open import Cubical.Relation.Nullary
-open import Cubical.Relation.Nullary.DecidableEq
 open import Cubical.Relation.Nullary.HLevels
 
 private
diff --git a/Cubical/Data/Int/Properties.agda b/Cubical/Data/Int/Properties.agda
index 8c5eeeb95b..aa4e16abb1 100644
--- a/Cubical/Data/Int/Properties.agda
+++ b/Cubical/Data/Int/Properties.agda
@@ -20,7 +20,6 @@ open import Cubical.Data.Sum
 open import Cubical.Data.Int.Base
 
 open import Cubical.Relation.Nullary
-open import Cubical.Relation.Nullary.DecidableEq
 
 sucPred : ∀ i → sucℤ (predℤ i) ≡ i
 sucPred (pos zero)    = refl
diff --git a/Cubical/Data/Nat/Properties.agda b/Cubical/Data/Nat/Properties.agda
index 6014b3ec59..3f81bcf568 100644
--- a/Cubical/Data/Nat/Properties.agda
+++ b/Cubical/Data/Nat/Properties.agda
@@ -13,7 +13,6 @@ open import Cubical.Data.Sigma
 open import Cubical.Data.Sum.Base
 
 open import Cubical.Relation.Nullary
-open import Cubical.Relation.Nullary.DecidableEq
 
 private
   variable
diff --git a/Cubical/Data/SumFin/Base.agda b/Cubical/Data/SumFin/Base.agda
index 31efed10b9..9c0f7c14ef 100644
--- a/Cubical/Data/SumFin/Base.agda
+++ b/Cubical/Data/SumFin/Base.agda
@@ -10,7 +10,6 @@ open import Cubical.Data.Sum using (_⊎_; inl; inr) public
 open import Cubical.Data.Nat hiding (elim)
 
 open import Cubical.Relation.Nullary
-open import Cubical.Relation.Nullary.DecidableEq
 
 private
   variable
diff --git a/Cubical/Foundations/HLevels.agda b/Cubical/Foundations/HLevels.agda
index 8ac4970082..cd3b5a9adf 100644
--- a/Cubical/Foundations/HLevels.agda
+++ b/Cubical/Foundations/HLevels.agda
@@ -4,7 +4,7 @@ Basic theory about h-levels/n-types:
 
 - Basic properties of isContr, isProp and isSet (definitions are in Prelude)
 
-- Hedberg's theorem can be found in Cubical/Relation/Nullary/DecidableEq
+- Hedberg's theorem can be found in Cubical/Relation/Nullary/Properties
 
 -}
 {-# OPTIONS --safe #-}
diff --git a/Cubical/HITs/AssocList/Properties.agda b/Cubical/HITs/AssocList/Properties.agda
index 95d8d7337b..cd87b4b7de 100644
--- a/Cubical/HITs/AssocList/Properties.agda
+++ b/Cubical/HITs/AssocList/Properties.agda
@@ -11,7 +11,6 @@ open import Cubical.Foundations.Univalence
 open import Cubical.Foundations.SIP
 
 open import Cubical.Relation.Nullary
-open import Cubical.Relation.Nullary.DecidableEq
 
 open import Cubical.Structures.MultiSet
 
diff --git a/Cubical/HITs/FiniteMultiset/CountExtensionality.agda b/Cubical/HITs/FiniteMultiset/CountExtensionality.agda
index 79bea106e0..4cae1506c7 100644
--- a/Cubical/HITs/FiniteMultiset/CountExtensionality.agda
+++ b/Cubical/HITs/FiniteMultiset/CountExtensionality.agda
@@ -12,7 +12,6 @@ open import Cubical.Relation.Nullary
 open import Cubical.HITs.FiniteMultiset.Base
 open import Cubical.HITs.FiniteMultiset.Properties as FMS
 open import Cubical.Structures.MultiSet
-open import Cubical.Relation.Nullary.DecidableEq
 
 
 private
diff --git a/Cubical/HITs/FiniteMultiset/Properties.agda b/Cubical/HITs/FiniteMultiset/Properties.agda
index 1a4e240285..81f96e341f 100644
--- a/Cubical/HITs/FiniteMultiset/Properties.agda
+++ b/Cubical/HITs/FiniteMultiset/Properties.agda
@@ -8,7 +8,6 @@ open import Cubical.Data.Empty as ⊥
 open import Cubical.Relation.Nullary
 open import Cubical.HITs.FiniteMultiset.Base
 open import Cubical.Structures.MultiSet
-open import Cubical.Relation.Nullary.DecidableEq
 
 private
   variable
diff --git a/Cubical/Relation/Nullary/DecidableEq.agda b/Cubical/Relation/Nullary/DecidableEq.agda
deleted file mode 100644
index 7c66fe00a6..0000000000
--- a/Cubical/Relation/Nullary/DecidableEq.agda
+++ /dev/null
@@ -1,5 +0,0 @@
-{-# OPTIONS --safe #-}
-module Cubical.Relation.Nullary.DecidableEq where
-
-open import Cubical.Relation.Nullary.Properties
-  using (Dec→Stable; Discrete→isSet) public