added structure and bundle; tidied up

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