diff --git a/CHANGELOG.md b/CHANGELOG.md
index 1da4157a62..72bcb575da 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -881,7 +881,8 @@ Non-backwards compatible changes
     lookup : All P xs → (∀ {x} → x ∈ₚ xs → P x)
     lookupₛ : P Respects _≈_ → All P xs → (∀ {x} → x ∈ xs → P x)
     ```
-
+  * `excluded-middle` in `Relation.Nullary.Decidable.Core` has been renamed to
+    `¬¬-excluded-middle`.
 
 Major improvements
 ------------------
diff --git a/src/Axiom/DoubleNegationElimination.agda b/src/Axiom/DoubleNegationElimination.agda
index 49e8b01eaa..777f08c017 100644
--- a/src/Axiom/DoubleNegationElimination.agda
+++ b/src/Axiom/DoubleNegationElimination.agda
@@ -32,4 +32,4 @@ em⇒dne : ∀ {ℓ} → ExcludedMiddle ℓ → DoubleNegationElimination ℓ
 em⇒dne em = decidable-stable em
 
 dne⇒em : ∀ {ℓ} → DoubleNegationElimination ℓ → ExcludedMiddle ℓ
-dne⇒em dne = dne excluded-middle
+dne⇒em dne = dne ¬¬-excluded-middle
diff --git a/src/Codata/Musical/Colist.agda b/src/Codata/Musical/Colist.agda
index 2ec01be70f..d70a101f6a 100644
--- a/src/Codata/Musical/Colist.agda
+++ b/src/Codata/Musical/Colist.agda
@@ -36,7 +36,7 @@ open import Relation.Binary.PropositionalEquality as P using (_≡_)
 open import Relation.Nullary.Reflects using (invert)
 open import Relation.Nullary
 open import Relation.Nullary.Negation
-open import Relation.Nullary.Decidable using (excluded-middle)
+open import Relation.Nullary.Decidable using (¬¬-excluded-middle)
 open import Relation.Unary using (Pred)
 
 private
@@ -244,7 +244,7 @@ not-finite-is-infinite (x ∷ xs) hyp =
 
 finite-or-infinite :
   (xs : Colist A) → ¬ ¬ (Finite xs ⊎ Infinite xs)
-finite-or-infinite xs = helper <$> excluded-middle
+finite-or-infinite xs = helper <$> ¬¬-excluded-middle
   where
   helper : Dec (Finite xs) → Finite xs ⊎ Infinite xs
   helper ( true because  [fin]) = inj₁ (invert [fin])
diff --git a/src/Data/List/Membership/Propositional/Properties.agda b/src/Data/List/Membership/Propositional/Properties.agda
index 364c6d29b8..2ddd26e02b 100644
--- a/src/Data/List/Membership/Propositional/Properties.agda
+++ b/src/Data/List/Membership/Propositional/Properties.agda
@@ -43,7 +43,7 @@ import Relation.Nullary.Reflects as Reflects
 open import Relation.Nullary.Reflects using (invert)
 open import Relation.Nullary using (¬_; Dec; does; yes; no; _because_)
 open import Relation.Nullary.Negation using (contradiction)
-open import Relation.Nullary.Decidable using (excluded-middle)
+open import Relation.Nullary.Decidable using (¬¬-excluded-middle)
 
 private
   open module ListMonad {ℓ} = RawMonad (monad {ℓ = ℓ})
@@ -344,7 +344,7 @@ module _ {_•_ : Op₂ A} where
 
 finite : (f : ℕ ↣ A) → ∀ xs → ¬ (∀ i → Injection.to f ⟨$⟩ i ∈ xs)
 finite inj []       fᵢ∈[]   = ¬Any[] (fᵢ∈[] 0)
-finite inj (x ∷ xs) fᵢ∈x∷xs = excluded-middle helper
+finite inj (x ∷ xs) fᵢ∈x∷xs = ¬¬-excluded-middle helper
   where
   open Injection inj renaming (injective to f-inj)
 
diff --git a/src/Effect/Monad/Partiality.agda b/src/Effect/Monad/Partiality.agda
index e6cfdd1c05..194b079339 100644
--- a/src/Effect/Monad/Partiality.agda
+++ b/src/Effect/Monad/Partiality.agda
@@ -401,7 +401,7 @@ module _ {A : Set a} {_∼_ : A → A → Set ℓ} where
   now-or-never : Reflexive _∼_ →
                  ∀ {k} (x : A ⊥) →
                  ¬ ¬ ((∃ λ y → x ⇓[ other k ] y) ⊎ x ⇑[ other k ])
-  now-or-never refl x = helper <$> excluded-middle
+  now-or-never refl x = helper <$> ¬¬-excluded-middle
     where
     open RawMonad ¬¬-Monad
 
diff --git a/src/Relation/Nullary/Decidable/Core.agda b/src/Relation/Nullary/Decidable/Core.agda
index e06dc32239..6296db24df 100644
--- a/src/Relation/Nullary/Decidable/Core.agda
+++ b/src/Relation/Nullary/Decidable/Core.agda
@@ -175,5 +175,13 @@ decidable-stable (no ¬p) ¬¬p = ⊥-elim (¬¬p ¬p)
 -- A double-negation-translated variant of excluded middle (or: every
 -- nullary relation is decidable in the double-negation monad).
 
+¬¬-excluded-middle : DoubleNegation (Dec P)
+¬¬-excluded-middle ¬h = ¬h (no (λ p → ¬h (yes p)))
+
 excluded-middle : DoubleNegation (Dec P)
-excluded-middle ¬h = ¬h (no (λ p → ¬h (yes p)))
+excluded-middle = ¬¬-excluded-middle
+
+{-# WARNING_ON_USAGE excluded-middle
+"Warning: excluded-middle was deprecated in v2.0.
+Please use ¬¬-excluded-middle instead."
+#-}
diff --git a/src/Relation/Nullary/Negation.agda b/src/Relation/Nullary/Negation.agda
index 5111db897f..59e96f3429 100644
--- a/src/Relation/Nullary/Negation.agda
+++ b/src/Relation/Nullary/Negation.agda
@@ -15,7 +15,7 @@ open import Data.Product.Base as Prod using (_,_; Σ; Σ-syntax; ∃; curry; unc
 open import Data.Sum.Base as Sum using (_⊎_; inj₁; inj₂; [_,_])
 open import Function.Base using (flip; _∘_; const; _∘′_)
 open import Level using (Level)
-open import Relation.Nullary.Decidable.Core using (Dec; yes; no; excluded-middle)
+open import Relation.Nullary.Decidable.Core using (Dec; yes; no; ¬¬-excluded-middle)
 open import Relation.Unary using (Universal)
 
 private
@@ -85,7 +85,7 @@ call/cc hyp ¬p = hyp (λ p → ⊥-elim (¬p p)) ¬p
 
 independence-of-premise : {R : Q → Set r} →
                           Q → (P → Σ Q R) → DoubleNegation (Σ[ x ∈ Q ] (P → R x))
-independence-of-premise {P = P} q f = ¬¬-map helper excluded-middle
+independence-of-premise {P = P} q f = ¬¬-map helper ¬¬-excluded-middle
   where
   helper : Dec P → _
   helper (yes p) = Prod.map₂ const (f p)
@@ -94,7 +94,7 @@ independence-of-premise {P = P} q f = ¬¬-map helper excluded-middle
 -- The independence of premise rule for binary sums.
 
 independence-of-premise-⊎ : (P → Q ⊎ R) → DoubleNegation ((P → Q) ⊎ (P → R))
-independence-of-premise-⊎ {P = P} f = ¬¬-map helper excluded-middle
+independence-of-premise-⊎ {P = P} f = ¬¬-map helper ¬¬-excluded-middle
   where
   helper : Dec P → _
   helper (yes p) = Sum.map const const (f p)