diff --git a/src/Algebra/Operations/CommutativeMonoid.agda b/src/Algebra/Operations/CommutativeMonoid.agda
index 1506e17c80..55753fe4a8 100644
--- a/src/Algebra/Operations/CommutativeMonoid.agda
+++ b/src/Algebra/Operations/CommutativeMonoid.agda
@@ -18,7 +18,7 @@ open import Data.Nat.Base using (ℕ; zero; suc)
 open import Data.List.Base as List using (List; []; _∷_; _++_)
 open import Data.Fin.Base using (Fin; zero)
 open import Data.Product using (proj₁; proj₂)
-open import Data.Table.Base as Table using (Table)
+open import Data.Vec.Functional as V
 open import Function using (_∘_; _⟨_⟩_)
 open import Relation.Binary
 open import Relation.Binary.PropositionalEquality as P using (_≡_)
@@ -59,15 +59,15 @@ suc n ×′ x = x + n ×′ x
 sumₗ : List Carrier → Carrier
 sumₗ = List.foldr _+_ 0#
 
-sumₜ : ∀ {n} → Table Carrier n → Carrier
-sumₜ = Table.foldr _+_ 0#
+sumₜ : ∀ {n} → Vector Carrier n → Carrier
+sumₜ = V.foldr _+_ 0#
 
 -- An alternative mathematical-style syntax for sumₜ
 
 infixl 10 sumₜ-syntax
 
 sumₜ-syntax : ∀ n → (Fin n → Carrier) → Carrier
-sumₜ-syntax _ = sumₜ ∘ Table.tabulate
+sumₜ-syntax _ = sumₜ
 
 syntax sumₜ-syntax n (λ i → x) = ∑[ i < n ] x
 
diff --git a/src/Algebra/Properties/CommutativeMonoid.agda b/src/Algebra/Properties/CommutativeMonoid.agda
index dc14381aa2..2598ebef71 100644
--- a/src/Algebra/Properties/CommutativeMonoid.agda
+++ b/src/Algebra/Properties/CommutativeMonoid.agda
@@ -24,10 +24,11 @@ open import Data.List.Base as List using ([]; _∷_)
 import Data.Fin.Properties as FP
 open import Data.Fin.Permutation as Perm using (Permutation; Permutation′; _⟨$⟩ˡ_; _⟨$⟩ʳ_)
 open import Data.Fin.Permutation.Components as PermC
-open import Data.Table as Table
-open import Data.Table.Relation.Binary.Equality as TE using (_≗_)
 open import Data.Unit using (tt)
-import Data.Table.Properties as TP
+open import Data.Vec.Functional as VF
+open import Data.Vec.Functional.Relation.Binary.Pointwise as VFP using ()
+open import Data.Vec.Functional.Relation.Binary.Pointwise.Properties as VFPP using (_≗_)
+import Data.Vec.Functional.Properties as VProp
 open import Relation.Binary.PropositionalEquality as P using (_≡_)
 open import Relation.Nullary as Nullary using (¬_; does; _because_)
 open import Relation.Nullary.Negation using (contradiction)
@@ -50,13 +51,14 @@ open import Algebra.Definitions _≈_
 open import Relation.Binary.Reasoning.Setoid setoid
 
 module _ {n} where
-  open B.Setoid (TE.setoid setoid n) public
+  open B.Setoid (VFPP.setoid setoid n) public
     using ()
     renaming (_≈_ to _≋_)
 
+
 -- When summing over a function from a finite set, we can pull out any value and move it to the front.
 
-sumₜ-remove : ∀ {n} {i : Fin (suc n)} t → sumₜ t ≈ lookup t i + sumₜ (remove i t)
+sumₜ-remove : ∀ {n} {i : Fin (suc n)} t → sumₜ t ≈ t i + sumₜ (remove i t)
 sumₜ-remove {_}     {zero}   t = refl
 sumₜ-remove {suc n} {suc i}  t′ =
   begin
@@ -66,7 +68,7 @@ sumₜ-remove {suc n} {suc i}  t′ =
   where
   t = tail t′
   t₀ = head t′
-  tᵢ = lookup t i
+  tᵢ = t i
   ∑t = sumₜ t
   ∑t′ = sumₜ (remove i t)
 
@@ -133,26 +135,26 @@ sumₜ-permute {zero}  {zero}  t π = refl
 sumₜ-permute {zero}  {suc n} t π = contradiction π (Perm.refute λ())
 sumₜ-permute {suc m} {zero}  t π = contradiction π (Perm.refute λ())
 sumₜ-permute {suc m} {suc n} t π = begin
