From e580033eb4100551bef4ec7c5c7c3c2bb9ba5a2a Mon Sep 17 00:00:00 2001
From: Ruifeng Xie <ruifengx@outlook.com>
Date: Fri, 19 Dec 2025 13:58:56 +0800
Subject: [PATCH 1/4] Add irrelevant & antisym for Vec.Pointwise.Inductive

---
 src/Data/Vec/Relation/Binary/Pointwise/Inductive.agda | 11 ++++++++++-
 1 file changed, 10 insertions(+), 1 deletion(-)

diff --git a/src/Data/Vec/Relation/Binary/Pointwise/Inductive.agda b/src/Data/Vec/Relation/Binary/Pointwise/Inductive.agda
index 1d91f4e4a6..5dc7a4932c 100644
--- a/src/Data/Vec/Relation/Binary/Pointwise/Inductive.agda
+++ b/src/Data/Vec/Relation/Binary/Pointwise/Inductive.agda
@@ -23,7 +23,7 @@ open import Relation.Binary.Bundles using (Setoid; DecSetoid)
 open import Relation.Binary.Structures
   using (IsEquivalence; IsDecEquivalence)
 open import Relation.Binary.Definitions
-  using (Trans; Decidable; Reflexive; Sym)
+  using (Trans; Decidable; Reflexive; Sym; Antisym; Irrelevant)
 open import Relation.Binary.PropositionalEquality.Core as ≡ using (_≡_)
 open import Relation.Nullary.Decidable using (yes; no; _×?_; map′)
 open import Relation.Unary using (Pred)
@@ -88,6 +88,10 @@ module _ {_∼_ : REL A B ℓ} where
 ------------------------------------------------------------------------
 -- Relational properties
 
+irrelevant : ∀ {_∼_ : REL A B ℓ} {n m} → Irrelevant _∼_ → Irrelevant (Pointwise _∼_ {n} {m})
+irrelevant irr []      []      = ≡.refl
+irrelevant irr (p ∷ r) (q ∷ s) = ≡.cong₂ _∷_ (irr p q) (irrelevant irr r s)
+
 refl : ∀ {_∼_ : Rel A ℓ} {n} →
        Reflexive _∼_ → Reflexive (Pointwise _∼_ {n})
 refl ∼-refl {[]}      = []
@@ -105,6 +109,11 @@ trans trns []             []             = []
 trans trns (x∼y ∷ xs∼ys) (y∼z ∷ ys∼zs) =
   trns x∼y y∼z ∷ trans trns xs∼ys ys∼zs
 
+antisym : ∀ {P : REL A B ℓ₁} {Q : REL B A ℓ₂} {R : REL A B ℓ} {m n} →
+          Antisym P Q R → Antisym (Pointwise P {m}) (Pointwise Q {n}) (Pointwise R)
+antisym asym []            []            = []
+antisym asym (x∼y ∷ xs∼ys) (y∼x ∷ ys∼xs) = asym x∼y y∼x ∷ antisym asym xs∼ys ys∼xs
+
 decidable : ∀ {_∼_ : REL A B ℓ} →
             Decidable _∼_ → ∀ {m n} → Decidable (Pointwise _∼_ {m} {n})
 decidable dec []       []       = yes []

From 5134b1f4345fda22c5d94a89146db3bf4be1ccdb Mon Sep 17 00:00:00 2001
From: Ruifeng Xie <ruifengx@outlook.com>
Date: Fri, 19 Dec 2025 14:00:33 +0800
Subject: [PATCH 2/4] Fix: relax sym & trans to allow different levels

---
 src/Data/Vec/Relation/Binary/Pointwise/Inductive.agda | 10 +++++-----
 1 file changed, 5 insertions(+), 5 deletions(-)

