From 90ca0a713e89e00013f39633fb4eaa2941197837 Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Mon, 2 Mar 2026 11:46:40 +0000
Subject: [PATCH 1/6] =?UTF-8?q?[=20refactor=20]=20name=20of=20`Data.Produc?=
 =?UTF-8?q?t.Relation.Binary.Pointwise.NonDependent.=C3=97-decidable`?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 CHANGELOG.md                                  |  5 +++++
 .../Binary/Pointwise/NonDependent.agda        | 21 ++++++++++++++++---
 2 files changed, 23 insertions(+), 3 deletions(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index f83411bc22..bd9572122f 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -89,6 +89,11 @@ Deprecated names
   ¬∀⟶∃¬-          ↦   ¬∀⇒∃¬
   ```
 
+* In `Data.Product.Relation.Binary.Pointwise.NonDependent`:
+  ```agda
+  ×-decidable  ↦  pointwise?
+  ```
+
 * In `Data.Rational.Properties`:
   ```agda
   nonPos*nonPos⇒nonPos  ↦  nonPos*nonPos⇒nonNeg
diff --git a/src/Data/Product/Relation/Binary/Pointwise/NonDependent.agda b/src/Data/Product/Relation/Binary/Pointwise/NonDependent.agda
index 20a1d5ce01..71c2b10d1b 100644
--- a/src/Data/Product/Relation/Binary/Pointwise/NonDependent.agda
+++ b/src/Data/Product/Relation/Binary/Pointwise/NonDependent.agda
@@ -87,8 +87,8 @@ Pointwise R S (a , c) (b , d) = (R a b) × (S c d)
 ... | inj₂ y₁∼x₁ | inj₂ y₂∼x₂ = inj₂ (     y₁∼x₁ , y₂∼x₂)
 ... | inj₂ y₁∼x₁ | inj₁ x₂∼y₂ = inj₁ (sym₁ y₁∼x₁ , x₂∼y₂)
 
-×-decidable : Decidable R → Decidable S → Decidable (Pointwise R S)
-×-decidable _≟₁_ _≟₂_ (x₁ , x₂) (y₁ , y₂) = (x₁ ≟₁ y₁) ×? (x₂ ≟₂ y₂)
+pointwise? : Decidable R → Decidable S → Decidable (Pointwise R S)
+pointwise? _R?_ _S?_ (x₁ , x₂) (y₁ , y₂) = (x₁ R? y₁) ×? (x₂ S? y₂)
 
 ------------------------------------------------------------------------
 -- Structures can also be combined.
@@ -108,7 +108,7 @@ Pointwise R S (a , c) (b , d) = (R a b) × (S c d)
 ×-isDecEquivalence eq₁ eq₂ = record
   { isEquivalence = ×-isEquivalence
                       (isEquivalence eq₁) (isEquivalence eq₂)
-  ; _≟_           = ×-decidable (_≟_ eq₁) (_≟_ eq₂)
+  ; _≟_           = pointwise? (_≟_ eq₁) (_≟_ eq₂)
   } where open IsDecEquivalence
 
 ×-isPreorder : IsPreorder ≈₁ R → IsPreorder ≈₂ S →
@@ -204,3 +204,18 @@ Pointwise-≡↔≡ = record
   ; from-cong  = ≡⇒≡×≡
   ; inverse    = ≡×≡⇒≡ , ≡⇒≡×≡
   }
