From 744e1101b4eb21a9165f7a6fe79057b17031f27d Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Sat, 11 Oct 2025 08:43:38 +0100
Subject: [PATCH] fix: naming convention

---
 CHANGELOG.md                       |  9 +++++
 src/Relation/Nullary/Negation.agda | 59 +++++++++++++++++++++++++-----
 2 files changed, 58 insertions(+), 10 deletions(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 12039b4aed..1803b067c8 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -46,6 +46,15 @@ Deprecated names
   interchange  ↦   medial
   ```
 
+* In `Relation.Nullary.Negation`:
+  ```agda
+  ∃⟶¬∀¬  ↦   ∃⇒¬∀¬
+  ∀⟶¬∃¬  ↦   ∀⇒¬∃¬
+  ¬∃⟶∀¬  ↦   ¬∃⇒∀¬
+  ∀¬⟶¬∃  ↦   ∀¬⇒¬∃
+  ∃¬⟶¬∀  ↦   ∃¬⇒¬∀
+  ```
+
 New modules
 -----------
 
diff --git a/src/Relation/Nullary/Negation.agda b/src/Relation/Nullary/Negation.agda
index e451d95b07..8c21aa9bc2 100644
--- a/src/Relation/Nullary/Negation.agda
+++ b/src/Relation/Nullary/Negation.agda
@@ -32,20 +32,20 @@ open import Relation.Nullary.Negation.Core public
 ------------------------------------------------------------------------
 -- Quantifier juggling
 
-∃⟶¬∀¬ : ∃ P → ¬ (∀ x → ¬ P x)
-∃⟶¬∀¬ = flip uncurry
+∃⇒¬∀¬ : ∃ P → ¬ (∀ x → ¬ P x)
+∃⇒¬∀¬ = flip uncurry
 
-∀⟶¬∃¬ : (∀ x → P x) → ¬ ∃ λ x → ¬ P x
-∀⟶¬∃¬ ∀xPx (x , ¬Px) = ¬Px (∀xPx x)
+∀⇒¬∃¬ : (∀ x → P x) → ¬ ∃ λ x → ¬ P x
+∀⇒¬∃¬ ∀xPx (x , ¬Px) = ¬Px (∀xPx x)
 
-¬∃⟶∀¬ : ¬ ∃ (λ x → P x) → ∀ x → ¬ P x
-¬∃⟶∀¬ = curry
+¬∃⇒∀¬ : ¬ ∃ (λ x → P x) → ∀ x → ¬ P x
+¬∃⇒∀¬ = curry
 
-∀¬⟶¬∃ : (∀ x → ¬ P x) → ¬ ∃ (λ x → P x)
-∀¬⟶¬∃ = uncurry
+∀¬⇒¬∃ : (∀ x → ¬ P x) → ¬ ∃ (λ x → P x)
+∀¬⇒¬∃ = uncurry
 
-∃¬⟶¬∀ : ∃ (λ x → ¬ P x) → ¬ (∀ x → P x)
-∃¬⟶¬∀ = flip ∀⟶¬∃¬
+∃¬⇒¬∀ : ∃ (λ x → ¬ P x) → ¬ (∀ x → P x)
+∃¬⇒¬∀ = flip ∀⇒¬∃¬
 
 ------------------------------------------------------------------------
 -- Double Negation
@@ -106,3 +106,42 @@ private
     helper : ∃ (λ b → A → if b then B else C) → (A → B) ⊎ (A → C)
     helper (true  , f) = inj₁ f
     helper (false , f) = inj₂ f
+
+
+------------------------------------------------------------------------
+-- DEPRECATED NAMES
+------------------------------------------------------------------------
+-- Please use the new names as continuing support for the old names is
+-- not guaranteed.
+
+-- Version 2.4
+
+∃⟶¬∀¬ = ∃⇒¬∀¬
+{-# WARNING_ON_USAGE ∃⟶¬∀¬
+"Warning: ∃⟶¬∀¬ was deprecated in v2.4.
+Please use ∃⇒¬∀¬ instead."
+#-}
+
+∀⟶¬∃¬ = ∀⇒¬∃¬
+{-# WARNING_ON_USAGE ∀⟶¬∃¬
+"Warning: ∀⟶¬∃¬ was deprecated in v2.4.
+Please use ∀⇒¬∃¬ instead."
+#-}
+
+¬∃⟶∀¬ = ¬∃⇒∀¬
+{-# WARNING_ON_USAGE ¬∃⟶∀¬
+"Warning: ¬∃⟶∀¬ was deprecated in v2.4.
+Please use ¬∃⇒∀¬ instead."
+#-}
+
+∀¬⟶¬∃ = ∀¬⇒¬∃
+{-# WARNING_ON_USAGE ∀¬⟶¬∃
+"Warning: ∀¬⟶¬∃ was deprecated in v2.4.
+Please use ∀¬⇒¬∃ instead."
+#-}
+
+∃¬⟶¬∀ = ∃¬⇒¬∀
+{-# WARNING_ON_USAGE ∃¬⟶¬∀
+"Warning: ∃¬⟶¬∀ was deprecated in v2.4.
+Please use ∃¬⇒¬∀ instead."
+#-}