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
+ }