fixes #906 (#2401)

Author: jamesmckinna

CHANGELOG.md

@@ -36,9 +36,14 @@ Other major improvements
 
 Minor improvements
 ------------------
-The size of the dependency graph for many modules has been
-reduced. This may lead to speed ups for first-time loading of some
-modules.
+
+* The size of the dependency graph for many modules has been
+  reduced. This may lead to speed ups for first-time loading of some
+  modules.
+
+* The definition of the `Pointwise` relational combinator in
+  `Data.Product.Relation.Binary.Pointwise.NonDependent.Pointwise`
+  has been generalised to take heterogeneous arguments in `REL`.
 
 Deprecated modules
 ------------------

src/Data/Product/Relation/Binary/Pointwise/NonDependent.agda

@@ -11,10 +11,10 @@ module Data.Product.Relation.Binary.Pointwise.NonDependent where
 open import Data.Product.Base as Product
 open import Data.Sum.Base using (inj₁; inj₂)
 open import Level using (Level; _⊔_; 0ℓ)
-open import Function.Base using (_on_; id)
+open import Function.Base using (id)
 open import Function.Bundles using (Inverse)
 open import Relation.Nullary.Decidable using (_×-dec_)
-open import Relation.Binary.Core using (Rel; _⇒_)
+open import Relation.Binary.Core using (REL; Rel; _⇒_)
 open import Relation.Binary.Bundles
   using (Setoid; DecSetoid; Preorder; Poset; StrictPartialOrder)
 open import Relation.Binary.Definitions
@@ -25,14 +25,14 @@ import Relation.Binary.PropositionalEquality.Properties as ≡
 private
   variable
     a b ℓ₁ ℓ₂ ℓ₃ ℓ₄ : Level
-    A B : Set a
+    A B C D : Set a
     R S ≈₁ ≈₂ : Rel A ℓ₁
 
 ------------------------------------------------------------------------
 -- Definition
 
-Pointwise : Rel A ℓ₁ → Rel B ℓ₂ → Rel (A × B) (ℓ₁ ⊔ ℓ₂)
-Pointwise R S = (R on proj₁) -×- (S on proj₂)
+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)
 
 ------------------------------------------------------------------------
 -- Pointwise preserves many relational properties

src/Data/Vec/Functional/Relation/Binary/Pointwise/Properties.agda

@@ -172,12 +172,10 @@ 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 (λ xx yy → R (proj₁ xx) (proj₁ yy) × S (proj₂ xx) (proj₂ yy))
-                   (zip xs xs′) (zip {n = n} ys ys′)
+         Pointwise (×-Pointwise R S) (zip xs xs′) (zip {n = n} ys ys′)
   zip⁺ rs ss i = rs i , ss i
 
-  zip⁻ : Pointwise (λ xx yy → R (proj₁ xx) (proj₁ yy) × S (proj₂ xx) (proj₂ yy))
-                   (zip xs xs′) (zip {n = n} ys ys′) →
+  zip⁻ : Pointwise (×-Pointwise R S) (zip xs xs′) (zip {n = n} ys ys′) →
          Pointwise R xs ys × Pointwise S xs′ ys′
   zip⁻ rss = proj₁ ∘ rss , proj₂ ∘ rss