-  sumₜ t                                                                            ≡⟨⟩
-  lookup t 0i           + sumₜ (remove 0i t)                                        ≡⟨ P.cong₂ _+_ (P.cong (lookup t) (P.sym (Perm.inverseʳ π))) P.refl ⟩
-  lookup πt (π ⟨$⟩ˡ 0i) + sumₜ (remove 0i t)                                        ≈⟨ +-congˡ (sumₜ-permute (remove 0i t) (Perm.remove (π ⟨$⟩ˡ 0i) π)) ⟩
-  lookup πt (π ⟨$⟩ˡ 0i) + sumₜ (permute (Perm.remove (π ⟨$⟩ˡ 0i) π) (remove 0i t))  ≡⟨ P.cong₂ _+_ P.refl (sumₜ-cong-≡ (P.sym ∘ TP.remove-permute π 0i t)) ⟩
-  lookup πt (π ⟨$⟩ˡ 0i) + sumₜ (remove (π ⟨$⟩ˡ 0i) πt)                              ≈⟨ sym (sumₜ-remove (permute π t)) ⟩
+  sumₜ t                                                                     ≡⟨⟩
+  t 0i           + sumₜ (remove 0i t)                                        ≡⟨ P.cong₂ _+_ (P.cong t (P.sym (Perm.inverseʳ π))) P.refl ⟩
+  πt (π ⟨$⟩ˡ 0i) + sumₜ (remove 0i t)                                        ≈⟨ +-congˡ (sumₜ-permute (remove 0i t) (Perm.remove (π ⟨$⟩ˡ 0i) π)) ⟩
+  πt (π ⟨$⟩ˡ 0i) + sumₜ (permute (Perm.remove (π ⟨$⟩ˡ 0i) π) (remove 0i t))  ≡⟨ P.cong₂ _+_ P.refl (sumₜ-cong-≡ (P.sym ∘ VProp.remove-permute π 0i t)) ⟩
+  πt (π ⟨$⟩ˡ 0i) + sumₜ (remove (π ⟨$⟩ˡ 0i) πt)                              ≈⟨ sym (sumₜ-remove (permute π t)) ⟩
   sumₜ πt                                                                           ∎
   where
   0i = zero
   πt = permute π t
 
 ∑-permute : ∀ {m n} f (π : Permutation m n) → ∑[ i < n ] f i ≈ ∑[ i < m ] f (π ⟨$⟩ʳ i)
-∑-permute = sumₜ-permute ∘ tabulate
+∑-permute = sumₜ-permute -- ∘ tabulate
 
 -- If the function takes the same value at 'i' and 'j', then transposing 'i' and
 -- 'j' then selecting 'j' is the same as selecting 'i'.
 
 select-transpose :
