diff --git a/CHANGELOG.md b/CHANGELOG.md
index aeb0d48fcc..5e02e72135 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -148,12 +148,18 @@ New modules
   ```agda
   Function.Properties.Inverse
   Function.Properties.Equivalence
+  ```
 
 * Indexed nullary relations/sets:
   ```
   Relation.Nullary.Indexed
   ```
 
+* Properties for functional vectors:
+  ```
+  Data.Vec.Functional.Properties
+  ```
+
 * Generic printf
   ```
   Text.Format.Generic
@@ -388,6 +394,36 @@ Other minor additions
   _⇔_ : REL A B ℓ₁ → REL A B ℓ₂ → Set _
   ```
 
+* Added new functions to `Data.Fin.Base`:
+  ```agda
+  quotRem : ∀ {n} k → Fin (n ℕ.* k) → Fin k × Fin n
+  opposite : ∀ {n} → Fin n → Fin n
+  ```
+
+* Added new proofs to `Data.Fin.Properties`:
+  ```agda
+  splitAt-< : ∀ m {n} i → (i<m : toℕ i ℕ.< m) → splitAt m {n} i ≡ inj₁ (fromℕ< i<m)
+  splitAt-≥ : ∀ m {n} i → (i≥m : toℕ i ℕ.≥ m) → splitAt m {n} i ≡ inj₂ (reduce≥ i i≥m)
+  ```
+
+* Added new functions to `Data.Vec.Functional`:
+  ```agda
+  length : ∀ {n} → Vector A n → ℕ
+  insert : ∀ {n} → Vector A n → Fin (suc n) → A → Vector A (suc n)
+  updateAt : ∀ {n} → Fin n → (A → A) → Vector A n → Vector A n
+  _++_ : ∀ {m n} → Vector A m → Vector A n → Vector A (m ℕ.+ n)
+  concat : ∀ {m n} → Vector (Vector A m) n → Vector A (n ℕ.* m)
+  _>>=_ : ∀ {m n} → Vector A m → (A → Vector B n) → Vector B (m ℕ.* n)
+  unzipWith : ∀ {n} → (A → B × C) → Vector A n → Vector B n × Vector C n
+  unzip : ∀ {n} → Vector (A × B) n → Vector A n × Vector B n
+  take : ∀ m {n} → Vector A (m ℕ.+ n) → Vector A m
+  drop : ∀ m {n} → Vector A (m ℕ.+ n) → Vector A n
+  reverse : ∀ {n} → Vector A n → Vector A n
+  init : ∀ {n} → Vector A (suc n) → Vector A n
+  last : ∀ {n} → Vector A (suc n) → A
+  transpose : ∀ {m n} → Vector (Vector A n) m → Vector (Vector A m) n
+  ```
+
 Refactorings
 ------------
 
diff --git a/src/Data/Fin/Base.agda b/src/Data/Fin/Base.agda
index a660ef658b..681a8b8463 100644
--- a/src/Data/Fin/Base.agda
+++ b/src/Data/Fin/Base.agda
@@ -15,6 +15,7 @@ module Data.Fin.Base where
 open import Data.Empty using (⊥-elim)
 open import Data.Nat.Base as ℕ using (ℕ; zero; suc; z≤n; s≤s)
 open import Data.Nat.Properties.Core using (≤-pred)
+open import Data.Product as Product using (_×_; _,_)
 open import Data.Sum.Base as Sum using (_⊎_; inj₁; inj₂)
 open import Function.Base using (id; _∘_; _on_)
 open import Level using () renaming (zero to ℓ₀)
@@ -130,6 +131,14 @@ splitAt zero    i       = inj₂ i
 splitAt (suc m) zero    = inj₁ zero
 splitAt (suc m) (suc i) = Sum.map suc id (splitAt m i)
 
+-- quotRem k "i" = "i % k" , "i / k"
+-- This is dual to group from Data.Vec.
+
+quotRem : ∀ {n} k → Fin (n ℕ.* k) → Fin k × Fin n
+quotRem {suc n} k i with splitAt k i
+... | inj₁ j = j , zero
+... | inj₂ j = Product.map₂ suc (quotRem {n} k j)
+
 ------------------------------------------------------------------------
 -- Operations
 
