From 16c15b5c784f68a8e664d55f61065ce3dad7745d Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Fri, 27 Feb 2026 11:19:34 +0000
Subject: [PATCH 1/2] [ rename ] decidability for
 `Relation.Binary.Construct.Intersection`

---
 CHANGELOG.md                                  | 10 +++++++++
 .../Binary/Construct/Intersection.agda        | 21 +++++++++++++++++--
 src/Relation/Binary/Construct/Union.agda      | 21 +++++++++++++++++--
 3 files changed, 48 insertions(+), 4 deletions(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index f83411bc22..7e0df82f36 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -99,6 +99,16 @@ Deprecated names
   truncate-irrelevant  ↦  Relation.Binary.PropositionalEquality.Core.refl
   ```
 
+* In `Relation.Binary.Construct.Intersection`:
+  ```agda
+  decidable     ↦   _∩?_
+  ```
+
+* In `Relation.Binary.Construct.Union`:
+  ```agda
+  decidable     ↦   _∪?_
+  ```
+
 * In `Relation.Nullary.Decidable.Core`:
   ```agda
   ⊤-dec     ↦   ⊤?
diff --git a/src/Relation/Binary/Construct/Intersection.agda b/src/Relation/Binary/Construct/Intersection.agda
index b5dda5737e..aa6a1b9274 100644
--- a/src/Relation/Binary/Construct/Intersection.agda
+++ b/src/Relation/Binary/Construct/Intersection.agda
@@ -86,8 +86,10 @@ module _ (≈ : Rel A ℓ₁) (L : Rel A ℓ₂) (R : Rel A ℓ₃) where
 
 module _ {L : REL A B ℓ₁} {R : REL A B ℓ₂} where
 
-  decidable : Decidable L → Decidable R → Decidable (L ∩ R)
-  decidable L? R? x y = L? x y ×? R? x y
+  infixl 6 _∩?_
+
+  _∩?_ : Decidable L → Decidable R → Decidable (L ∩ R)
+  _∩?_ L? R? x y = L? x y ×? R? x y
 
 ------------------------------------------------------------------------
 -- Structures
@@ -144,3 +146,18 @@ isStrictPartialOrderʳ {L = L} {≈ = ≈} {R = R} transₗ respₗ Oᵣ = recor
   ; trans         = transitive L R transₗ Oᵣ.trans
   ; <-resp-≈      = respects₂ ≈ L R respₗ Oᵣ.<-resp-≈
   } where module Oᵣ = IsStrictPartialOrder Oᵣ
+
+
+------------------------------------------------------------------------
+-- DEPRECATED NAMES
+------------------------------------------------------------------------
+-- Please use the new names as continuing support for the old names is
+-- not guaranteed.
+
+-- version 2.4
+
+decidable = _∩?_
+{-# WARNING_ON_USAGE decidable
+"Warning: decidable was deprecated in v2.4.
+Please use _∩?_ instead."
+#-}
diff --git a/src/Relation/Binary/Construct/Union.agda b/src/Relation/Binary/Construct/Union.agda
index a99c54dd1b..1096242437 100644
--- a/src/Relation/Binary/Construct/Union.agda
+++ b/src/Relation/Binary/Construct/Union.agda
@@ -84,5 +84,22 @@ module _ (≈ : REL A B ℓ₁) (L : REL A B ℓ₂) (R : REL A B ℓ₃) where
 
 module _ {L : REL A B ℓ₁} {R : REL A B ℓ₂} where
 
-  decidable : Decidable L → Decidable R → Decidable (L ∪ R)
-  decidable L? R? x y = L? x y ⊎? R? x y
+  infixr 6 _∪?_
+
+  _∪?_ : Decidable L → Decidable R → Decidable (L ∪ R)
+  _∪?_ L? R? x y = L? x y ⊎? R? x y
+
+
+------------------------------------------------------------------------
+-- DEPRECATED NAMES
+------------------------------------------------------------------------
+-- Please use the new names as continuing support for the old names is
+-- not guaranteed.
+
+-- version 2.4
+
+decidable = _∪?_
+{-# WARNING_ON_USAGE decidable
+"Warning: decidable was deprecated in v2.4.
+Please use _∪?_ instead."
+#-}

From 76b6d059114d5e58b5bafbe021d7a1b2a594a406 Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Fri, 27 Feb 2026 11:32:21 +0000
Subject: [PATCH 2/2] d'oh

---
 src/Relation/Binary/Construct/Intersection.agda | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/Relation/Binary/Construct/Intersection.agda b/src/Relation/Binary/Construct/Intersection.agda
index aa6a1b9274..16603994b6 100644
--- a/src/Relation/Binary/Construct/Intersection.agda
+++ b/src/Relation/Binary/Construct/Intersection.agda
@@ -104,7 +104,7 @@ isEquivalence {L = L} {R = R} eqₗ eqᵣ = record
 isDecEquivalence : IsDecEquivalence L → IsDecEquivalence R → IsDecEquivalence (L ∩ R)
 isDecEquivalence eqₗ eqᵣ = record
   { isEquivalence = isEquivalence L.isEquivalence R.isEquivalence
-  ; _≟_           = decidable L._≟_ R._≟_
+  ; _≟_           = L._≟_ ∩? R._≟_
   } where module L = IsDecEquivalence eqₗ; module R = IsDecEquivalence eqᵣ
 
 isPreorder : IsPreorder ≈ L → IsPreorder ≈ R → IsPreorder ≈ (L ∩ R)