Tidy up functional vector permutation #2066

CHANGELOG.md

@@ -54,7 +54,22 @@ New modules
   ```agda
   Algebra.Module.Construct.Idealization
   ```
-
+
+* `Data.Vec.Functional.Relation.Binary.Permutation`, defining:
+  ```agda
+  _↭_ : IRel (Vector A) _
+  ```
+
+* `Data.Vec.Functional.Relation.Binary.Permutation.Properties` of the above:
+  ```agda
+  ↭-refl      : Reflexive (Vector A) _↭_
+  ↭-reflexive : xs ≡ ys → xs ↭ ys
+  ↭-sym       : Symmetric (Vector A) _↭_
+  ↭-trans     : Transitive (Vector A) _↭_
+  isIndexedEquivalence : {A : Set a} → IsIndexedEquivalence (Vector A) _↭_
+  indexedSetoid        : {A : Set a} → IndexedSetoid ℕ a _
+  ```
+
 * `Function.Relation.Binary.Equality`
   ```agda
   setoid : Setoid a₁ a₂ → Setoid b₁ b₂ → Setoid _ _
@@ -246,26 +261,13 @@ Additions to existing modules
   WeaklyDecidable : Set _
   ```
 
-* Added new definitions in `Relation.Unary`
-  ```
-  Stable          : Pred A ℓ → Set _
-  WeaklyDecidable : Pred A ℓ → Set _
-  ```
-
 * Added new proof in `Relation.Nullary.Decidable`:
   ```agda
   ⌊⌋-map′ : (a? : Dec A) → ⌊ map′ t f a? ⌋ ≡ ⌊ a? ⌋
   ```
 
-* Added module `Data.Vec.Functional.Relation.Binary.Permutation`:
-  ```agda
-  _↭_ : IRel (Vector A) _
+* Added new definitions in `Relation.Unary`
   ```
-
-* 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) _↭_
+  Stable          : Pred A ℓ → Set _
+  WeaklyDecidable : Pred A ℓ → Set _
   ```

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

@@ -17,8 +17,8 @@ open import Relation.Binary.PropositionalEquality.Core using (_≡_)
 
 private
   variable
-    ℓ : Level
-    A : Set ℓ
+    a : Level
+    A : Set a
 
 infix 3 _↭_
 

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

@@ -15,18 +15,20 @@ 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
+  using (_≡_; refl; trans; cong; module ≡-Reasoning)
+open import Relation.Binary.Indexed.Heterogeneous
 
 private
   variable
-    ℓ : Level
-    A : Set ℓ
+    a : Level
+    A : Set a
     n : ℕ
     xs ys : Vector A n
 
+
+------------------------------------------------------------------------
+-- Basics
+
 ↭-refl : Reflexive (Vector A) _↭_
 ↭-refl = id , λ _ → refl
 
@@ -36,10 +38,32 @@ private
 ↭-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≡ _ ⟩
+  ys (flip xs↭ys ⟨$⟩ʳ i)              ≡⟨ xs↭ys≡ _ ⟨
   xs (xs↭ys ⟨$⟩ʳ (flip xs↭ys ⟨$⟩ʳ i)) ≡⟨ cong xs (inverseʳ xs↭ys) ⟩
-  xs i ∎
+  xs i                                ∎
+  where open ≡-Reasoning
 
 ↭-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 _)
+
+------------------------------------------------------------------------
+-- Structure
+
+isIndexedEquivalence : IsIndexedEquivalence (Vector A) _↭_
+isIndexedEquivalence {A = A} = record
+  { refl = ↭-refl
+  ; sym = ↭-sym
+  ; trans = λ {n₁ n₂ n₃} {xs : Vector A n₁} {ys : Vector A n₂} {zs : Vector A n₃}
+              xs↭ys ys↭zs → ↭-trans {i = n₁} {i = xs} xs↭ys ys↭zs
+  }
+
+------------------------------------------------------------------------
+-- Bundle
+
+indexedSetoid : {A : Set a} → IndexedSetoid ℕ a _
+indexedSetoid {A = A} = record
+  { Carrier = Vector A
+  ; _≈_ = _↭_
+  ; isEquivalence = isIndexedEquivalence
+  }