@@ -195,6 +204,12 @@ pred : ∀ {n} → Fin n → Fin n
 pred zero    = zero
 pred (suc i) = inject₁ i
 
+-- opposite "i" = "n - i" (i.e. the additive inverse).
+
+opposite : ∀ {n} → Fin n → Fin n
+opposite {suc n} zero    = fromℕ n
+opposite {suc n} (suc i) = inject₁ (opposite i)
+
 -- The function f(i,j) = if j>i then j-1 else j
 -- This is a variant of the thick function from Conor
 -- McBride's "First-order unification by structural recursion".
diff --git a/src/Data/Fin/Properties.agda b/src/Data/Fin/Properties.agda
index 96d64ef6d3..6ba04d604d 100644
--- a/src/Data/Fin/Properties.agda
+++ b/src/Data/Fin/Properties.agda
@@ -19,7 +19,7 @@ open import Data.Nat.Base as ℕ using (ℕ; zero; suc; s≤s; z≤n; _∸_)
 import Data.Nat.Properties as ℕₚ
 open import Data.Unit using (tt)
 open import Data.Product using (∃; ∃₂; ∄; _×_; _,_; map; proj₁; uncurry; <_,_>)
-open import Data.Sum.Base using (_⊎_; inj₁; inj₂; [_,_])
+open import Data.Sum.Base as Sum using (_⊎_; inj₁; inj₂; [_,_])
 open import Data.Sum.Properties using ([,]-map-commute; [,]-∘-distr)
 open import Function.Base using (_∘_; id; _$_)
 open import Function.Equivalence using (_⇔_; equivalence)
@@ -436,6 +436,17 @@ inject+-raise-splitAt (suc m) n (suc i) = begin
   suc i                                                        ∎
   where open ≡-Reasoning
 
+-- splitAt "m" "i" ≡ inj₁ "i" if i < m
+
+splitAt-< : ∀ m {n} i → (i<m : toℕ i ℕ.< m) → splitAt m {n} i ≡ inj₁ (fromℕ< i<m)
+splitAt-< (suc m) zero    _         = refl
+splitAt-< (suc m) (suc i) (s≤s i<m) = cong (Sum.map suc id) (splitAt-< m i i<m)
+
+-- splitAt "m" "i" ≡ inj₂ "i - m" if i ≥ m
+
+splitAt-≥ : ∀ m {n} i → (i≥m : toℕ i ℕ.≥ m) → splitAt m {n} i ≡ inj₂ (reduce≥ i i≥m)
+splitAt-≥ zero    i       _         = refl
+splitAt-≥ (suc m) (suc i) (s≤s i≥m) = cong (Sum.map suc id) (splitAt-≥ m i i≥m)
 
 ------------------------------------------------------------------------
 -- lift
diff --git a/src/Data/Vec/Functional.agda b/src/Data/Vec/Functional.agda
index 1bc0eef9f5..b0398c1fa3 100644
--- a/src/Data/Vec/Functional.agda
+++ b/src/Data/Vec/Functional.agda
@@ -15,10 +15,10 @@
 
 module Data.Vec.Functional where
 
-open import Data.Fin.Base using (Fin; zero; suc; splitAt; punchIn)
+open import Data.Fin.Base
 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.Nat.Base as ℕ using (ℕ; zero; suc)
+open import Data.Product using (Σ; ∃; _×_; _,_; proj₁; proj₂; uncurry)
 open import Data.Sum.Base using (_⊎_; inj₁; inj₂; [_,_])
 open import Data.Vec.Base as V using (Vec)
 open import Function
@@ -26,6 +26,7 @@ open import Level using (Level)
 
 infixr 5 _∷_ _++_
 infixl 4 _⊛_
+infixl 1 _>>=_
 
 private
   variable
