diff --git a/src/Axiom/DoubleNegationElimination.agda b/src/Axiom/DoubleNegationElimination.agda
index 777f08c017..c25679ef94 100644
--- a/src/Axiom/DoubleNegationElimination.agda
+++ b/src/Axiom/DoubleNegationElimination.agda
@@ -10,9 +10,13 @@ module Axiom.DoubleNegationElimination where
 
 open import Axiom.ExcludedMiddle
 open import Level
-open import Relation.Nullary
-open import Relation.Nullary.Negation
-open import Relation.Nullary.Decidable
+open import Relation.Nullary.Decidable.Core
+  using (decidable-stable; ¬¬-excluded-middle)
+open import Relation.Nullary.Negation.Core using (Stable)
+
+private
+  variable
+    ℓ : Level
 
 ------------------------------------------------------------------------
 -- Definition
@@ -20,16 +24,16 @@ open import Relation.Nullary.Decidable
 -- The classical statement of double negation elimination says that
 -- if a property is not not true then it is true.
 
-DoubleNegationElimination : (ℓ : Level) → Set (suc ℓ)
-DoubleNegationElimination ℓ = {P : Set ℓ} → ¬ ¬ P → P
+DoubleNegationElimination : ∀ ℓ → Set (suc ℓ)
+DoubleNegationElimination ℓ = {P : Set ℓ} → Stable P
 
 ------------------------------------------------------------------------
 -- Properties
 
 -- Double negation elimination is equivalent to excluded middle
 
-em⇒dne : ∀ {ℓ} → ExcludedMiddle ℓ → DoubleNegationElimination ℓ
+em⇒dne : ExcludedMiddle ℓ → DoubleNegationElimination ℓ
 em⇒dne em = decidable-stable em
 
-dne⇒em : ∀ {ℓ} → DoubleNegationElimination ℓ → ExcludedMiddle ℓ
+dne⇒em : DoubleNegationElimination ℓ → ExcludedMiddle ℓ
 dne⇒em dne = dne ¬¬-excluded-middle
diff --git a/src/Axiom/ExcludedMiddle.agda b/src/Axiom/ExcludedMiddle.agda
index 446da0cb1f..6d295eed0d 100644
--- a/src/Axiom/ExcludedMiddle.agda
+++ b/src/Axiom/ExcludedMiddle.agda
@@ -9,7 +9,7 @@
 module Axiom.ExcludedMiddle where
 
 open import Level
-open import Relation.Nullary
+open import Relation.Nullary.Decidable.Core using (Dec)
 
 ------------------------------------------------------------------------
 -- Definition
@@ -17,5 +17,5 @@ open import Relation.Nullary
 -- The classical statement of excluded middle says that every
 -- statement/set is decidable (i.e. it either holds or it doesn't hold).
 
-ExcludedMiddle : (ℓ : Level) → Set (suc ℓ)
+ExcludedMiddle : ∀ ℓ → Set (suc ℓ)
 ExcludedMiddle ℓ = {P : Set ℓ} → Dec P