[add] irrelevant & antisym to Pointwise for Data.Vec

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

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

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,23 +88,32 @@ 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 {[]}      = []
+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
 
+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 []