diff --git a/src/Data/Vec/Relation/Binary/Pointwise/Inductive.agda b/src/Data/Vec/Relation/Binary/Pointwise/Inductive.agda
index 5dc7a4932c..50fe5fc824 100644
--- a/src/Data/Vec/Relation/Binary/Pointwise/Inductive.agda
+++ b/src/Data/Vec/Relation/Binary/Pointwise/Inductive.agda
@@ -94,18 +94,18 @@ irrelevant irr (p ∷ r) (q ∷ s) = ≡.cong₂ _∷_ (irr p q) (irrelevant irr
 
 refl : ∀ {_∼_ : Rel A ℓ} {n} →
        Reflexive _∼_ → Reflexive (Pointwise _∼_ {n})
-refl ∼-refl {[]}      = []
+refl ∼-refl {[]}     = []
 refl ∼-refl {x ∷ xs} = ∼-refl ∷ refl ∼-refl
 
-sym : ∀ {P : REL A B ℓ} {Q : REL B A ℓ} {m n} →
+sym : ∀ {P : REL A B ℓ₁} {Q : REL B A ℓ₂} {m n} →
       Sym P Q → Sym (Pointwise P) (Pointwise Q {m} {n})
-sym sm []             = []
+sym sm []            = []
 sym sm (x∼y ∷ xs∼ys) = sm x∼y ∷ sym sm xs∼ys
 
-trans : ∀ {P : REL A B ℓ} {Q : REL B C ℓ} {R : REL A C ℓ} {m n o} →
+trans : ∀ {P : REL A B ℓ₁} {Q : REL B C ℓ₂} {R : REL A C ℓ} {m n o} →
         Trans P Q R →
         Trans (Pointwise P {m}) (Pointwise Q {n} {o}) (Pointwise R)
-trans trns []             []             = []
+trans trns []            []            = []
 trans trns (x∼y ∷ xs∼ys) (y∼z ∷ ys∼zs) =
   trns x∼y y∼z ∷ trans trns xs∼ys ys∼zs
 

From 77a6cbdd3c5f7b2b8eea8137ddcc6559e893f12d Mon Sep 17 00:00:00 2001
From: Ruifeng Xie <ruifengx@outlook.com>
Date: Fri, 19 Dec 2025 14:06:10 +0800
Subject: [PATCH 3/4] Add irrelevant & antisym to Vec.Pointwise.Extensional

---
 .../Vec/Relation/Binary/Pointwise/Extensional.agda  | 13 +++++++++----
 1 file changed, 9 insertions(+), 4 deletions(-)

diff --git a/src/Data/Vec/Relation/Binary/Pointwise/Extensional.agda b/src/Data/Vec/Relation/Binary/Pointwise/Extensional.agda
index 8dff457607..832bba496c 100644
--- a/src/Data/Vec/Relation/Binary/Pointwise/Extensional.agda
+++ b/src/Data/Vec/Relation/Binary/Pointwise/Extensional.agda
@@ -21,7 +21,7 @@ open import Level using (Level; _⊔_; 0ℓ)
 open import Relation.Binary.Core using (Rel; REL; _⇒_; _=[_]⇒_)
 open import Relation.Binary.Bundles using (Setoid)
 open import Relation.Binary.Structures using (IsEquivalence; IsDecEquivalence)
-open import Relation.Binary.Definitions using (Reflexive; Sym; Trans; Decidable)
+open import Relation.Binary.Definitions using (Reflexive; Sym; Trans; Antisym; Decidable)
 open import Relation.Binary.PropositionalEquality.Core as ≡ using (_≡_)
 open import Relation.Binary.Construct.Closure.Transitive as Plus
   hiding (equivalent; map)
@@ -30,7 +30,7 @@ import Relation.Nullary.Decidable as Dec
 
 private
   variable
-    a b c ℓ : Level
+    a b c ℓ ℓ₁ ℓ₂ : Level
     A : Set a
     B : Set b
     C : Set c
@@ -98,16 +98,21 @@ refl : ∀ {_∼_ : Rel A ℓ} {n} →
        Reflexive _∼_ → Reflexive (Pointwise _∼_ {n = n})
 refl ∼-rfl = ext (λ _ → ∼-rfl)
 
-sym : ∀ {P : REL A B ℓ} {Q : REL B A ℓ} {n} →
+sym : ∀ {P : REL A B ℓ₁} {Q : REL B A ℓ₂} {n} →
       Sym P Q → Sym (Pointwise P) (Pointwise Q {n = n})
 sym sm xs∼ys = ext λ i → sm (Pointwise.app xs∼ys i)
 
-trans : ∀ {P : REL A B ℓ} {Q : REL B C ℓ} {R : REL A C ℓ} {n} →
+trans : ∀ {P : REL A B ℓ₁} {Q : REL B C ℓ₂} {R : REL A C ℓ} {n} →
         Trans P Q R →
         Trans (Pointwise P) (Pointwise Q) (Pointwise R {n = n})
 trans trns xs∼ys ys∼zs = ext λ i →
   trns (Pointwise.app xs∼ys i) (Pointwise.app ys∼zs i)
 
+antisym : ∀ {P : REL A B ℓ₁} {Q : REL B A ℓ₂} {R : REL A B ℓ} {n} →
+          Antisym P Q R → Antisym (Pointwise P {n}) (Pointwise Q) (Pointwise R)
+antisym asym xs∼ys ys∼xs = ext λ i →
+  asym (Pointwise.app xs∼ys i) (Pointwise.app ys∼xs i)
+
 decidable : ∀ {_∼_ : REL A B ℓ} →
             Decidable _∼_ → ∀ {n} → Decidable (Pointwise _∼_ {n = n})
 decidable dec xs ys = Dec.map

From 5650a1d72bd80da38db6b045b725097a58e8b6d6 Mon Sep 17 00:00:00 2001
From: Ruifeng Xie <ruifengx@outlook.com>
Date: Fri, 19 Dec 2025 15:33:10 +0800
Subject: [PATCH 4/4] Update CHANGELOG

---
 CHANGELOG.md | 17 +++++++++++++++++
 1 file changed, 17 insertions(+)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index c88b4856d6..8b3e6b6403 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -42,6 +42,10 @@ Minor improvements
   Data.Nat.Combinatorics
   ```
 
+* In `Data.Vec.Relation.Binary.Pointwise.{Inductive,Extensional}`, the types of
+  `refl`, `sym`, and `trans` have been weakened to allow relations of different
+  levels to be used.
+
 Deprecated modules
 ------------------
 
@@ -254,6 +258,19 @@ Additions to existing modules
                     updateAt (padRight m≤n x xs) (inject≤ i m≤n) f ≡ padRight m≤n x (updateAt xs i f)
   ```
 
+* In `Data.Vec.Relation.Binary.Pointwise.Inductive`
+  ```agda
+  irrelevant : ∀ {_∼_ : REL A B ℓ} {n m} → Irrelevant _∼_ → Irrelevant (Pointwise _∼_ {n} {m})
+  antisym : ∀ {P : REL A B ℓ₁} {Q : REL B A ℓ₂} {R : REL A B ℓ} {m n} →
+            Antisym P Q R → Antisym (Pointwise P {m}) (Pointwise Q {n}) (Pointwise R)
+  ```
+
+* In `Data.Vec.Relation.Binary.Pointwise.Extensional`
+  ```agda
+  antisym : ∀ {P : REL A B ℓ₁} {Q : REL B A ℓ₂} {R : REL A B ℓ} {n} →
+            Antisym P Q R → Antisym (Pointwise P {n}) (Pointwise Q) (Pointwise R)
+  ```
+
 * In `Relation.Nullary.Negation.Core`
   ```agda
   ¬¬-η           : A → ¬ ¬ A