@@ -56,7 +57,7 @@ fromList : ∀ (xs : List A) → Vector A (L.length xs)
 fromList = L.lookup
 
 ------------------------------------------------------------------------
--- Construction and deconstruction
+-- Basic operations
 
 [] : Vector A zero
 [] ()
@@ -65,6 +66,9 @@ _∷_ : ∀ {n} → A → Vector A n → Vector A (suc n)
 (x ∷ xs) zero    = x
 (x ∷ xs) (suc i) = xs i
 
+length : ∀ {n} → Vector A n → ℕ
+length {n = n} _ = n
+
 head : ∀ {n} → Vector A (suc n) → A
 head xs = xs zero
 
@@ -77,18 +81,33 @@ uncons xs = head xs , tail xs
 replicate : ∀ {n} → A → Vector A n
 replicate = const
 
+insert : ∀ {n} → Vector A n → Fin (suc n) → A → Vector A (suc n)
+insert {n = n}     xs zero    v zero    = v
+insert {n = n}     xs zero    v (suc j) = xs j
+insert {n = suc n} xs (suc i) v zero    = head xs
+insert {n = suc n} xs (suc i) v (suc j) = insert (tail xs) i v j
+
 remove : ∀ {n} → Fin (suc n) → Vector A (suc n) → Vector A n
 remove i t = t ∘ punchIn i
 
+updateAt : ∀ {n} → Fin n → (A → A) → Vector A n → Vector A n
+updateAt {n = suc n} zero    f xs zero    = f (head xs)
+updateAt {n = suc n} zero    f xs (suc j) = xs (suc j)
+updateAt {n = suc n} (suc i) f xs zero    = head xs
+updateAt {n = suc n} (suc i) f xs (suc j) = updateAt i f (tail xs) j
+
 ------------------------------------------------------------------------
 -- 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 n} → Vector A m → Vector A n → Vector A (m ℕ.+ n)
 _++_ {m = m} xs ys i = [ xs , ys ] (splitAt m i)
 
+concat : ∀ {m n} → Vector (Vector A m) n → Vector A (n ℕ.* m)
+concat {m = m} xss i = uncurry (flip xss) (quotRem 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))
@@ -103,8 +122,35 @@ rearrange r xs = xs ∘ r
 _⊛_ : ∀ {n} → Vector (A → B) n → Vector A n → Vector B n
 _⊛_ = _ˢ_
 
+_>>=_ : ∀ {m n} → Vector A m → (A → Vector B n) → Vector B (m ℕ.* n)
+xs >>= f = concat (map f xs)
+
 zipWith : (A → B → C) → ∀ {n} → Vector A n → Vector B n → Vector C n
 zipWith f xs ys i = f (xs i) (ys i)
 
+unzipWith : ∀ {n} → (A → B × C) → Vector A n → Vector B n × Vector C n
+unzipWith f xs = proj₁ ∘ f ∘ xs , proj₂ ∘ f ∘ xs
+
 zip : ∀ {n} → Vector A n → Vector B n → Vector (A × B) n
 zip = zipWith _,_