-  ∀ {n} t (i j : Fin n) → lookup t i ≈ lookup t j →
-  ∀ k → (lookup (select 0# j t) ∘ PermC.transpose i j) k
-      ≈  lookup (select 0# i t) k
+  ∀ {n} t (i j : Fin n) → t i ≈ t j →
+  ∀ k → (select 0# j t ∘ PermC.transpose i j) k
+      ≈ select 0# i t k
 select-transpose _ i j e k with k FP.≟ i
 ... | true  because _ rewrite dec-true (j FP.≟ j) P.refl = sym e
 ... | false because [k≢i] with k FP.≟ j
@@ -163,13 +165,13 @@ select-transpose _ i j e k with k FP.≟ i
 
 -- Summing over a pulse gives you the single value picked out by the pulse.
 
-sumₜ-select : ∀ {n i} (t : Table Carrier n) → sumₜ (select 0# i t) ≈ lookup t i
+sumₜ-select : ∀ {n i} (t : Vector Carrier n) → sumₜ (select 0# i t) ≈ t i
 sumₜ-select {suc n} {i} t = begin
-  sumₜ (select 0# i t)                                        ≈⟨ sumₜ-remove {i = i} (select 0# i t) ⟩
-  lookup (select 0# i t) i + sumₜ (remove i (select 0# i t))  ≡⟨ P.cong₂ _+_ (TP.select-lookup t) (sumₜ-cong-≡ (TP.select-remove i t)) ⟩
-  lookup t i + sumₜ (replicate {n = n} 0#)                    ≈⟨ +-congˡ (sumₜ-zero n) ⟩
-  lookup t i + 0#                                             ≈⟨ +-identityʳ _ ⟩
-  lookup t i                                                  ∎
+  sumₜ (select 0# i t)                                 ≈⟨ sumₜ-remove {i = i} (select 0# i t) ⟩
+  select 0# i t i + sumₜ (remove i (select 0# i t))    ≡⟨ P.cong₂ _+_ (VProp.select-lookup t) (sumₜ-cong-≡ (VProp.select-remove i t)) ⟩
+  t i + sumₜ (replicate {n = n} 0#)                    ≈⟨ +-congˡ (sumₜ-zero n) ⟩
+  t i + 0#                                             ≈⟨ +-identityʳ _ ⟩
+  t i                                                  ∎
 
 -- Converting to a table then summing is the same as summing the original list
 
@@ -179,6 +181,6 @@ sumₜ-fromList (x ∷ xs) = P.cong (_ +_) (sumₜ-fromList xs)
 
 -- Converting to a list then summing is the same as summing the original table
 
-sumₜ-toList : ∀ {n} (t : Table Carrier n) → sumₜ t ≡ sumₗ (toList t)
+sumₜ-toList : ∀ {n} (t : Vector Carrier n) → sumₜ t ≡ sumₗ (toList t)
 sumₜ-toList {zero}  _ = P.refl
 sumₜ-toList {suc n} _ = P.cong (_ +_) (sumₜ-toList {n} _)
diff --git a/src/Data/Vec/Functional.agda b/src/Data/Vec/Functional.agda
index 1bc0eef9f5..b6ad0aec50 100644
--- a/src/Data/Vec/Functional.agda
+++ b/src/Data/Vec/Functional.agda
@@ -4,107 +4,33 @@
 -- Vectors defined as functions from a finite set to a type.
 ------------------------------------------------------------------------
 
--- This implementation is designed for reasoning about fixed-size
--- vectors where ease of retrieval of elements is prioritised.
-
--- See `Data.Vec` for an alternative implementation using inductive
--- data-types, which is more suitable for reasoning about vectors that
--- will grow or shrink in size.
-
 {-# OPTIONS --without-K --safe #-}
 
 module Data.Vec.Functional where
 
-open import Data.Fin.Base using (Fin; zero; suc; splitAt; punchIn)
-open import Data.List.Base as L using (List)
-open import Data.Nat.Base using (ℕ; zero; suc; _+_)
-open import Data.Product using (Σ; ∃; _×_; _,_; proj₁; proj₂)
-open import Data.Sum.Base using (_⊎_; inj₁; inj₂; [_,_])
-open import Data.Vec.Base as V using (Vec)
-open import Function
-open import Level using (Level)
-
-infixr 5 _∷_ _++_
-infixl 4 _⊛_
-
-private
-  variable
-    a b c : Level
-    A : Set a
-    B : Set b
-    C : Set c
-
-------------------------------------------------------------------------
--- Definition
-
-Vector : Set a → ℕ → Set a
-Vector A n = Fin n → A
-
-------------------------------------------------------------------------
--- Conversion
-
-toVec : ∀ {n} → Vector A n → Vec A n
-toVec = V.tabulate
-
-fromVec : ∀ {n} → Vec A n → Vector A n
-fromVec = V.lookup
-
-toList : ∀ {n} → Vector A n → List A
-toList = L.tabulate
-
-fromList : ∀ (xs : List A) → Vector A (L.length xs)
-fromList = L.lookup
-
-------------------------------------------------------------------------
--- Construction and deconstruction
-
-[] : Vector A zero
-[] ()
-
-_∷_ : ∀ {n} → A → Vector A n → Vector A (suc n)
-(x ∷ xs) zero    = x
-(x ∷ xs) (suc i) = xs i
-
-head : ∀ {n} → Vector A (suc n) → A
-head xs = xs zero
-
-tail : ∀ {n} → Vector A (suc n) → Vector A n
-tail xs = xs ∘ suc
-
-uncons : ∀ {n} → Vector A (suc n) → A × Vector A n
-uncons xs = head xs , tail xs
-
-replicate : ∀ {n} → A → Vector A n
-replicate = const
-
-remove : ∀ {n} → Fin (suc n) → Vector A (suc n) → Vector A n
-remove i t = t ∘ punchIn i
-
-------------------------------------------------------------------------
--- Transformations
-
-map : (A → B) → ∀ {n} → Vector A n → Vector B n
-map f xs = f ∘ xs
-
-_++_ : ∀ {m n} → Vector A m → Vector A n → Vector A (m + n)
-_++_ {m = m} xs ys i = [ xs , ys ] (splitAt m i)
+open import Data.Vec.Functional.Base public
 
-foldr : (A → B → B) → B → ∀ {n} → Vector A n → B
-foldr f z {n = zero}  xs = z
-foldr f z {n = suc n} xs = f (head xs) (foldr f z (tail xs))
+open import Data.Bool.Base using (true; false)
+open import Data.Fin using (Fin; _≟_)
+open import Function.Equality using (_⟨$⟩_)
+open import Function.Inverse using (Inverse; _↔_)
+open import Relation.Nullary using (does)
+open import Relation.Nullary.Decidable using (⌊_⌋)
 
-foldl : (B → A → B) → B → ∀ {n} → Vector A n → B
-foldl f z {n = zero}  xs = z
-foldl f z {n = suc n} xs = foldl f (f z (head xs)) (tail xs)
+--------------------------------------------------------------------------------
+--  Combinators
+--------------------------------------------------------------------------------
 
-rearrange : ∀ {m n} → (Fin m → Fin n) → Vector A n → Vector A m
-rearrange r xs = xs ∘ r
+-- Changes the order of elements in the table according to a permutation (i.e.
+-- an 'Inverse' object on the indices).
 
-_⊛_ : ∀ {n} → Vector (A → B) n → Vector A n → Vector B n
-_⊛_ = _ˢ_
+permute : ∀ {m n a} {A : Set a} → Fin m ↔ Fin n → Vector A n → Vector A m
+permute π = rearrange (Inverse.to π ⟨$⟩_)
 
-zipWith : (A → B → C) → ∀ {n} → Vector A n → Vector B n → Vector C n
-zipWith f xs ys i = f (xs i) (ys i)
+-- The result of 'select z i t' takes the value of 'lookup t i' at index 'i',
+-- and 'z' everywhere else.
 
-zip : ∀ {n} → Vector A n → Vector B n → Vector (A × B) n
-zip = zipWith _,_
+select : ∀ {n} {a} {A : Set a} → A → Fin n → Vector A n → Vector A n
+select z i t j with does (j ≟ i)
+... | true  = t i
+... | false = z
diff --git a/src/Data/Vec/Functional/Base.agda b/src/Data/Vec/Functional/Base.agda
new file mode 100644
index 0000000000..29c1062065
--- /dev/null
+++ b/src/Data/Vec/Functional/Base.agda
@@ -0,0 +1,110 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Vectors defined as functions from a finite set to a type.
+------------------------------------------------------------------------
+
+-- This implementation is designed for reasoning about fixed-size
+-- vectors where ease of retrieval of elements is prioritised.
+
+-- See `Data.Vec` for an alternative implementation using inductive
+-- data-types, which is more suitable for reasoning about vectors that
+-- will grow or shrink in size.
+
+{-# OPTIONS --without-K --safe #-}
+
+module Data.Vec.Functional.Base where
+
+open import Data.Fin.Base using (Fin; zero; suc; splitAt; punchIn)
+open import Data.List.Base as L using (List)
+open import Data.Nat.Base using (ℕ; zero; suc; _+_)
+open import Data.Product using (Σ; ∃; _×_; _,_; proj₁; proj₂)
+open import Data.Sum.Base using (_⊎_; inj₁; inj₂; [_,_])
+open import Data.Vec.Base as V using (Vec)
+open import Function
+open import Level using (Level)
+
+infixr 5 _∷_ _++_
+infixl 4 _⊛_
+
+private
+  variable
+    a b c : Level
+    A : Set a
+    B : Set b
+    C : Set c
+
+------------------------------------------------------------------------
+-- Definition
+
+Vector : Set a → ℕ → Set a
+Vector A n = Fin n → A
+
+------------------------------------------------------------------------
+-- Conversion
+
+toVec : ∀ {n} → Vector A n → Vec A n
+toVec = V.tabulate
+
+fromVec : ∀ {n} → Vec A n → Vector A n
+fromVec = V.lookup
+
+toList : ∀ {n} → Vector A n → List A
+toList = L.tabulate
+
+fromList : ∀ (xs : List A) → Vector A (L.length xs)
+fromList = L.lookup
+
+------------------------------------------------------------------------
+-- Construction and deconstruction
+
+[] : Vector A zero
+[] ()
+
+_∷_ : ∀ {n} → A → Vector A n → Vector A (suc n)
+(x ∷ xs) zero    = x
+(x ∷ xs) (suc i) = xs i
+
+head : ∀ {n} → Vector A (suc n) → A
+head xs = xs zero
+
+tail : ∀ {n} → Vector A (suc n) → Vector A n
+tail xs = xs ∘ suc
+
+uncons : ∀ {n} → Vector A (suc n) → A × Vector A n
+uncons xs = head xs , tail xs
+
+replicate : ∀ {n} → A → Vector A n
+replicate = const
+
+remove : ∀ {n} → Fin (suc n) → Vector A (suc n) → Vector A n
+remove i t = t ∘ punchIn i
+
+------------------------------------------------------------------------
+-- Transformations
+
+map : (A → B) → ∀ {n} → Vector A n → Vector B n
+map f xs = f ∘ xs
+
+_++_ : ∀ {m n} → Vector A m → Vector A n → Vector A (m + n)
+_++_ {m = m} xs ys i = [ xs , ys ] (splitAt m i)
+
+foldr : (A → B → B) → B → ∀ {n} → Vector A n → B
+foldr f z {n = zero}  xs = z
+foldr f z {n = suc n} xs = f (head xs) (foldr f z (tail xs))
+
+foldl : (B → A → B) → B → ∀ {n} → Vector A n → B
+foldl f z {n = zero}  xs = z
+foldl f z {n = suc n} xs = foldl f (f z (head xs)) (tail xs)
+
+rearrange : ∀ {m n} → (Fin m → Fin n) → Vector A n → Vector A m
+rearrange r xs = xs ∘ r
+
+_⊛_ : ∀ {n} → Vector (A → B) n → Vector A n → Vector B n
+_⊛_ = _ˢ_
+
+zipWith : (A → B → C) → ∀ {n} → Vector A n → Vector B n → Vector C n
+zipWith f xs ys i = f (xs i) (ys i)
+
+zip : ∀ {n} → Vector A n → Vector B n → Vector (A × B) n
+zip = zipWith _,_
diff --git a/src/Data/Vec/Functional/Properties.agda b/src/Data/Vec/Functional/Properties.agda
new file mode 100644
index 0000000000..67d7b6ee60
--- /dev/null
+++ b/src/Data/Vec/Functional/Properties.agda
@@ -0,0 +1,112 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Properties for functional vectors
+------------------------------------------------------------------------
+
+{-# OPTIONS --without-K --safe #-}
+
+module Data.Vec.Functional.Properties where
+
+open import Data.Vec.Functional
+open import Data.Vec.Functional.Relation.Binary.Pointwise
+open import Data.Vec.Functional.Relation.Binary.Pointwise.Properties using (_≗_; ≡-setoid)
+
+open import Data.Bool.Base using (true; false; if_then_else_)
+open import Data.Nat.Base using (zero; suc)
+open import Data.Empty using (⊥-elim)
+open import Data.Fin using (Fin; suc; zero; _≟_; punchIn)
+import Data.Fin.Properties as FP
+open import Data.Fin.Permutation as Perm using (Permutation; _⟨$⟩ʳ_; _⟨$⟩ˡ_)
+open import Data.List.Base as L using (List; _∷_; [])
+open import Data.List.Relation.Unary.Any using (here; there; index)
+open import Data.List.Membership.Propositional using (_∈_)
+open import Data.Product as Product using (Σ; ∃; _,_; proj₁; proj₂)
+open import Data.Vec.Base as V using (Vec; _∷_; [])
+import Data.Vec.Properties as VP
+open import Level using (Level)
+open import Function.Base using (_∘_; flip)
+open import Function.Inverse using (Inverse)
+open import Relation.Binary.PropositionalEquality as P
+  using (_≡_; _≢_; refl; sym; cong)
+open import Relation.Nullary using (does)
+open import Relation.Nullary.Decidable using (dec-true; dec-false)
+open import Relation.Nullary.Negation using (contradiction)
+
+private
+  variable
+    a : Level
+    A : Set a
+
+------------------------------------------------------------------------
+-- select
+
+-- Selecting from any table is the same as selecting from a constant table.
+
+select-const : ∀ {n} (z : A) (i : Fin n) t →
+               select z i t ≗ select z i (replicate (t i))
+select-const z i t j with does (j ≟ i)
+... | true  = refl
+... | false = refl
+
+-- Selecting an element from a table then looking it up is the same as looking
+-- up the index in the original table
+
+select-lookup : ∀ {n x i} (t : Vector A n) →
+                select x i t i ≡ t i
+select-lookup {i = i} t rewrite dec-true (i ≟ i) refl = refl
+
+-- Selecting an element from a table then removing the same element produces a
+-- constant table
+
+select-remove : ∀ {n x} i (t : Vector A (suc n)) →
+                remove i (select x i t) ≗ replicate {n = n} x
+select-remove i t j rewrite dec-false (punchIn i j ≟ i) (FP.punchInᵢ≢i _ _)
+                          = refl
+
+
+------------------------------------------------------------------------
+-- permute
+
+-- Removing an index 'i' from a table permuted with 'π' is the same as
+-- removing the element, then permuting with 'π' minus 'i'.
+
+remove-permute : ∀ {m n} (π : Permutation (suc m) (suc n))
+                 i (t : Vector A (suc n)) →
+                 remove (π ⟨$⟩ˡ i) (permute π t)
+                 ≗ permute (Perm.remove (π ⟨$⟩ˡ i) π) (remove i t)
+remove-permute π i t j = P.cong t (Perm.punchIn-permute′ π i j)
+
+------------------------------------------------------------------------
+-- fromList
+
+fromList-∈ : ∀ {xs : List A} (i : Fin (L.length xs)) → fromList xs i ∈ xs
+fromList-∈ {xs = x ∷ xs} zero    = here refl
+fromList-∈ {xs = x ∷ xs} (suc i) = there (fromList-∈ i)
+
+index-fromList-∈ : ∀ {xs : List A} {i} → index (fromList-∈ {xs = xs} i) ≡ i
+index-fromList-∈ {xs = x ∷ xs} {zero}  = refl
+index-fromList-∈ {xs = x ∷ xs} {suc i} = cong suc index-fromList-∈
+
+fromList-index : ∀ {xs} {x : A} (x∈xs : x ∈ xs) → fromList xs (index x∈xs) ≡ x
+fromList-index (here px)    = sym px
+fromList-index (there x∈xs) = fromList-index x∈xs
+
+------------------------------------------------------------------------
+-- There exists an isomorphism between tables and vectors.
+
+↔Vec : ∀ {n} → Inverse (≡-setoid A n) (P.setoid (Vec A n))
+↔Vec = record
+  { to = record { _⟨$⟩_ = toVec ; cong = VP.tabulate-cong }
+  ; from = P.→-to-⟶ fromVec
+  ; inverse-of = record
+    { left-inverse-of  = VP.lookup∘tabulate
+    ; right-inverse-of = VP.tabulate∘lookup
+    }
+  }
+
+------------------------------------------------------------------------
+-- Other
+
+lookup∈ : ∀ {xs : List A} (i : Fin (L.length xs)) → ∃ λ x → x ∈ xs
+lookup∈ i = _ , fromList-∈ i
diff --git a/src/Data/Vec/Functional/Relation/Binary/Pointwise/Properties.agda b/src/Data/Vec/Functional/Relation/Binary/Pointwise/Properties.agda
index f961e2f118..ae47155081 100644
--- a/src/Data/Vec/Functional/Relation/Binary/Pointwise/Properties.agda
+++ b/src/Data/Vec/Functional/Relation/Binary/Pointwise/Properties.agda
@@ -10,7 +10,7 @@ module Data.Vec.Functional.Relation.Binary.Pointwise.Properties where
 
 open import Data.Fin.Base
 open import Data.Fin.Properties
-  hiding (isDecEquivalence; setoid; decSetoid)
+  hiding (isDecEquivalence; setoid; ≡-setoid; decSetoid)
 open import Data.Nat.Base
 open import Data.Product using (_×_; _,_; proj₁; proj₂)
 open import Data.Product.Relation.Binary.Pointwise.NonDependent
@@ -80,6 +80,13 @@ decSetoid S n = record
   { isDecEquivalence = isDecEquivalence S.isDecEquivalence n
   } where module S = DecSetoid S
 
+≡-setoid : ∀ {a} → Set a → ℕ → Setoid _ _
+≡-setoid A = setoid (≡.setoid A)
+
+module _ {a} {A : Set a} {n} where
+  open Setoid (≡-setoid A n) public
+    using () renaming (_≈_ to _≗_)
+
 ------------------------------------------------------------------------
 -- map