+
+
+------------------------------------------------------------------------
+-- DEPRECATED NAMES
+------------------------------------------------------------------------
+-- Please use the new names as continuing support for the old names is
+-- not guaranteed.
+
+-- Version 2.4
+
+×-decidable = pointwise?
+{-# WARNING_ON_USAGE ×-decidable
+"Warning: ×-decidable was deprecated in v2.4.
+Please use pointwise? instead."
+#-}

From ebc7ee9c372caad6fbddf1808e67eec548648fe2 Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Mon, 2 Mar 2026 11:55:08 +0000
Subject: [PATCH 2/6] fix: use of `pointwise?`

---
 src/Data/Product/Relation/Binary/Lex/NonStrict.agda | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/Data/Product/Relation/Binary/Lex/NonStrict.agda b/src/Data/Product/Relation/Binary/Lex/NonStrict.agda
index 599a7d011c..365e28468a 100644
--- a/src/Data/Product/Relation/Binary/Lex/NonStrict.agda
+++ b/src/Data/Product/Relation/Binary/Lex/NonStrict.agda
@@ -157,7 +157,7 @@ module _ {_≈₁_ : Rel A ℓ₁} {_≤₁_ : Rel A ℓ₂}
     { isTotalOrder = ×-isTotalOrder (_≟_ to₁)
                                     (isTotalOrder to₁)
                                     (isTotalOrder to₂)
-    ; _≟_          = Pointwise.×-decidable (_≟_ to₁) (_≟_ to₂)
+    ; _≟_          = Pointwise.pointwise? (_≟_ to₁) (_≟_ to₂)
     ; _≤?_         = ×-decidable (_≟_ to₁) (_≤?_ to₁) (_≤?_ to₂)
     }
     where open IsDecTotalOrder

From ebdc280a4d6a5cc8f1c2679c75544dab9d08b091 Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Tue, 3 Mar 2026 09:40:21 +0000
Subject: [PATCH 3/6] fix: tighten `import`s

---
 src/Data/Product/Relation/Binary/Pointwise/NonDependent.agda | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/Data/Product/Relation/Binary/Pointwise/NonDependent.agda b/src/Data/Product/Relation/Binary/Pointwise/NonDependent.agda
index 71c2b10d1b..7a1b8c80eb 100644
--- a/src/Data/Product/Relation/Binary/Pointwise/NonDependent.agda
+++ b/src/Data/Product/Relation/Binary/Pointwise/NonDependent.agda
@@ -13,7 +13,7 @@ open import Data.Sum.Base using (inj₁; inj₂)
 open import Level using (Level; _⊔_; 0ℓ)
 open import Function.Base using (id)
 open import Function.Bundles using (Inverse)
-open import Relation.Nullary.Decidable using (_×?_)
+open import Relation.Nullary.Decidable.Core using (_×?_)
 open import Relation.Binary.Core using (REL; Rel; _⇒_)
 open import Relation.Binary.Bundles
   using (Setoid; DecSetoid; Preorder; Poset; StrictPartialOrder)

From e35807f34de3521253b5032f35f65455904feab8 Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Thu, 5 Mar 2026 14:34:28 +0000
Subject: [PATCH 4/6] refactor: introduce revised notation, plus knock-ons

---
 src/Algebra/Construct/DirectProduct.agda      | 38 ++++-----
 src/Algebra/Construct/LexProduct.agda         |  8 +-
 .../Module/Construct/DirectProduct.agda       |  8 +-
 src/Data/Product/Effectful/Examples.agda      | 18 +++--
 .../Function/NonDependent/Propositional.agda  |  4 +-
 .../Relation/Binary/Lex/NonStrict.agda        | 12 +--
 .../Product/Relation/Binary/Lex/Strict.agda   | 14 ++--
 .../Binary/Pointwise/NonDependent.agda        | 79 +++++++++++--------
 .../AVL/Map/Membership/Propositional.agda     |  2 +-
 .../Membership/Propositional/Properties.agda  |  5 +-
 .../Relation/Binary/Pointwise/Properties.agda | 16 ++--
 .../Binary/Morphism/Construct/Product.agda    |  4 +-
 12 files changed, 113 insertions(+), 95 deletions(-)

diff --git a/src/Algebra/Construct/DirectProduct.agda b/src/Algebra/Construct/DirectProduct.agda
index 3c0ec699ee..8c36c1eb48 100644
--- a/src/Algebra/Construct/DirectProduct.agda
+++ b/src/Algebra/Construct/DirectProduct.agda
@@ -16,7 +16,7 @@
 module Algebra.Construct.DirectProduct where
 
 open import Algebra
-open import Data.Product.Base using (_×_; zip; _,_; map; _<*>_; uncurry)
+open import Data.Product.Base as Product using (zip; _,_; map; _<*>_; uncurry)
 open import Data.Product.Relation.Binary.Pointwise.NonDependent
 open import Level using (Level; _⊔_)
 
@@ -29,23 +29,23 @@ private
 
 rawMagma : RawMagma a ℓ₁ → RawMagma b ℓ₂ → RawMagma (a ⊔ b) (ℓ₁ ⊔ ℓ₂)
 rawMagma M N = record
-  { Carrier = M.Carrier × N.Carrier
-  ; _≈_     = Pointwise M._≈_ N._≈_
+  { Carrier = M.Carrier Product.× N.Carrier
+  ; _≈_     = M._≈_ × N._≈_
   ; _∙_     = zip M._∙_ N._∙_
   } where module M = RawMagma M; module N = RawMagma N
 
 rawMonoid : RawMonoid a ℓ₁ → RawMonoid b ℓ₂ → RawMonoid (a ⊔ b) (ℓ₁ ⊔ ℓ₂)
 rawMonoid M N = record
-  { Carrier = M.Carrier × N.Carrier
-  ; _≈_     = Pointwise M._≈_ N._≈_
+  { Carrier = M.Carrier Product.× N.Carrier
+  ; _≈_     = M._≈_ × N._≈_
   ; _∙_     = zip M._∙_ N._∙_
   ; ε       = M.ε , N.ε
   } where module M = RawMonoid M; module N = RawMonoid N
 
 rawGroup : RawGroup a ℓ₁ → RawGroup b ℓ₂ → RawGroup (a ⊔ b) (ℓ₁ ⊔ ℓ₂)
 rawGroup G H = record
-  { Carrier = G.Carrier × H.Carrier
-  ; _≈_     = Pointwise G._≈_ H._≈_
+  { Carrier = G.Carrier Product.× H.Carrier
+  ; _≈_     = G._≈_ × H._≈_
   ; _∙_     = zip G._∙_ H._∙_
   ; ε       = G.ε , H.ε
   ; _⁻¹     = map G._⁻¹ H._⁻¹
@@ -53,8 +53,8 @@ rawGroup G H = record
 
 rawSemiring : RawSemiring a ℓ₁ → RawSemiring b ℓ₂ → RawSemiring (a ⊔ b) (ℓ₁ ⊔ ℓ₂)
 rawSemiring R S = record
-  { Carrier = R.Carrier × S.Carrier
-  ; _≈_     = Pointwise R._≈_ S._≈_
+  { Carrier = R.Carrier Product.× S.Carrier
+  ; _≈_     = R._≈_ × S._≈_
   ; _+_     = zip R._+_ S._+_
   ; _*_     = zip R._*_ S._*_
   ; 0#      = R.0# , S.0#
@@ -63,8 +63,8 @@ rawSemiring R S = record
 
 rawRingWithoutOne : RawRingWithoutOne a ℓ₁ → RawRingWithoutOne b ℓ₂ → RawRingWithoutOne (a ⊔ b) (ℓ₁ ⊔ ℓ₂)
 rawRingWithoutOne R S = record
-  { Carrier = R.Carrier × S.Carrier
-  ; _≈_     = Pointwise R._≈_ S._≈_
+  { Carrier = R.Carrier Product.× S.Carrier
+  ; _≈_     = R._≈_ × S._≈_
   ; _+_     = zip R._+_ S._+_
   ; _*_     = zip R._*_ S._*_
   ; -_      = map R.-_ S.-_
@@ -73,8 +73,8 @@ rawRingWithoutOne R S = record
 
 rawRing : RawRing a ℓ₁ → RawRing b ℓ₂ → RawRing (a ⊔ b) (ℓ₁ ⊔ ℓ₂)
 rawRing R S = record
-  { Carrier = R.Carrier × S.Carrier
-  ; _≈_     = Pointwise R._≈_ S._≈_
+  { Carrier = R.Carrier Product.× S.Carrier
+  ; _≈_     = R._≈_ × S._≈_
   ; _+_     = zip R._+_ S._+_
   ; _*_     = zip R._*_ S._*_
   ; -_      = map R.-_ S.-_
@@ -84,8 +84,8 @@ rawRing R S = record
 
 rawQuasigroup : RawQuasigroup a ℓ₁ → RawQuasigroup b ℓ₂ → RawQuasigroup (a ⊔ b) (ℓ₁ ⊔ ℓ₂)
 rawQuasigroup M N = record
-  { Carrier = M.Carrier × N.Carrier
-  ; _≈_     = Pointwise M._≈_ N._≈_
+  { Carrier = M.Carrier Product.× N.Carrier
+  ; _≈_     = M._≈_ × N._≈_
   ; _∙_     = zip M._∙_ N._∙_
   ; _\\_    = zip M._\\_ N._\\_
   ; _//_    = zip M._//_ N._//_
@@ -93,8 +93,8 @@ rawQuasigroup M N = record
 
 rawLoop : RawLoop a ℓ₁ → RawLoop b ℓ₂ → RawLoop (a ⊔ b) (ℓ₁ ⊔ ℓ₂)
 rawLoop M N = record
-  { Carrier = M.Carrier × N.Carrier
-  ; _≈_     = Pointwise M._≈_ N._≈_
+  { Carrier = M.Carrier Product.× N.Carrier
+  ; _≈_     = M._≈_ × N._≈_
   ; _∙_     = zip M._∙_ N._∙_
   ; _\\_    = zip M._\\_ N._\\_
   ; _//_    = zip M._//_ N._//_
@@ -106,8 +106,8 @@ rawLoop M N = record
 
 magma : Magma a ℓ₁ → Magma b ℓ₂ → Magma (a ⊔ b) (ℓ₁ ⊔ ℓ₂)
 magma M N = record
-  { Carrier = M.Carrier × N.Carrier
-  ; _≈_     = Pointwise M._≈_ N._≈_
+  { Carrier = M.Carrier Product.× N.Carrier
+  ; _≈_     = M._≈_ × N._≈_
   ; _∙_     = zip M._∙_ N._∙_
   ; isMagma = record
     { isEquivalence = ×-isEquivalence M.isEquivalence N.isEquivalence
diff --git a/src/Algebra/Construct/LexProduct.agda b/src/Algebra/Construct/LexProduct.agda
index 3fbcf86c80..23ad3c53d0 100644
--- a/src/Algebra/Construct/LexProduct.agda
+++ b/src/Algebra/Construct/LexProduct.agda
@@ -9,8 +9,8 @@
 open import Algebra.Bundles using (Magma)
 open import Algebra.Definitions
 open import Data.Bool.Base using (true; false)
-open import Data.Product.Base using (_×_; _,_)
-open import Data.Product.Relation.Binary.Pointwise.NonDependent using (Pointwise)
+open import Data.Product.Base as Product using (_,_)
+open import Data.Product.Relation.Binary.Pointwise.NonDependent using (_×_)
 open import Data.Sum.Base using (inj₁; inj₂; map)
 open import Function.Base using (_∘_)
 open import Relation.Binary.Core using (Rel)
@@ -43,8 +43,8 @@ import Algebra.Construct.LexProduct.Inner M N _≟₁_ as InnerLex
 
 private
   infix 4 _≋_
-  _≋_ : Rel (A × B) _
-  _≋_ = Pointwise _≈₁_ _≈₂_
+  _≋_ : Rel (A Product.× B) _
+  _≋_ = _≈₁_ × _≈₂_
 
   variable
     a b : A
diff --git a/src/Algebra/Module/Construct/DirectProduct.agda b/src/Algebra/Module/Construct/DirectProduct.agda
index c369983904..f262395560 100644
--- a/src/Algebra/Module/Construct/DirectProduct.agda
+++ b/src/Algebra/Module/Construct/DirectProduct.agda
@@ -16,7 +16,7 @@ open import Algebra.Construct.DirectProduct using (commutativeMonoid)
 open import Algebra.Module.Bundles
 open import Data.Product.Base using (map; zip; _,_; proj₁; proj₂)
 open import Data.Product.Relation.Binary.Pointwise.NonDependent
-  using (Pointwise)
+  using (_×_)
 open import Level using (Level; _⊔_)
 
 private
@@ -31,7 +31,7 @@ rawLeftSemimodule : {R : Set r} →
                     RawLeftSemimodule R m′ ℓm′ →
                     RawLeftSemimodule R (m ⊔ m′) (ℓm ⊔ ℓm′)
 rawLeftSemimodule M N = record
-  { _≈ᴹ_ = Pointwise M._≈ᴹ_ N._≈ᴹ_
+  { _≈ᴹ_ = M._≈ᴹ_ × N._≈ᴹ_
   ; _+ᴹ_ = zip M._+ᴹ_ N._+ᴹ_
   ; _*ₗ_ = λ r → map (r M.*ₗ_) (r N.*ₗ_)
   ; 0ᴹ = M.0ᴹ , N.0ᴹ
@@ -52,7 +52,7 @@ rawRightSemimodule : {R : Set r} →
                     RawRightSemimodule R m′ ℓm′ →
                     RawRightSemimodule R (m ⊔ m′) (ℓm ⊔ ℓm′)
 rawRightSemimodule M N = record
-  { _≈ᴹ_ = Pointwise M._≈ᴹ_ N._≈ᴹ_
+  { _≈ᴹ_ = M._≈ᴹ_ × N._≈ᴹ_
   ; _+ᴹ_ = zip M._+ᴹ_ N._+ᴹ_
   ; _*ᵣ_ = λ mn r → map (M._*ᵣ r) (N._*ᵣ r) mn
   ; 0ᴹ = M.0ᴹ , N.0ᴹ
@@ -72,7 +72,7 @@ rawBisemimodule : {R : Set r} {S : Set s} →
                     RawBisemimodule R S m′ ℓm′ →
                     RawBisemimodule R S (m ⊔ m′) (ℓm ⊔ ℓm′)
 rawBisemimodule M N = record
-  { _≈ᴹ_ = Pointwise M._≈ᴹ_ N._≈ᴹ_
+  { _≈ᴹ_ = M._≈ᴹ_ × N._≈ᴹ_
   ; _+ᴹ_ = zip M._+ᴹ_ N._+ᴹ_
   ; _*ₗ_ = λ r → map (r M.*ₗ_) (r N.*ₗ_)
   ; _*ᵣ_ = λ mn r → map (M._*ᵣ r) (N._*ᵣ r) mn
diff --git a/src/Data/Product/Effectful/Examples.agda b/src/Data/Product/Effectful/Examples.agda
index f9f25fa389..11967b1315 100644
--- a/src/Data/Product/Effectful/Examples.agda
+++ b/src/Data/Product/Effectful/Examples.agda
@@ -14,7 +14,7 @@ module Data.Product.Effectful.Examples
 open import Level using (Lift; lift; _⊔_)
 open import Effect.Functor using (RawFunctor)
 open import Effect.Monad using (RawMonad)
-open import Data.Product.Base using (_×_; _,_)
+open import Data.Product.Base as Product using (_,_)
 open import Data.Product.Relation.Binary.Pointwise.NonDependent
 open import Function.Base using (id)
 open import Relation.Binary.Core using (Rel)
@@ -30,16 +30,18 @@ private
 
   module A = Monoid A
 
+  A×B = A.Carrier Product.× Lift a B
+
   open import Data.Product.Effectful.Left A.rawMonoid b
 
-  _≈_ : Rel (A.Carrier × Lift a B) (e ⊔ a ⊔ b)
-  _≈_ = Pointwise A._≈_ _≡_
+  _≈_ : Rel A×B (e ⊔ a ⊔ b)
+  _≈_ = A._≈_ × _≡_
 
   open RawFunctor functor
 
   -- This type to the right of × needs to be a "lifted" version of
   -- (B : Set b) that lives in the universe (Set (a ⊔ b)).
-  fmapIdₗ : (x : A.Carrier × Lift a B) → (id <$> x) ≈ x
+  fmapIdₗ : (x : A×B) → (id <$> x) ≈ x
   fmapIdₗ x = A.refl , refl
 
   open RawMonad monad
@@ -47,15 +49,15 @@ private
   -- Now, let's show that "pure" is a unit for >>=. We use Lift in
   -- exactly the same way as above. The data (x : B) then needs to be
   -- "lifted" to this new type (Lift B).
-  pureUnitL : ∀ {x : B} {f : Lift a B → A.Carrier × Lift a B} →
+  pureUnitL : ∀ {x : B} {f : Lift a B → A×B} →
                 (pure (lift x) >>= f) ≈ f (lift x)
   pureUnitL = A.identityˡ _ , refl
 
-  pureUnitR : {x : A.Carrier × Lift a B} → (x >>= pure) ≈ x
+  pureUnitR : {x : A×B} → (x >>= pure) ≈ x
   pureUnitR = A.identityʳ _ , refl
 
   -- And another (limited version of a) monad law...
-  bindCompose : ∀ {f g : Lift a B → A.Carrier × Lift a B} →
-                {x : A.Carrier × Lift a B} →
+  bindCompose : ∀ {f g : Lift a B → A×B} →
+                {x : A×B} →
                 ((x >>= f) >>= g) ≈ (x >>= (λ y → (f y >>= g)))
   bindCompose = A.assoc _ _ _ , refl
diff --git a/src/Data/Product/Function/NonDependent/Propositional.agda b/src/Data/Product/Function/NonDependent/Propositional.agda
index 1552564ed0..d92615ad09 100644
--- a/src/Data/Product/Function/NonDependent/Propositional.agda
+++ b/src/Data/Product/Function/NonDependent/Propositional.agda
@@ -12,7 +12,7 @@ module Data.Product.Function.NonDependent.Propositional where
 open import Data.Product.Base using (_×_; map)
 open import Data.Product.Function.NonDependent.Setoid
 open import Data.Product.Relation.Binary.Pointwise.NonDependent
-  using (_×ₛ_; Pointwise-≡↔≡)
+  using (_×ₛ_; ×-≡↔≡-×)
 open import Function.Base using (id)
 open import Function.Bundles
   using (Inverse; _⟶_; _⇔_; _↣_; _↠_; _⤖_; _↩_; _↪_; _↔_)
@@ -43,7 +43,7 @@ private
                    R (setoid A) (setoid C) → R (setoid B) (setoid D) →
                    R (setoid (A × B)) (setoid (C × D))
   liftViaInverse trans inv⇒R lift RAC RBD =
-    Inv.transportVia trans inv⇒R (Inv.sym Pointwise-≡↔≡) (lift RAC RBD) Pointwise-≡↔≡
+    Inv.transportVia trans inv⇒R (Inv.sym ×-≡↔≡-×) (lift RAC RBD) ×-≡↔≡-×
 
 ------------------------------------------------------------------------
 -- Combinators for various function types
diff --git a/src/Data/Product/Relation/Binary/Lex/NonStrict.agda b/src/Data/Product/Relation/Binary/Lex/NonStrict.agda
index 365e28468a..6c9cb4f547 100644
--- a/src/Data/Product/Relation/Binary/Lex/NonStrict.agda
+++ b/src/Data/Product/Relation/Binary/Lex/NonStrict.agda
@@ -11,9 +11,9 @@
 
 module Data.Product.Relation.Binary.Lex.NonStrict where
 
-open import Data.Product.Base using (_×_; _,_; proj₁; proj₂)
+open import Data.Product.Base as Product using (_,_; proj₁; proj₂)
 open import Data.Product.Relation.Binary.Pointwise.NonDependent as Pointwise
-  using (Pointwise)
+  using (_×_; _×?_)
 import Data.Product.Relation.Binary.Lex.Strict as Strict
 open import Data.Sum.Base using (inj₁; inj₂)
 open import Level using (Level)
@@ -39,7 +39,7 @@ private
 -- Definition
 
 ×-Lex : (_≈₁_ : Rel A ℓ₁) (_≤₁_ : Rel A ℓ₂) (_≤₂_ : Rel B ℓ₃) →
-        Rel (A × B) _
+        Rel (A Product.× B) _
 ×-Lex _≈₁_ _≤₁_ _≤₂_ = Strict.×-Lex _≈₁_ (Conv._<_ _≈₁_ _≤₁_) _≤₂_
 
 ------------------------------------------------------------------------
@@ -48,7 +48,7 @@ private
 ×-reflexive : (_≈₁_ : Rel A ℓ₁) (_≤₁_ : Rel A ℓ₂)
               {_≈₂_ : Rel B ℓ₃} (_≤₂_ : Rel B ℓ₄) →
               _≈₂_ ⇒ _≤₂_ →
-              (Pointwise _≈₁_ _≈₂_) ⇒ (×-Lex _≈₁_ _≤₁_ _≤₂_)
+              (_≈₁_ × _≈₂_) ⇒ (×-Lex _≈₁_ _≤₁_ _≤₂_)
 ×-reflexive _≈₁_ _≤₁_ _≤₂_ refl₂ =
   Strict.×-reflexive _≈₁_ (Conv._<_ _≈₁_ _≤₁_) _≤₂_ refl₂
 
@@ -94,7 +94,7 @@ module _ {_≈₁_ : Rel A ℓ₁} {_≤₁_ : Rel A ℓ₂}
 
   private
     _≤ₗₑₓ_ = ×-Lex _≈₁_ _≤₁_ _≤₂_
-    _≋_    = Pointwise _≈₁_ _≈₂_
+    _≋_    = _≈₁_ × _≈₂_
 
   ×-antisymmetric : IsPartialOrder _≈₁_ _≤₁_ → Antisymmetric _≈₂_ _≤₂_ →
                    Antisymmetric _≋_ _≤ₗₑₓ_
@@ -157,7 +157,7 @@ module _ {_≈₁_ : Rel A ℓ₁} {_≤₁_ : Rel A ℓ₂}
     { isTotalOrder = ×-isTotalOrder (_≟_ to₁)
                                     (isTotalOrder to₁)
                                     (isTotalOrder to₂)
-    ; _≟_          = Pointwise.pointwise? (_≟_ to₁) (_≟_ to₂)
+    ; _≟_          =(_≟_ to₁) ×? (_≟_ to₂)
     ; _≤?_         = ×-decidable (_≟_ to₁) (_≤?_ to₁) (_≤?_ to₂)
     }
     where open IsDecTotalOrder
diff --git a/src/Data/Product/Relation/Binary/Lex/Strict.agda b/src/Data/Product/Relation/Binary/Lex/Strict.agda
index 7ccc8357f4..2a6f78ca22 100644
--- a/src/Data/Product/Relation/Binary/Lex/Strict.agda
+++ b/src/Data/Product/Relation/Binary/Lex/Strict.agda
@@ -11,9 +11,9 @@
 
 module Data.Product.Relation.Binary.Lex.Strict where
 
-open import Data.Product.Base
+open import Data.Product.Base as Product using (_,_; proj₁; proj₂; _-×-_)
 open import Data.Product.Relation.Binary.Pointwise.NonDependent as Pointwise
-  using (Pointwise)
+  using (_×_)
 open import Data.Sum.Base using (inj₁; inj₂; _-⊎-_; [_,_])
 open import Function.Base using (flip; _on_; _$_; _∘_)
 open import Induction.WellFounded using (Acc; acc; WfRec; WellFounded; Acc-resp-flip-≈)
@@ -42,7 +42,7 @@ private
 -- A lexicographic ordering over products
 
 ×-Lex : (_≈₁_ : Rel A ℓ₁) (_<₁_ : Rel A ℓ₂) (_≤₂_ : Rel B ℓ₃) →
-        Rel (A × B) _
+        Rel (A Product.× B) _
 ×-Lex _≈₁_ _<₁_ _≤₂_ =
   (_<₁_ on proj₁) -⊎- (_≈₁_ on proj₁) -×- (_≤₂_ on proj₂)
 
@@ -52,7 +52,7 @@ private
 
 ×-reflexive : (_≈₁_ : Rel A ℓ₁) (_∼₁_ : Rel A ℓ₂)
               {_≈₂_ : Rel B ℓ₃} (_≤₂_ : Rel B ℓ₄) →
-              _≈₂_ ⇒ _≤₂_ → (Pointwise _≈₁_ _≈₂_) ⇒ (×-Lex _≈₁_ _∼₁_ _≤₂_)
+              _≈₂_ ⇒ _≤₂_ → (_≈₁_ × _≈₂_) ⇒ (×-Lex _≈₁_ _∼₁_ _≤₂_)
 ×-reflexive _ _ _ refl₂ = λ x≈y →
   inj₂ (proj₁ x≈y , refl₂ (proj₂ x≈y))
 
@@ -120,11 +120,11 @@ module _ {_≈₁_ : Rel A ℓ₁} {_<₁_ : Rel A ℓ₂}
          {_≈₂_ : Rel B ℓ₃} {_<₂_ : Rel B ℓ₄} where
 
   private
-    _≋_    = Pointwise _≈₁_ _≈₂_
+    _≋_    = _≈₁_ × _≈₂_
     _<ₗₑₓ_ = ×-Lex _≈₁_ _<₁_ _<₂_
 
   ×-irreflexive : Irreflexive _≈₁_ _<₁_ → Irreflexive _≈₂_ _<₂_ →
-                  Irreflexive (Pointwise _≈₁_ _≈₂_) _<ₗₑₓ_
+                  Irreflexive (_≈₁_ × _≈₂_) _<ₗₑₓ_
   ×-irreflexive ir₁ ir₂ x≈y (inj₁ x₁<y₁) = ir₁ (proj₁ x≈y) x₁<y₁
   ×-irreflexive ir₁ ir₂ x≈y (inj₂ x≈<y)  = ir₂ (proj₂ x≈y) (proj₂ x≈<y)
 
@@ -230,7 +230,7 @@ module _ {_≈₁_ : Rel A ℓ₁} {_<₁_ : Rel A ℓ₂}
          {_≈₂_ : Rel B ℓ₃} {_<₂_ : Rel B ℓ₄} where
 
   private
-    _≋_    = Pointwise _≈₁_ _≈₂_
+    _≋_    = _≈₁_ × _≈₂_
     _<ₗₑₓ_ = ×-Lex _≈₁_ _<₁_ _<₂_
 
   ×-isPreorder : IsPreorder _≈₁_ _<₁_ →
diff --git a/src/Data/Product/Relation/Binary/Pointwise/NonDependent.agda b/src/Data/Product/Relation/Binary/Pointwise/NonDependent.agda
index 7a1b8c80eb..7bccbc394c 100644
--- a/src/Data/Product/Relation/Binary/Pointwise/NonDependent.agda
+++ b/src/Data/Product/Relation/Binary/Pointwise/NonDependent.agda
@@ -8,12 +8,11 @@
 
 module Data.Product.Relation.Binary.Pointwise.NonDependent where
 
-open import Data.Product.Base as Product
+open import Data.Product.Base as Product using (_,_; proj₁; proj₂)
 open import Data.Sum.Base using (inj₁; inj₂)
 open import Level using (Level; _⊔_; 0ℓ)
 open import Function.Base using (id)
 open import Function.Bundles using (Inverse)
-open import Relation.Nullary.Decidable.Core using (_×?_)
 open import Relation.Binary.Core using (REL; Rel; _⇒_)
 open import Relation.Binary.Bundles
   using (Setoid; DecSetoid; Preorder; Poset; StrictPartialOrder)
@@ -21,6 +20,7 @@ open import Relation.Binary.Definitions
 open import Relation.Binary.Structures
 open import Relation.Binary.PropositionalEquality.Core as ≡ using (_≡_)
 import Relation.Binary.PropositionalEquality.Properties as ≡
+import Relation.Nullary.Decidable.Core as Dec using (_×?_)
 
 private
   variable
@@ -31,55 +31,57 @@ private
 ------------------------------------------------------------------------
 -- Definition
 
-Pointwise : REL A B ℓ₁ → REL C D ℓ₂ → REL (A × C) (B × D) (ℓ₁ ⊔ ℓ₂)
-Pointwise R S (a , c) (b , d) = (R a b) × (S c d)
+infixr 2 _×_
+
+_×_ : REL A B ℓ₁ → REL C D ℓ₂ → REL (A Product.× C) (B Product.× D) (ℓ₁ ⊔ ℓ₂)
+(R × S) (a , c) (b , d) = (R a b) Product.× (S c d)
 
 ------------------------------------------------------------------------
 -- Pointwise preserves many relational properties
 
-×-reflexive : ≈₁ ⇒ R → ≈₂ ⇒ S → Pointwise ≈₁ ≈₂ ⇒ Pointwise R S
+×-reflexive : ≈₁ ⇒ R → ≈₂ ⇒ S → (≈₁ × ≈₂) ⇒ (R × S)
 ×-reflexive refl₁ refl₂ = Product.map refl₁ refl₂
 
-×-refl : Reflexive R → Reflexive S → Reflexive (Pointwise R S)
+×-refl : Reflexive R → Reflexive S → Reflexive (R × S)
 ×-refl refl₁ refl₂ = refl₁ , refl₂
 
 ×-irreflexive₁ : Irreflexive ≈₁ R →
-                 Irreflexive (Pointwise ≈₁ ≈₂) (Pointwise R S)
+                 Irreflexive (≈₁ × ≈₂) (R × S)
 ×-irreflexive₁ ir x≈y x<y = ir (proj₁ x≈y) (proj₁ x<y)
 
 ×-irreflexive₂ : Irreflexive ≈₂ S →
-                 Irreflexive (Pointwise ≈₁ ≈₂) (Pointwise R S)
+                 Irreflexive (≈₁ × ≈₂) (R × S)
 ×-irreflexive₂ ir x≈y x<y = ir (proj₂ x≈y) (proj₂ x<y)
 
-×-symmetric : Symmetric R → Symmetric S → Symmetric (Pointwise R S)
+×-symmetric : Symmetric R → Symmetric S → Symmetric (R × S)
 ×-symmetric sym₁ sym₂ = Product.map sym₁ sym₂
 
-×-transitive : Transitive R → Transitive S → Transitive (Pointwise R S)
+×-transitive : Transitive R → Transitive S → Transitive (R × S)
 ×-transitive trans₁ trans₂ = Product.zip trans₁ trans₂
 
 ×-antisymmetric : Antisymmetric ≈₁ R → Antisymmetric ≈₂ S →
-                  Antisymmetric (Pointwise ≈₁ ≈₂) (Pointwise R S)
+                  Antisymmetric (≈₁ × ≈₂) (R × S)
 ×-antisymmetric antisym₁ antisym₂ = Product.zip antisym₁ antisym₂
 
-×-asymmetric₁ : Asymmetric R → Asymmetric (Pointwise R S)
+×-asymmetric₁ : Asymmetric R → Asymmetric (R × S)
 ×-asymmetric₁ asym₁ x<y y<x = asym₁ (proj₁ x<y) (proj₁ y<x)
 
-×-asymmetric₂ : Asymmetric S → Asymmetric (Pointwise R S)
+×-asymmetric₂ : Asymmetric S → Asymmetric (R × S)
 ×-asymmetric₂ asym₂ x<y y<x = asym₂ (proj₂ x<y) (proj₂ y<x)
 
 ×-respectsʳ : R Respectsʳ ≈₁ → S Respectsʳ ≈₂ →
-             (Pointwise R S) Respectsʳ (Pointwise ≈₁ ≈₂)
+             (R × S) Respectsʳ (≈₁ × ≈₂)
 ×-respectsʳ resp₁ resp₂ = Product.zip resp₁ resp₂
 
 ×-respectsˡ : R Respectsˡ ≈₁ → S Respectsˡ ≈₂ →
-             (Pointwise R S) Respectsˡ (Pointwise ≈₁ ≈₂)
+             (R × S) Respectsˡ (≈₁ × ≈₂)
 ×-respectsˡ resp₁ resp₂ = Product.zip resp₁ resp₂
 
 ×-respects₂ : R Respects₂ ≈₁ → S Respects₂ ≈₂ →
-              (Pointwise R S) Respects₂ (Pointwise ≈₁ ≈₂)
+              (R × S) Respects₂ (≈₁ × ≈₂)
 ×-respects₂ = Product.zip ×-respectsʳ ×-respectsˡ
 
-×-total : Symmetric R → Total R → Total S → Total (Pointwise R S)
+×-total : Symmetric R → Total R → Total S → Total (R × S)
 ×-total sym₁ total₁ total₂ (x₁ , x₂) (y₁ , y₂)
   with total₁ x₁ y₁ | total₂ x₂ y₂
 ... | inj₁ x₁∼y₁ | inj₁ x₂∼y₂ = inj₁ (     x₁∼y₁ , x₂∼y₂)
@@ -87,8 +89,9 @@ Pointwise R S (a , c) (b , d) = (R a b) × (S c d)
 ... | inj₂ y₁∼x₁ | inj₂ y₂∼x₂ = inj₂ (     y₁∼x₁ , y₂∼x₂)
 ... | inj₂ y₁∼x₁ | inj₁ x₂∼y₂ = inj₁ (sym₁ y₁∼x₁ , x₂∼y₂)
 
-pointwise? : Decidable R → Decidable S → Decidable (Pointwise R S)
-pointwise? _R?_ _S?_ (x₁ , x₂) (y₁ , y₂) = (x₁ R? y₁) ×? (x₂ S? y₂)
+infixr 2 _×?_
+_×?_ : Decidable R → Decidable S → Decidable (R × S)
+_×?_ _R?_ _S?_ (x₁ , x₂) (y₁ , y₂) = (x₁ R? y₁) Dec.×? (x₂ S? y₂)
 
 ------------------------------------------------------------------------
 -- Structures can also be combined.
@@ -96,7 +99,7 @@ pointwise? _R?_ _S?_ (x₁ , x₂) (y₁ , y₂) = (x₁ R? y₁) ×? (x₂ S? y
 -- Some collections of properties which are preserved by ×-Rel.
 
 ×-isEquivalence : IsEquivalence R → IsEquivalence S →
-                  IsEquivalence (Pointwise R S)
+                  IsEquivalence (R × S)
 ×-isEquivalence {R = R} {S = S} eq₁ eq₂ = record
   { refl  = ×-refl {R = R} {S = S} (refl eq₁) (refl eq₂)
   ; sym   = ×-symmetric {R = R} {S = S} (sym eq₁) (sym eq₂)
@@ -104,15 +107,15 @@ pointwise? _R?_ _S?_ (x₁ , x₂) (y₁ , y₂) = (x₁ R? y₁) ×? (x₂ S? y
   } where open IsEquivalence
 
 ×-isDecEquivalence : IsDecEquivalence R → IsDecEquivalence S →
-                     IsDecEquivalence (Pointwise R S)
+                     IsDecEquivalence (R × S)
 ×-isDecEquivalence eq₁ eq₂ = record
   { isEquivalence = ×-isEquivalence
                       (isEquivalence eq₁) (isEquivalence eq₂)
-  ; _≟_           = pointwise? (_≟_ eq₁) (_≟_ eq₂)
+  ; _≟_           = (_≟_ eq₁) ×? (_≟_ eq₂)
   } where open IsDecEquivalence
 
 ×-isPreorder : IsPreorder ≈₁ R → IsPreorder ≈₂ S →
-               IsPreorder (Pointwise ≈₁ ≈₂) (Pointwise R S)
+               IsPreorder (≈₁ × ≈₂) (R × S)
 ×-isPreorder {R = R} {S = S} pre₁ pre₂ = record
   { isEquivalence = ×-isEquivalence
                       (isEquivalence pre₁) (isEquivalence pre₂)
@@ -123,7 +126,7 @@ pointwise? _R?_ _S?_ (x₁ , x₂) (y₁ , y₂) = (x₁ R? y₁) ×? (x₂ S? y
   } where open IsPreorder
 
 ×-isPartialOrder : IsPartialOrder ≈₁ R → IsPartialOrder ≈₂ S →
-                   IsPartialOrder (Pointwise ≈₁ ≈₂) (Pointwise R S)
+                   IsPartialOrder (≈₁ × ≈₂) (R × S)
 ×-isPartialOrder {R = R} {S = S} po₁ po₂ = record
   { isPreorder = ×-isPreorder (isPreorder po₁) (isPreorder po₂)
   ; antisym    = ×-antisymmetric {R = R} {S = S}
@@ -132,7 +135,7 @@ pointwise? _R?_ _S?_ (x₁ , x₂) (y₁ , y₂) = (x₁ R? y₁) ×? (x₂ S? y
 
 ×-isStrictPartialOrder : IsStrictPartialOrder ≈₁ R →
                          IsStrictPartialOrder ≈₂ S →
-                         IsStrictPartialOrder (Pointwise ≈₁ ≈₂) (Pointwise R S)
+                         IsStrictPartialOrder (≈₁ × ≈₂) (R × S)
 ×-isStrictPartialOrder {R = R} {≈₂ = ≈₂} {S = S} spo₁ spo₂ = record
   { isEquivalence = ×-isEquivalence
                       (isEquivalence spo₁) (isEquivalence spo₂)
@@ -190,14 +193,14 @@ _×ₛ_ = ×-setoid
 -- The propositional equality setoid over products can be
 -- decomposed using ×-Rel
 
-≡×≡⇒≡ : Pointwise _≡_ _≡_ ⇒ _≡_ {A = A × B}
+≡×≡⇒≡ : (_≡_ × _≡_) ⇒ _≡_ {A = A Product.× B}
 ≡×≡⇒≡ (≡.refl , ≡.refl) = ≡.refl
 
-≡⇒≡×≡ : _≡_ {A = A × B} ⇒ Pointwise _≡_ _≡_
-≡⇒≡×≡ ≡.refl = (≡.refl , ≡.refl)
+≡⇒≡×≡ : _≡_ {A = A Product.× B} ⇒ (_≡_ × _≡_)
+≡⇒≡×≡ ≡.refl = ≡.refl , ≡.refl
 
-Pointwise-≡↔≡ : Inverse (≡.setoid A ×ₛ ≡.setoid B) (≡.setoid (A × B))
-Pointwise-≡↔≡ = record
+×-≡↔≡-× : Inverse (≡.setoid A ×ₛ ≡.setoid B) (≡.setoid (A Product.× B))
+×-≡↔≡-× = record
   { to         = id
   ; from       = id
   ; to-cong    = ≡×≡⇒≡
@@ -214,8 +217,20 @@ Pointwise-≡↔≡ = record
 
 -- Version 2.4
 
-×-decidable = pointwise?
+Pointwise = _×_
+{-# WARNING_ON_USAGE Pointwise
+"Warning: Pointwise was deprecated in v2.4.
+Please use _×_ instead."
+#-}
+
+×-decidable = _×?_
 {-# WARNING_ON_USAGE ×-decidable
 "Warning: ×-decidable was deprecated in v2.4.
-Please use pointwise? instead."
+Please use _×?_ instead."
+#-}
+
+Pointwise-≡↔≡ = ×-≡↔≡-×
+{-# WARNING_ON_USAGE Pointwise-≡↔≡
+"Warning: Pointwise-≡↔≡ was deprecated in v2.4.
+Please use ×-≡↔≡-× instead."
 #-}
diff --git a/src/Data/Tree/AVL/Map/Membership/Propositional.agda b/src/Data/Tree/AVL/Map/Membership/Propositional.agda
index c63f7d5440..c1131e101b 100644
--- a/src/Data/Tree/AVL/Map/Membership/Propositional.agda
+++ b/src/Data/Tree/AVL/Map/Membership/Propositional.agda
@@ -16,7 +16,7 @@ module Data.Tree.AVL.Map.Membership.Propositional
 open import Data.Product.Base using (_×_)
 open import Data.Product.Relation.Binary.Pointwise.NonDependent
   using ()
-  renaming (Pointwise to _×ᴿ_)
+  renaming (_×_ to _×ᴿ_)
 open import Level using (Level)
 open import Relation.Binary.Core using (Rel)
 open import Relation.Binary.PropositionalEquality.Core using (_≡_)
diff --git a/src/Data/Tree/AVL/Map/Membership/Propositional/Properties.agda b/src/Data/Tree/AVL/Map/Membership/Propositional/Properties.agda
index 5e472cfe2b..f4fe7882c0 100644
--- a/src/Data/Tree/AVL/Map/Membership/Propositional/Properties.agda
+++ b/src/Data/Tree/AVL/Map/Membership/Propositional/Properties.agda
@@ -18,7 +18,7 @@ open import Data.Maybe.Base using (just; nothing; is-just)
 open import Data.Product.Base as Product
   using (_×_; ∃-syntax; _,_; proj₁; proj₂)
 open import Data.Product.Relation.Binary.Pointwise.NonDependent
-  renaming (Pointwise to _×ᴿ_)
+  renaming (_×_ to _×ᴿ_)
 open import Data.Sum.Base using (_⊎_; inj₁; inj₂)
 open import Function.Base using (_∘_; _∘′_)
 open import Level using (Level)
@@ -100,7 +100,8 @@ private
   ≈ₖᵥ-Resp : k ≈ k′ → kx ≈ₖᵥ (k′ , x) → kx ≈ₖᵥ (k , x)
   ≈ₖᵥ-Resp = (λ{ k′≈l (k≈l , x≡) → (trans k≈l (sym k′≈l) , x≡)})
 
-∈ₖᵥ-insert⁻ : (k , x) ∈ₖᵥ insert k′ x′ m → (k ≈ k′ × x ≡ x′) ⊎ (k ≉ k′ × (k , x) ∈ₖᵥ m)
+∈ₖᵥ-insert⁻ : (k , x) ∈ₖᵥ insert k′ x′ m →
+              (k ≈ k′ × x ≡ x′) ⊎ (k ≉ k′ × (k , x) ∈ₖᵥ m)
 ∈ₖᵥ-insert⁻ {m = tree t} (tree kx∈insert)
     with IAnyₚ.insert⁻ ≈ₖᵥ-Resp _ _ t (⊥⁺<[ _ ]<⊤⁺) kx∈insert
 ... | inj₁ p = inj₁ p
diff --git a/src/Data/Vec/Functional/Relation/Binary/Pointwise/Properties.agda b/src/Data/Vec/Functional/Relation/Binary/Pointwise/Properties.agda
index 1ba6aed44f..c9f7f94a34 100644
--- a/src/Data/Vec/Functional/Relation/Binary/Pointwise/Properties.agda
+++ b/src/Data/Vec/Functional/Relation/Binary/Pointwise/Properties.agda
@@ -11,11 +11,11 @@ module Data.Vec.Functional.Relation.Binary.Pointwise.Properties where
 open import Data.Fin.Base using (zero; suc; _↑ˡ_; _↑ʳ_; splitAt)
 open import Data.Fin.Properties using (all?; splitAt-↑ˡ; splitAt-↑ʳ)
 open import Data.Nat.Base using (ℕ; zero; suc)
-open import Data.Product.Base using (_×_; _,_; proj₁; proj₂)
+open import Data.Product.Base as Product using (_,_; proj₁; proj₂)
 open import Data.Product.Relation.Binary.Pointwise.NonDependent
-  using () renaming (Pointwise to ×-Pointwise)
+  using (_×_)
 open import Data.Sum.Base using (_⊎_; inj₁; inj₂; [_,_])
-open import Data.Vec.Functional as VF hiding (map)
+open import Data.Vec.Functional as Functional hiding (map)
 open import Data.Vec.Functional.Relation.Binary.Pointwise
 open import Function.Base using (const; _∘_)
 open import Level using (Level)
@@ -91,7 +91,7 @@ module _ {R : REL A B r} {S : REL A′ B′ s} {f : A → A′} {g : B → B′}
 
   map⁺ : (∀ {x y} → R x y → S (f x) (g y)) →
          ∀ {n} {xs : Vector A n} {ys : Vector B n} →
-         Pointwise R xs ys → Pointwise S (VF.map f xs) (VF.map g ys)
+         Pointwise R xs ys → Pointwise S (Functional.map f xs) (Functional.map g ys)
   map⁺ f rs i = f (rs i)
 
 ------------------------------------------------------------------------
@@ -134,7 +134,7 @@ module _ (R : REL A B r) where
 
   ++⁻ : ∀ {m n} xs ys {xs′ ys′} →
         Pointwise R (xs ++ xs′) (ys ++ ys′) →
-        Pointwise R {n = m} xs ys × Pointwise R {n = n} xs′ ys′
+        Pointwise R {n = m} xs ys Product.× Pointwise R {n = n} xs′ ys′
   ++⁻ _ _ rs = ++⁻ˡ _ _ rs , ++⁻ʳ _ _ rs
 
 ------------------------------------------------------------------------
@@ -172,11 +172,11 @@ module _ {R : REL A B r} {S : REL A′ B′ s} {T : REL A″ B″ t} where
 module _ {R : REL A B r} {S : REL A′ B′ s} {n xs ys xs′ ys′} where
 
   zip⁺ : Pointwise R xs ys → Pointwise S xs′ ys′ →
-         Pointwise (×-Pointwise R S) (zip xs xs′) (zip {n = n} ys ys′)
+         Pointwise (R × S) (zip xs xs′) (zip {n = n} ys ys′)
   zip⁺ rs ss i = rs i , ss i
 
-  zip⁻ : Pointwise (×-Pointwise R S) (zip xs xs′) (zip {n = n} ys ys′) →
-         Pointwise R xs ys × Pointwise S xs′ ys′
+  zip⁻ : Pointwise (R × S) (zip xs xs′) (zip {n = n} ys ys′) →
+         Pointwise R xs ys Product.× Pointwise S xs′ ys′
   zip⁻ rss = proj₁ ∘ rss , proj₂ ∘ rss
 
 ------------------------------------------------------------------------
diff --git a/src/Relation/Binary/Morphism/Construct/Product.agda b/src/Relation/Binary/Morphism/Construct/Product.agda
index b531fd9b72..b58449a95c 100644
--- a/src/Relation/Binary/Morphism/Construct/Product.agda
+++ b/src/Relation/Binary/Morphism/Construct/Product.agda
@@ -11,7 +11,7 @@ module Relation.Binary.Morphism.Construct.Product where
 
 import Data.Product.Base as Product using (<_,_>; proj₁; proj₂)
 open import Data.Product.Relation.Binary.Pointwise.NonDependent as Pointwise
-  using (Pointwise)
+  using (_×_)
 open import Level using (Level)
 open import Relation.Binary.Bundles.Raw using (RawSetoid)
 open import Relation.Binary.Core using (Rel)
@@ -32,7 +32,7 @@ module _ (_≈₁_ : Rel A ℓ₁) (_≈₂_ : Rel B ℓ₂) where
 
   private
 
-    _≈_ = Pointwise _≈₁_ _≈₂_
+    _≈_ = _≈₁_ × _≈₂_
 
   module Proj₁ where
 

From 8d87be05b496b7754eed36e7ca66d1e338d9d782 Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Thu, 5 Mar 2026 15:09:55 +0000
Subject: [PATCH 5/6] fix: `CHANGELOG`

---
 CHANGELOG.md | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index bd9572122f..84d4c3bb57 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -91,7 +91,9 @@ Deprecated names
 
 * In `Data.Product.Relation.Binary.Pointwise.NonDependent`:
   ```agda
-  ×-decidable  ↦  pointwise?
+  Pointwise      ↦  _×_
+  ×-decidable    ↦  _×?_
+  Pointwise-≡↔≡  ↦  ×-≡↔≡-×
   ```
 
 * In `Data.Rational.Properties`:

From 390b3c175ed84d714d44587d8ce786a730224b77 Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Tue, 17 Mar 2026 11:30:16 +0000
Subject: [PATCH 6/6] fix: `CHANGELOG`

---
 CHANGELOG.md | 15 +++++++--------
 1 file changed, 7 insertions(+), 8 deletions(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 12dc27930c..9f604f0d79 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -89,13 +89,6 @@ Deprecated names
   ¬∀⟶∃¬-          ↦   ¬∀⇒∃¬
   ```
 
-<<<<<<< decidable-pointwise
-* In `Data.Product.Relation.Binary.Pointwise.NonDependent`:
-  ```agda
-  Pointwise      ↦  _×_
-  ×-decidable    ↦  _×?_
-  Pointwise-≡↔≡  ↦  ×-≡↔≡-×
-=======
 * In `Data.List.Fresh.Membership.Setoid.Properties`:
   ```agda
   ≈-subst-∈   ↦   ∈-resp-≈
@@ -104,7 +97,13 @@ Deprecated names
 * In `Data.List.Fresh.Relation.Unary.Any`:
   ```agda
   witness   ↦   satisfiable
->>>>>>> master
+  ```
+
+* In `Data.Product.Relation.Binary.Pointwise.NonDependent`:
+  ```agda
+  Pointwise      ↦  _×_
+  ×-decidable    ↦  _×?_
+  Pointwise-≡↔≡  ↦  ×-≡↔≡-×
   ```
 
 * In `Data.Rational.Properties`: