Added functional vector permutation

CHANGELOG.md

@@ -3352,3 +3352,16 @@ This is a full list of proofs that have changed form to use irrelevant instance
       c ≈⟨ c≈d ⟩
       d ∎
     ```
+
+* Added module `Data.Vec.Functional.Relation.Binary.Permutation`:
+  ```agda
+  _↭_ : IRel (Vector A) _
+  ```
+
+* Added new file `Data.Vec.Functional.Relation.Binary.Permutation.Properties`:
+  ```agda
+  ↭-refl : xs ↭ xs
+  ↭-reflexive : xs ≡ ys → xs ↭ ys
+  ↭-sym : xs ↭ ys → ys ↭ xs
+  ↭-trans : xs ↭ ys → ys ↭ zs → xs ↭ zs
+  ```

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 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 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,44 @@
+------------------------------------------------------------------------
+-- 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 using (_,_; proj₁; proj₂)
+open import Data.Nat 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 ≡-Reasoning
+
+private
+  variable
+    ℓ : Level
+    A : Set ℓ
+    n : ℕ
+    xs ys zs : Vector A n
+
+↭-refl : xs ↭ xs
+↭-refl = id , λ _ → refl
+
+↭-reflexive : xs ≡ ys → xs ↭ ys
+↭-reflexive refl = ↭-refl
+
+↭-sym : xs ↭ ys → ys ↭ xs
+proj₁ (↭-sym (xs↭ys , _)) = flip xs↭ys
+proj₂ (↭-sym {xs = xs} {ys = 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 : xs ↭ ys → ys ↭ zs → xs ↭ zs
+proj₁ (↭-trans (xs↭ys , _) (ys↭zs , _))   = ys↭zs ∘ₚ xs↭ys
+proj₂ (↭-trans (_ , xs↭ys) (_ , ys↭zs)) _ = trans (xs↭ys _) (ys↭zs _)