+
+unzip : ∀ {n} → Vector (A × B) n → Vector A n × Vector B n
+unzip = unzipWith id
+
+take : ∀ m {n} → Vector A (m ℕ.+ n) → Vector A m
+take _ {n = n} xs = xs ∘ inject+ n
+
+drop : ∀ m {n} → Vector A (m ℕ.+ n) → Vector A n
+drop m xs = xs ∘ raise m
+
+reverse : ∀ {n} → Vector A n → Vector A n
+reverse xs = xs ∘ opposite
+
+init : ∀ {n} → Vector A (suc n) → Vector A n
+init xs = xs ∘ inject₁
+
+last : ∀ {n} → Vector A (suc n) → A
+last {n = n} xs = xs (fromℕ n)
+
+transpose : ∀ {m n} → Vector (Vector A n) m → Vector (Vector A m) n
+transpose = flip
diff --git a/src/Data/Vec/Functional/Properties.agda b/src/Data/Vec/Functional/Properties.agda
new file mode 100644
index 0000000000..a868739fe9
--- /dev/null
+++ b/src/Data/Vec/Functional/Properties.agda
@@ -0,0 +1,265 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Some Vector-related properties
+------------------------------------------------------------------------
+
+{-# OPTIONS --without-K --safe #-}
+
+module Data.Vec.Functional.Properties where
+
+open import Data.Empty using (⊥-elim)
+open import Data.Fin.Base
+open import Data.Nat as ℕ
+import Data.Nat.Properties as ℕₚ
+open import Data.Product as Product using (_×_; _,_; proj₁; proj₂)
+open import Data.List as L using (List)
+import Data.List.Properties as Lₚ
+open import Data.Sum.Base as Sum using (_⊎_; inj₁; inj₂)
+open import Data.Vec as V using (Vec)
+import Data.Vec.Properties as Vₚ
+open import Data.Vec.Functional
+open import Function.Base
+open import Level using (Level)
+open import Relation.Binary as B
+open import Relation.Binary.PropositionalEquality
+open import Relation.Nullary using (Dec; does; yes; no)
+open import Relation.Nullary.Decidable using (map′)
+open import Relation.Nullary.Product using (_×-dec_)
+
+import Data.Fin.Properties as Finₚ
+
+private
+  variable
+    a b c : Level
+    A : Set a
+    B : Set b
+    C : Set c
+
+------------------------------------------------------------------------
+
+module _ {n} {xs ys : Vector A (suc n)} where
+
+  ∷-cong : head xs ≡ head ys → tail xs ≗ tail ys → xs ≗ ys
+  ∷-cong eq _ zero    = eq
+  ∷-cong _ eq (suc i) = eq i
+
+  ∷-injective : xs ≗ ys → head xs ≡ head ys × tail xs ≗ tail ys
+  ∷-injective eq = eq zero , eq ∘ suc
+
+≗-dec : B.DecidableEquality A →
+        ∀ {n} → B.Decidable {A = Vector A n} _≗_
+≗-dec _≟_ {zero}  xs ys = yes λ ()
+≗-dec _≟_ {suc n} xs ys =
+  map′ (Product.uncurry ∷-cong) ∷-injective
+       (head xs ≟ head ys ×-dec ≗-dec _≟_ (tail xs) (tail ys))
+
+------------------------------------------------------------------------
+-- updateAt
+
+-- (+) updateAt i actually updates the element at index i.
+
+updateAt-updates : ∀ {n} (i : Fin n) {f : A → A} (xs : Vector A n) →
+                   updateAt i f xs i ≡ f (xs i)
+updateAt-updates zero    xs = refl
+updateAt-updates (suc i) xs = updateAt-updates i (tail xs)
+
+-- (-) updateAt i does not touch the elements at other indices.
+
+updateAt-minimal : ∀ {n} (i j : Fin n) {f : A → A} (xs : Vector A n) →
+                   i ≢ j → updateAt j f xs i ≡ xs i
+updateAt-minimal zero    zero    xs 0≢0 = ⊥-elim (0≢0 refl)
+updateAt-minimal zero    (suc j) xs _   = refl
+updateAt-minimal (suc i) zero    xs _   = refl
+updateAt-minimal (suc i) (suc j) xs i≢j = updateAt-minimal i j (tail xs) (i≢j ∘ cong suc)
+
+-- updateAt i is a monoid morphism from A → A to Vector A n → Vector A n.
+
+updateAt-id-relative : ∀ {n} (i : Fin n) {f : A → A} (xs : Vector A n) →
+                       f (xs i) ≡ xs i →
+                       updateAt i f xs ≗ xs
+updateAt-id-relative zero    xs eq zero    = eq
+updateAt-id-relative zero    xs eq (suc j) = refl
+updateAt-id-relative (suc i) xs eq zero    = refl
+updateAt-id-relative (suc i) xs eq (suc j) = updateAt-id-relative i (tail xs) eq j
+
+updateAt-id : ∀ {n} (i : Fin n) (xs : Vector A n) →
+              updateAt i id xs ≗ xs
+updateAt-id i xs = updateAt-id-relative i xs refl
+
+updateAt-compose-relative : ∀ {n} (i : Fin n) {f g h : A → A} (xs : Vector A n) →
+                            f (g (xs i)) ≡ h (xs i) →
+                            updateAt i f (updateAt i g xs) ≗ updateAt i h xs
+updateAt-compose-relative zero    xs eq zero    = eq
+updateAt-compose-relative zero    xs eq (suc j) = refl
+updateAt-compose-relative (suc i) xs eq zero    = refl
+updateAt-compose-relative (suc i) xs eq (suc j) = updateAt-compose-relative i (tail xs) eq j
+
+updateAt-compose : ∀ {n} (i : Fin n) {f g : A → A} (xs : Vector A n) →
+                   updateAt i f (updateAt i g xs) ≗ updateAt i (f ∘ g) xs
+updateAt-compose i xs = updateAt-compose-relative i xs refl
+
+updateAt-cong-relative : ∀ {n} (i : Fin n) {f g : A → A} (xs : Vector A n) →
+                         f (xs i) ≡ g (xs i) →
+                         updateAt i f xs ≗ updateAt i g xs
+updateAt-cong-relative zero    xs eq zero    = eq
+updateAt-cong-relative zero    xs eq (suc j) = refl
+updateAt-cong-relative (suc i) xs eq zero    = refl
+updateAt-cong-relative (suc i) xs eq (suc j) = updateAt-cong-relative i (tail xs) eq j
+
+updateAt-cong : ∀ {n} (i : Fin n) {f g : A → A} →
+                f ≗ g → (xs : Vector A n) → updateAt i f xs ≗ updateAt i g xs
+updateAt-cong zero    eq xs zero    = eq (xs zero)
+updateAt-cong zero    eq xs (suc j) = refl
+updateAt-cong (suc i) eq xs zero    = refl
+updateAt-cong (suc i) eq xs (suc j) = updateAt-cong i eq (tail xs) j
+
+-- The order of updates at different indices i ≢ j does not matter.
+
+updateAt-commutes : ∀ {n} (i j : Fin n) {f g : A → A} → i ≢ j → (xs : Vector A n) →
+                    updateAt i f (updateAt j g xs) ≗ updateAt j g (updateAt i f xs)
+updateAt-commutes zero    zero    0≢0 xs k       = ⊥-elim (0≢0 refl)
+updateAt-commutes zero    (suc j) _   xs zero    = refl
+updateAt-commutes zero    (suc j) _   xs (suc k) = refl
+updateAt-commutes (suc i) zero    _   xs zero    = refl
+updateAt-commutes (suc i) zero    _   xs (suc k) = refl
+updateAt-commutes (suc i) (suc j) _   xs zero    = refl
+updateAt-commutes (suc i) (suc j) i≢j xs (suc k) = updateAt-commutes i j (i≢j ∘ cong suc) (tail xs) k
+
+------------------------------------------------------------------------
+-- map
+
+map-id : ∀ {n} → (xs : Vector A n) → map id xs ≗ xs
+map-id xs = λ _ → refl
+
+map-cong : ∀ {n} {f g : A → B} → f ≗ g → (xs : Vector A n) → map f xs ≗ map g xs
+map-cong f≗g xs = f≗g ∘ xs
+
+map-∘ : ∀ {n} {f : B → C} {g : A → B} →
+        (xs : Vector A n) → map (f ∘ g) xs ≗ map f (map g xs)
+map-∘ xs = λ _ → refl
+
+lookup-map : ∀ {n} (i : Fin n) (f : A → B) (xs : Vector A n) →
+             map f xs i ≡ f (xs i)
+lookup-map i f xs = refl
+
+map-updateAt : ∀ {n} {f : A → B} {g : A → A} {h : B → B}
+               (xs : Vector A n) (i : Fin n) →
+               f (g (xs i)) ≡ h (f (xs i)) →
+               map f (updateAt i g xs) ≗ updateAt i h (map f xs)
+map-updateAt {n = suc n}       {f = f} xs zero    eq zero    = eq
+map-updateAt {n = suc n}       {f = f} xs zero    eq (suc j) = refl
+map-updateAt {n = suc (suc n)} {f = f} xs (suc i) eq zero    = refl
+map-updateAt {n = suc (suc n)} {f = f} xs (suc i) eq (suc j) = map-updateAt {f = f} (tail xs) i eq j
+
+------------------------------------------------------------------------
+-- _++_
+
+lookup-++-< : ∀ {m n} (xs : Vector A m) (ys : Vector A n) →
+              ∀ i (i<m : toℕ i ℕ.< m) →
+              (xs ++ ys) i ≡ xs (fromℕ< i<m)
+lookup-++-< {m = m} xs ys i i<m = cong Sum.[ xs , ys ] (Finₚ.splitAt-< m i i<m)
+
+lookup-++-≥ : ∀ {m n} (xs : Vector A m) (ys : Vector A n) →
+              ∀ i (i≥m : toℕ i ℕ.≥ m) →
+              (xs ++ ys) i ≡ ys (reduce≥ i i≥m)
+lookup-++-≥ {m = m} xs ys i i≥m = cong Sum.[ xs , ys ] (Finₚ.splitAt-≥ m i i≥m)
+
+lookup-++ˡ : ∀ {m n} (xs : Vector A m) (ys : Vector A n) i →
+             (xs ++ ys) (inject+ n i) ≡ xs i
+lookup-++ˡ {m = m} {n = n} xs ys i = cong Sum.[ xs , ys ] (Finₚ.splitAt-inject+ m n i)
+
+lookup-++ʳ : ∀ {m n} (xs : Vector A m) (ys : Vector A n) i →
+             (xs ++ ys) (raise m i) ≡ ys i
+lookup-++ʳ {m = m} {n = n} xs ys i = cong Sum.[ xs , ys ] (Finₚ.splitAt-raise m n i)
+
+module _ {m} {ys ys′ : Vector A m} where
+
+  ++-cong : ∀ {n} (xs xs′ : Vector A n) →
+            xs ≗ xs′ → ys ≗ ys′ → xs ++ ys ≗ xs′ ++ ys′
+  ++-cong {n} xs xs′ eq₁ eq₂ i with toℕ i ℕₚ.<? n
+  ... | yes i<n = begin
+    (xs ++ ys) i      ≡⟨ lookup-++-< xs ys i i<n ⟩
+    xs (fromℕ< i<n)   ≡⟨ eq₁ (fromℕ< i<n) ⟩
+    xs′ (fromℕ< i<n)  ≡˘⟨ lookup-++-< xs′ ys′ i i<n ⟩
+    (xs′ ++ ys′) i    ∎
+    where open ≡-Reasoning
+  ... | no i≮n = begin
+    (xs ++ ys) i               ≡⟨ lookup-++-≥ xs ys i (ℕₚ.≮⇒≥ i≮n) ⟩
+    ys (reduce≥ i (ℕₚ.≮⇒≥ i≮n))   ≡⟨ eq₂ (reduce≥ i (ℕₚ.≮⇒≥ i≮n)) ⟩
+    ys′ (reduce≥ i (ℕₚ.≮⇒≥ i≮n))  ≡˘⟨ lookup-++-≥ xs′ ys′ i (ℕₚ.≮⇒≥ i≮n) ⟩
+    (xs′ ++ ys′) i             ∎
+    where open ≡-Reasoning
+
+  ++-injectiveˡ : ∀ {n} (xs xs′ : Vector A n) →
+                  xs ++ ys ≗ xs′ ++ ys′ → xs ≗ xs′
+  ++-injectiveˡ xs xs′ eq i = begin
+    xs i                        ≡˘⟨ lookup-++ˡ xs ys i ⟩
+    (xs ++ ys) (inject+ m i)    ≡⟨ eq (inject+ m i) ⟩
+    (xs′ ++ ys′) (inject+ m i)  ≡⟨ lookup-++ˡ xs′ ys′ i ⟩
+    xs′ i                       ∎
+    where open ≡-Reasoning
+
+  ++-injectiveʳ : ∀ {n} (xs xs′ : Vector A n) →
+                  xs ++ ys ≗ xs′ ++ ys′ → ys ≗ ys′
+  ++-injectiveʳ {n} xs xs′ eq i = begin
+    ys i                      ≡˘⟨ lookup-++ʳ xs ys i ⟩
+    (xs ++ ys) (raise n i)    ≡⟨ eq (raise n i)   ⟩
+    (xs′ ++ ys′) (raise n i)  ≡⟨ lookup-++ʳ xs′ ys′ i ⟩
+    ys′ i                     ∎
+    where open ≡-Reasoning
+
+  ++-injective : ∀ {n} (xs xs′ : Vector A n) →
+                 xs ++ ys ≗ xs′ ++ ys′ → xs ≗ xs′ × ys ≗ ys′
+  ++-injective xs xs′ eq = ++-injectiveˡ xs xs′ eq , ++-injectiveʳ xs xs′ eq
+
+------------------------------------------------------------------------
+-- insert
+
+insert-lookup : ∀ {n} (xs : Vector A n) (i : Fin (suc n)) (v : A) →
+                insert xs i v i ≡ v
+insert-lookup {n = n}     xs zero    v = refl
+insert-lookup {n = suc n} xs (suc i) v = insert-lookup (tail xs) i v
+
+insert-punchIn : ∀ {n} (xs : Vector A n) (i : Fin (suc n)) (v : A)
+                 (j : Fin n) →
+                 insert xs i v (punchIn i j) ≡ xs j
+insert-punchIn {n = suc n} xs zero    v j       = refl
+insert-punchIn {n = suc n} xs (suc i) v zero    = refl
+insert-punchIn {n = suc n} xs (suc i) v (suc j) = insert-punchIn (tail xs) i v j
+
+------------------------------------------------------------------------
+-- remove
+
+remove-punchOut : ∀ {n} (xs : Vector A (suc n))
+                  {i : Fin (suc n)} {j : Fin (suc n)} (i≢j : i ≢ j) →
+                  remove i xs (punchOut i≢j) ≡ xs j
+remove-punchOut {n = n}     xs {zero}  {zero}  i≢j = ⊥-elim (i≢j refl)
+remove-punchOut {n = suc n} xs {zero}  {suc j} i≢j = refl
+remove-punchOut {n = suc n} xs {suc i} {zero}  i≢j = refl
+remove-punchOut {n = suc n} xs {suc i} {suc j} i≢j = remove-punchOut (tail xs) (i≢j ∘ cong suc)
+
+remove-insert : ∀ {n} (xs : Vector A n) (i : Fin (suc n)) (v : A) →
+                remove i (insert xs i v) ≗ xs
+remove-insert xs zero    v j       = refl
+remove-insert xs (suc i) v zero    = refl
+remove-insert xs (suc i) v (suc j) = remove-insert (tail xs) i v j
+
+insert-remove : ∀ {n} (xs : Vector A (suc n)) (i : Fin (suc n)) →
+                insert (remove i xs) i (xs i) ≗ xs
+insert-remove {n = n}     xs zero    zero    = refl
+insert-remove {n = n}     xs zero    (suc j) = refl
+insert-remove {n = suc n} xs (suc i) zero    = refl
+insert-remove {n = suc n} xs (suc i) (suc j) = insert-remove (tail xs) i j
+
+------------------------------------------------------------------------
+-- Conversion functions
+
+toVec∘fromVec : ∀ {n} → (xs : Vec A n) → toVec (fromVec xs) ≡ xs
+toVec∘fromVec = Vₚ.tabulate∘lookup
+
+fromVec∘toVec : ∀ {n} → (xs : Vector A n) → fromVec (toVec xs) ≗ xs
+fromVec∘toVec = Vₚ.lookup∘tabulate
+
+toList∘fromList : (xs : List A) → toList (fromList xs) ≡ xs
+toList∘fromList = Lₚ.tabulate-lookup