Added functional vector permutation

CHANGELOG.md

@@ -187,3 +187,16 @@ Additions to existing modules
   ```agda
   ⌊⌋-map′ : (a? : Dec A) → ⌊ map′ t f a? ⌋ ≡ ⌊ a? ⌋
   ```
+
+* Added module `Data.Vec.Functional.Relation.Binary.Permutation`:
+  ```agda
+  _↭_ : IRel (Vector A) _
+  ```
+
+* Added new file `Data.Vec.Functional.Relation.Binary.Permutation.Properties`:
+  ```agda
+  ↭-refl      : Reflexive (Vector A) _↭_
+  ↭-reflexive : xs ≡ ys → xs ↭ ys
+  ↭-sym       : Symmetric (Vector A) _↭_
+  ↭-trans     : Transitive (Vector A) _↭_
+  ```

src/Data/Vec/Functional/Relation/Binary/Permutation.agda

@@ -0,0 +1,26 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Permutation relations over Vector
+------------------------------------------------------------------------
+
+{-# OPTIONS --cubical-compatible --safe #-}
+
+module Data.Vec.Functional.Relation.Binary.Permutation where
+
+open import Level using (Level)
+open import Data.Product.Base using (Σ-syntax)
+open import Data.Fin.Permutation using (Permutation; _⟨$⟩ʳ_)
+open import Data.Vec.Functional using (Vector)
+open import Relation.Binary.Indexed.Heterogeneous.Core using (IRel)
+open import Relation.Binary.PropositionalEquality.Core using (_≡_)
+
+private
+  variable
+    ℓ : Level
+    A : Set ℓ
+
+infix 3 _↭_
+
+_↭_ : IRel (Vector A) _
+xs ↭ ys = Σ[ ρ ∈ Permutation _ _ ] (∀ i → xs (ρ ⟨$⟩ʳ i) ≡ ys i)

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

@@ -0,0 +1,45 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Properties of permutation
+------------------------------------------------------------------------
+
+{-# OPTIONS --cubical-compatible --safe #-}
+
+module Data.Vec.Functional.Relation.Binary.Permutation.Properties where
+
+open import Level using (Level)
+open import Data.Product.Base using (_,_; proj₁; proj₂)
+open import Data.Nat.Base using (ℕ)
+open import Data.Fin.Permutation using (id; flip; _⟨$⟩ʳ_; inverseʳ; _∘ₚ_)
+open import Data.Vec.Functional
+open import Data.Vec.Functional.Relation.Binary.Permutation
+open import Relation.Binary.PropositionalEquality
+  using (refl; trans; _≡_; cong; module ≡-Reasoning)
+open import Relation.Binary.Indexed.Heterogeneous.Definitions
+
+open ≡-Reasoning
+
+private
+  variable
+    ℓ : Level
+    A : Set ℓ
+    n : ℕ
+    xs ys : Vector A n
+
+↭-refl : Reflexive (Vector A) _↭_
+↭-refl = id , λ _ → refl
+
+↭-reflexive : xs ≡ ys → xs ↭ ys
+↭-reflexive refl = ↭-refl
+
+↭-sym : Symmetric (Vector A) _↭_
+proj₁ (↭-sym (xs↭ys , _)) = flip xs↭ys
+proj₂ (↭-sym {x = xs} {ys} (xs↭ys , xs↭ys≡)) i = begin
+  ys (flip xs↭ys ⟨$⟩ʳ i)             ≡˘⟨ xs↭ys≡ _ ⟩
+  xs (xs↭ys ⟨$⟩ʳ (flip xs↭ys ⟨$⟩ʳ i)) ≡⟨ cong xs (inverseʳ xs↭ys) ⟩
+  xs i ∎
+
+↭-trans : Transitive (Vector A) _↭_
+proj₁ (↭-trans (xs↭ys , _) (ys↭zs , _))   = ys↭zs ∘ₚ xs↭ys
+proj₂ (↭-trans (_ , xs↭ys) (_ , ys↭zs)) _ = trans (xs↭ys _) (ys↭zs _)