diff --git a/CHANGELOG.md b/CHANGELOG.md
index d9db593cef..f787065436 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -797,6 +797,50 @@ Non-backwards compatible changes
   IO.Instances
   ```
 
+### Standardisation of `insertAt`/`updateAt`/`removeAt`
+
+* Previously, the names and argument order of index-based insertion, update and removal functions for
+  various types of lists and vectors were inconsistent.
+
+* To fix this the names have all been standardised to `insertAt`/`updateAt`/`removeAt`.
+
+* Correspondingly the following changes have occurred:
+
+* In `Data.List.Base` the following have been added:
+  ```agda
+  insertAt : (xs : List A) → Fin (suc (length xs)) → A → List A
+  updateAt : (xs : List A) → Fin (length xs) → (A → A) → List A
+  removeAt : (xs : List A) → Fin (length xs) → List A
+  ```
+  and the following has been deprecated
+  ```
+  _─_ ↦ removeAt
+  ```
+  
+* In `Data.Vec.Base`:
+  ```agda
+  insert ↦ insertAt
+  remove ↦ removeAt
+  
+  updateAt : Fin n → (A → A) → Vec A n → Vec A n
+    ↦
+  updateAt : Vec A n → Fin n → (A → A) → Vec A n
+  ```
+
+* In `Data.Vec.Functional`:
+  ```agda
+  remove : Fin (suc n) → Vector A (suc n) → Vector A n
+    ↦
+  removeAt : Vector A (suc n) → Fin (suc n) → Vector A n
+ 
+  updateAt : Fin n → (A → A) → Vector A n → Vector A n
+    ↦
+  updateAt : Vector A n → Fin n → (A → A) → Vector A n
+  ```
+  
+* The old names (and the names of all proofs about these functions) have been deprecated appropriately.
+
+
 ### Changes to triple reasoning interface
 
 * The module `Relation.Binary.Reasoning.Base.Triple` now takes an extra proof that the strict
@@ -1321,6 +1365,11 @@ Deprecated names
   +-isAbelianGroup ↦ +-0-isAbelianGroup
   ```
 
+* In `Data.List.Base`:
+  ```
+  _─_  ↦  removeAt
+  ```
+
 * In `Data.List.Properties`:
   ```agda
   map-id₂         ↦  map-id-local
@@ -1337,7 +1386,10 @@ Deprecated names
 
   ʳ++-++  ↦  ++-ʳ++
 
-  take++drop ↦ take++drop≡id
+  take++drop  ↦  take++drop≡id
+
+  length-─  ↦  length-removeAt
+  map-─     ↦  map-removeAt
   ```
 
 * In `Data.List.NonEmpty.Properties`:
@@ -1350,8 +1402,8 @@ Deprecated names
 * In `Data.List.Relation.Unary.All.Properties`:
   ```agda
   updateAt-id-relative      ↦  updateAt-id-local
-  updateAt-compose-relative ↦  updateAt-∘-local
-  updateAt-compose          ↦  updateAt-∘
+  updateAt-compose-relative ↦  updateAt-updateAt-local
+  updateAt-compose          ↦  updateAt-updateAt
   updateAt-cong-relative    ↦  updateAt-cong-local
   ```
 
@@ -1497,6 +1549,12 @@ Deprecated names
   map-compose     ↦  map-∘
   ```
 
+* In `Data.Vec.Base`:
+  ```
+  remove  ↦  removeAt
+  insert  ↦  insertAt
+  ```
+
 * In `Data.Vec.Properties`:
   ```
   take-distr-zipWith ↦  take-zipWith
@@ -1505,8 +1563,8 @@ Deprecated names
   drop-distr-map     ↦  drop-map
 
   updateAt-id-relative      ↦  updateAt-id-local
-  updateAt-compose-relative ↦  updateAt-∘-local
-  updateAt-compose          ↦  updateAt-∘
+  updateAt-compose-relative ↦  updateAt-updateAt-local
+  updateAt-compose          ↦  updateAt-updateAt
   updateAt-cong-relative    ↦  updateAt-cong-local
 
   []%=-compose    ↦  []%=-∘
@@ -1516,7 +1574,15 @@ Deprecated names
   idIsFold        ↦ id-is-foldr
   sum-++-commute  ↦ sum-++
 
-  take-drop-id ↦ take++drop≡id
+  take-drop-id  ↦  take++drop≡id
+
+  map-insert       ↦  map-insertAt
+  
+  insert-lookup    ↦  insertAt-lookup
+  insert-punchIn   ↦  insertAt-punchIn
+  remove-PunchOut  ↦  removeAt-punchOut
+  remove-insert    ↦  removeAt-insertAt
+  insert-remove    ↦  insertAt-removeAt
 
   lookup-inject≤-take ↦ lookup-take-inject≤
   ```
@@ -1532,11 +1598,17 @@ Deprecated names
 * In `Data.Vec.Functional.Properties`:
   ```
   updateAt-id-relative      ↦  updateAt-id-local
-  updateAt-compose-relative ↦  updateAt-∘-local
-  updateAt-compose          ↦  updateAt-∘
+  updateAt-compose-relative ↦  updateAt-updateAt-local
+  updateAt-compose          ↦  updateAt-updateAt
   updateAt-cong-relative    ↦  updateAt-cong-local
 
   map-updateAt              ↦  map-updateAt-local
+  
+  insert-lookup             ↦  insertAt-lookup
+  insert-punchIn            ↦  insertAt-punchIn
+  remove-punchOut           ↦  removeAt-punchOut
+  remove-insert             ↦  removeAt-insertAt
+  insert-remove             ↦  insertAt-removeAt
   ```
   NB. This last one is complicated by the *addition* of a 'global' property `map-updateAt`
 
@@ -2312,7 +2384,7 @@ Additions to existing modules
   gcd-zero  : Zero 1ℤ gcd
   ```
 
-* Added new functions in `Data.List`:
+* Added new functions in `Data.List.Base`:
   ```agda
   takeWhileᵇ   : (A → Bool) → List A → List A
   dropWhileᵇ   : (A → Bool) → List A → List A
@@ -2331,14 +2403,14 @@ Additions to existing modules
   find         : Decidable P → List A → Maybe A
   findIndex    : Decidable P → (xs : List A) → Maybe $ Fin (length xs)
   findIndices  : Decidable P → (xs : List A) → List $ Fin (length xs)
-  ```
 
-* Added new functions and definitions to `Data.List.Base`:
-  ```agda
-  catMaybes : List (Maybe A) → List A
-  ap : List (A → B) → List A → List B
-  ++-rawMagma : Set a → RawMagma a _
+  catMaybes       : List (Maybe A) → List A
+  ap              : List (A → B) → List A → List B
+  ++-rawMagma     : Set a → RawMagma a _
   ++-[]-rawMonoid : Set a → RawMonoid a _
+
+  insertAt : (xs : List A) → Fin (suc (length xs)) → A → List A
+  updateAt : (xs : List A) → Fin (length xs) → (A → A) → List A
   ```
 
 * Added new proofs in `Data.List.Relation.Binary.Lex.Strict`:
@@ -2405,6 +2477,11 @@ Additions to existing modules
   map-replicate : map f (replicate n x) ≡ replicate n (f x)
 
   drop-drop : drop n (drop m xs) ≡ drop (m + n) xs
+
+  length-insertAt   : length (insertAt xs i v) ≡ suc (length xs)
+  length-removeAt′  : length xs ≡ suc (length (removeAt xs k))
+  removeAt-insertAt : removeAt (insertAt xs i v) ((cast (sym (length-insertAt xs i v)) i)) ≡ xs
+  insertAt-removeAt : insertAt (removeAt xs i) (cast (sym (lengthAt-removeAt xs i)) i) (lookup xs i) ≡ xs
   ```
 
 * Added new patterns and definitions to `Data.Nat.Base`:
@@ -2841,6 +2918,9 @@ Additions to existing modules
   fromList-map  : cast _ (fromList (List.map f xs)) ≡ map f (fromList xs)
   fromList-++   : cast _ (fromList (xs List.++ ys)) ≡ fromList xs ++ fromList ys
 
+  length-toList   : List.length (toList xs) ≡ length xs
+  toList-insertAt : toList (insertAt xs i v) ≡ List.insertAt (toList xs) (Fin.cast (cong suc (sym (length-toList xs))) i) v
+
   truncate≡take       : .(eq : n ≡ m + o) → truncate m≤n xs ≡ take m (cast eq xs)
   take≡truncate       : take m xs ≡ truncate (m≤m+n m n) xs
   lookup-truncate     : lookup (truncate m≤n xs) i ≡ lookup xs (Fin.inject≤ i m≤n)
diff --git a/src/Algebra/Properties/CommutativeMonoid/Sum.agda b/src/Algebra/Properties/CommutativeMonoid/Sum.agda
index 6cb417bc69..5873d4eb61 100644
--- a/src/Algebra/Properties/CommutativeMonoid/Sum.agda
+++ b/src/Algebra/Properties/CommutativeMonoid/Sum.agda
@@ -46,7 +46,7 @@ open import Algebra.Properties.Monoid.Sum monoid public
 
 -- 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 ≈ t i + sum (remove i t)
+sum-remove : ∀ {n} {i : Fin (suc n)} t → sum t ≈ t i + sum (removeAt t i)
 sum-remove {_}     {zero}   xs = refl
 sum-remove {suc n} {suc i}  xs = begin
   t₀ + ∑t           ≈⟨ +-congˡ (sum-remove t) ⟩
@@ -57,7 +57,7 @@ sum-remove {suc n} {suc i}  xs = begin
   t₀ = head xs
   tᵢ = t i
   ∑t = sum t
-  ∑t′ = sum (remove i t)
+  ∑t′ = sum (removeAt t i)
 
 -- The '∑' operator distributes over addition.
 ∑-distrib-+ : ∀ {n} (f g : Vector Carrier n) → ∑[ i < n ] (f i + g i) ≈ ∑[ i < n ] f i + ∑[ i < n ] g i
@@ -93,10 +93,10 @@ sum-permute {suc m} {suc n} f π = begin
   f 0F  + sum f/0                          ≡˘⟨ P.cong (_+ sum f/0) (P.cong f (Perm.inverseʳ π)) ⟩
   πf π₀ + sum f/0                          ≈⟨ +-congˡ (sum-permute f/0 (Perm.remove π₀ π)) ⟩
   πf π₀ + sum (rearrange (π/0 ⟨$⟩ʳ_) f/0)  ≡˘⟨ P.cong (πf π₀ +_) (sum-cong-≗ (P.cong f ∘ Perm.punchIn-permute′ π 0F)) ⟩
-  πf π₀ + sum (remove π₀ πf)               ≈⟨ sym (sum-remove πf) ⟩
+  πf π₀ + sum (removeAt πf π₀)             ≈⟨ sym (sum-remove πf) ⟩
   sum πf                                   ∎
   where
-  f/0 = remove 0F f
+  f/0 = removeAt f 0F
   π₀ = π ⟨$⟩ˡ 0F
   π/0 = Perm.remove π₀ π
   πf = rearrange (π ⟨$⟩ʳ_) f
diff --git a/src/Algebra/Properties/Semiring/Binomial.agda b/src/Algebra/Properties/Semiring/Binomial.agda
index b4d5ef81db..122da9fcb9 100644
--- a/src/Algebra/Properties/Semiring/Binomial.agda
+++ b/src/Algebra/Properties/Semiring/Binomial.agda
@@ -71,7 +71,7 @@ sum₂ n = ∑[ k ≤ suc n ] term₂ n k
 ------------------------------------------------------------------------
 -- Properties
 
-term₂[n,n+1]≈0# : ∀ n → term₂ n (fromℕ (suc n)) ≈ 0# 
+term₂[n,n+1]≈0# : ∀ n → term₂ n (fromℕ (suc n)) ≈ 0#
 term₂[n,n+1]≈0# n rewrite view-fromℕ (suc n) = refl
 
 lemma₁ : ∀ n → x * binomialExpansion n ≈ sum₁ n
@@ -117,7 +117,7 @@ x*lemma {n} i = begin
 ------------------------------------------------------------------------
 -- Next, a lemma which does require commutativity
 
-y*lemma : x * y ≈ y * x → ∀ {n : ℕ} (j : Fin n) → 
+y*lemma : x * y ≈ y * x → ∀ {n : ℕ} (j : Fin n) →
           y * binomialTerm n (suc j) ≈ (n C toℕ (suc j)) × binomial (suc n) (suc (inject₁ j))
 y*lemma x*y≈y*x {n} j = begin
   y * binomialTerm n (suc j)
diff --git a/src/Data/List/Base.agda b/src/Data/List/Base.agda
index 9817cf8648..b96a0451cc 100644
--- a/src/Data/List/Base.agda
+++ b/src/Data/List/Base.agda
@@ -196,6 +196,14 @@ tails : List A → List (List A)
 tails []       = [] ∷ []
 tails (x ∷ xs) = (x ∷ xs) ∷ tails xs
 
+insertAt : (xs : List A) → Fin (suc (length xs)) → A → List A
+insertAt xs       zero    v = v ∷ xs
+insertAt (x ∷ xs) (suc i) v = x ∷ insertAt xs i v
+
+updateAt : (xs : List A) → Fin (length xs) → (A → A) → List A
+updateAt (x ∷ xs) zero    f = f x ∷ xs
+updateAt (x ∷ xs) (suc i) f = x ∷ updateAt xs i f
+
 -- Scans
 
 scanr : (A → B → B) → B → List A → List B
@@ -330,6 +338,10 @@ splitAt zero    xs       = ([] , xs)
 splitAt (suc n) []       = ([] , [])
 splitAt (suc n) (x ∷ xs) = Prod.map₁ (x ∷_) (splitAt n xs)
 
+removeAt : (xs : List A) → Fin (length xs) → List A
+removeAt (x ∷ xs) zero     = xs
+removeAt (x ∷ xs) (suc i)  = x ∷ removeAt xs i
+
 -- The following are functions which split a list up using boolean
 -- predicates. However, in practice they are difficult to use and
 -- prove properties about, and are mainly provided for advanced use
@@ -469,19 +481,18 @@ findIndices P? = findIndicesᵇ (does ∘ P?)
 ------------------------------------------------------------------------
 -- Actions on single elements
 
-infixl 5 _[_]%=_ _[_]∷=_ _─_
+infixl 5 _[_]%=_ _[_]∷=_
+
+-- xs [ i ]%= f  modifies the i-th element of xs according to f
 
 _[_]%=_ : (xs : List A) → Fin (length xs) → (A → A) → List A
-(x ∷ xs) [ zero  ]%= f = f x ∷ xs
-(x ∷ xs) [ suc k ]%= f = x ∷ (xs [ k ]%= f)
+xs [ i ]%= f = updateAt xs i f
+
+-- xs [ i ]≔ y  overwrites the i-th element of xs with y
 
 _[_]∷=_ : (xs : List A) → Fin (length xs) → A → List A
 xs [ k ]∷= v = xs [ k ]%= const v
 
-_─_ : (xs : List A) → Fin (length xs) → List A
-(x ∷ xs) ─ zero  = xs
-(x ∷ xs) ─ suc k = x ∷ (xs ─ k)
-
 ------------------------------------------------------------------------
 -- Conditional versions of cons and snoc
 
@@ -527,3 +538,12 @@ _∷ʳ'_ = InitLast._∷ʳ′_
 "Warning: _∷ʳ'_ (ending in an apostrophe) was deprecated in v1.4.
 Please use _∷ʳ′_ (ending in a prime) instead."
 #-}
+
+-- Version 2.0
+
+infixl 5 _─_
+_─_ = removeAt
+{-# WARNING_ON_USAGE _─_
+"Warning: _─_ was deprecated in v2.0.
+Please use removeAt instead."
+#-}
diff --git a/src/Data/List/Properties.agda b/src/Data/List/Properties.agda
index eb403f8b91..48f533f08d 100644
--- a/src/Data/List/Properties.agda
+++ b/src/Data/List/Properties.agda
@@ -746,17 +746,41 @@ map-∷= (x ∷ xs) zero    v f = refl
 map-∷= (x ∷ xs) (suc k) v f = cong (f x ∷_) (map-∷= xs k v f)
 
 ------------------------------------------------------------------------
--- _─_
+-- insertAt
 
-length-─ : ∀ (xs : List A) k → length (xs ─ k) ≡ pred (length xs)
-length-─ (x ∷ xs) zero        = refl
-length-─ (x ∷ y ∷ xs) (suc k) = cong suc (length-─ (y ∷ xs) k)
+length-insertAt : ∀ (xs : List A) (i : Fin (suc (length xs))) v →
+                  length (insertAt xs i v) ≡ suc (length xs)
+length-insertAt xs       zero    v = refl
+length-insertAt (x ∷ xs) (suc i) v = cong suc (length-insertAt xs i v)
 
-map-─ : ∀ xs k (f : A → B) →
-        let eq = sym (length-map f xs) in
-        map f (xs ─ k) ≡ map f xs ─ cast eq k
-map-─ (x ∷ xs) zero    f = refl
-map-─ (x ∷ xs) (suc k) f = cong (f x ∷_) (map-─ xs k f)
+------------------------------------------------------------------------
+-- removeAt
+
+length-removeAt : ∀ (xs : List A) k → length (removeAt xs k) ≡ pred (length xs)
+length-removeAt (x ∷ xs) zero            = refl
+length-removeAt (x ∷ xs@(_ ∷ _)) (suc k) = cong suc (length-removeAt xs k)
+
+length-removeAt′ : ∀ (xs : List A) k → length xs ≡ suc (length (removeAt xs k))
+length-removeAt′ xs@(_ ∷ _) k rewrite length-removeAt xs k = refl
+
+map-removeAt : ∀ xs k (f : A → B) →
+            let eq = sym (length-map f xs) in
+            map f (removeAt xs k) ≡ removeAt (map f xs) (cast eq k)
+map-removeAt (x ∷ xs) zero    f = refl
+map-removeAt (x ∷ xs) (suc k) f = cong (f x ∷_) (map-removeAt xs k f)
+
+------------------------------------------------------------------------
+ -- insertAt and removeAt
+
+removeAt-insertAt : ∀ (xs : List A) (i : Fin (suc (length xs))) v →
+  removeAt (insertAt xs i v) ((cast (sym (length-insertAt xs i v)) i)) ≡ xs
+removeAt-insertAt xs       zero    v = refl
+removeAt-insertAt (x ∷ xs) (suc i) v = cong (_ ∷_) (removeAt-insertAt xs i v)
+
+insertAt-removeAt : (xs : List A) (i : Fin (length xs)) →
+  insertAt (removeAt xs i) (cast (length-removeAt′ xs i) i) (lookup xs i) ≡ xs
+insertAt-removeAt (x ∷ xs) zero    = refl
+insertAt-removeAt (x ∷ xs) (suc i) = cong (x ∷_) (insertAt-removeAt xs i)
 
 ------------------------------------------------------------------------
 -- take
@@ -1224,3 +1248,15 @@ take++drop = take++drop≡id
 "Warning: take++drop was deprecated in v2.0.
 Please use take++drop≡id instead."
 #-}
+
+length-─ = length-removeAt
+{-# WARNING_ON_USAGE length-─
+"Warning: length-─ was deprecated in v2.0.
+Please use length-removeAt instead."
+#-}
+
+map-─ = map-removeAt
+{-# WARNING_ON_USAGE map-─
+"Warning: map-─ was deprecated in v2.0.
+Please use map-removeAt instead."
+#-}
diff --git a/src/Data/List/Relation/Unary/All/Properties.agda b/src/Data/List/Relation/Unary/All/Properties.agda
index da617af44b..1b55bcd2b8 100644
--- a/src/Data/List/Relation/Unary/All/Properties.agda
+++ b/src/Data/List/Relation/Unary/All/Properties.agda
@@ -13,7 +13,7 @@ open import Data.Bool.Base using (Bool; T; true; false)
 open import Data.Bool.Properties using (T-∧)
 open import Data.Empty
 open import Data.Fin.Base using (Fin; zero; suc)
-open import Data.List.Base as List hiding (lookup)
+open import Data.List.Base as List hiding (lookup; updateAt)
 open import Data.List.Properties as Listₚ using (partition-defn)
 open import Data.List.Membership.Propositional
 open import Data.List.Membership.Propositional.Properties
diff --git a/src/Data/List/Relation/Unary/Any.agda b/src/Data/List/Relation/Unary/Any.agda
index eb010e2a39..169f6020aa 100644
--- a/src/Data/List/Relation/Unary/Any.agda
+++ b/src/Data/List/Relation/Unary/Any.agda
@@ -10,7 +10,7 @@ module Data.List.Relation.Unary.Any where
 
 open import Data.Empty
 open import Data.Fin.Base using (Fin; zero; suc)
-open import Data.List.Base as List using (List; []; [_]; _∷_)
+open import Data.List.Base as List using (List; []; [_]; _∷_; removeAt)
 open import Data.Product.Base as Prod using (∃; _,_)
 open import Data.Sum.Base as Sum using (_⊎_; inj₁; inj₂)
 open import Level using (Level; _⊔_)
@@ -69,7 +69,7 @@ _∷=_ {xs = xs} x∈xs v = xs List.[ index x∈xs ]∷= v
 
 infixl 4 _─_
 _─_ : {P : Pred A p} → ∀ xs → Any P xs → List A
-xs ─ x∈xs = xs List.─ index x∈xs
+xs ─ x∈xs = removeAt xs (index x∈xs)
 
 -- If any element satisfies P, then P is satisfied.
 
diff --git a/src/Data/Vec/Base.agda b/src/Data/Vec/Base.agda
index 507ac05463..469549e1ed 100644
--- a/src/Data/Vec/Base.agda
+++ b/src/Data/Vec/Base.agda
@@ -64,29 +64,27 @@ iterate : (A → A) → A → ∀ {n} → Vec A n
 iterate s z {zero}  = []
 iterate s z {suc n} = z ∷ iterate s (s z)
 
-insert : Vec A n → Fin (suc n) → A → Vec A (suc n)
-insert xs       zero     v = v ∷ xs
-insert (x ∷ xs) (suc i)  v = x ∷ insert xs i v
+insertAt : Vec A n → Fin (suc n) → A → Vec A (suc n)
+insertAt xs       zero     v = v ∷ xs
+insertAt (x ∷ xs) (suc i)  v = x ∷ insertAt xs i v
 
-remove : Vec A (suc n) → Fin (suc n) → Vec A n
-remove (_ ∷ xs)     zero     = xs
-remove (x ∷ y ∷ xs) (suc i)  = x ∷ remove (y ∷ xs) i
+removeAt : Vec A (suc n) → Fin (suc n) → Vec A n
+removeAt (x ∷ xs)         zero    = xs
+removeAt (x ∷ xs@(_ ∷ _)) (suc i) = x ∷ removeAt xs i
 
-updateAt : Fin n → (A → A) → Vec A n → Vec A n
-updateAt zero    f (x ∷ xs) = f x ∷ xs
-updateAt (suc i) f (x ∷ xs) = x   ∷ updateAt i f xs
+updateAt : Vec A n → Fin n → (A → A) → Vec A n
+updateAt (x ∷ xs) zero    f = f x ∷ xs
+updateAt (x ∷ xs) (suc i) f = x   ∷ updateAt xs i f
 
 -- xs [ i ]%= f  modifies the i-th element of xs according to f
 
-infixl 6 _[_]%=_
+infixl 6 _[_]%=_ _[_]≔_
 
 _[_]%=_ : Vec A n → Fin n → (A → A) → Vec A n
-xs [ i ]%= f = updateAt i f xs
+xs [ i ]%= f = updateAt xs i f
 
 -- xs [ i ]≔ y  overwrites the i-th element of xs with y
 
-infixl 6 _[_]≔_
-
 _[_]≔_ : Vec A n → Fin n → A → Vec A n
 xs [ i ]≔ y = xs [ i ]%= const y
 
@@ -353,3 +351,21 @@ transpose : Vec (Vec A n) m → Vec (Vec A m) n
 transpose []         = replicate []
 transpose (as ∷ ass) = replicate _∷_ ⊛ as ⊛ transpose ass
 
+------------------------------------------------------------------------
+-- DEPRECATED
+------------------------------------------------------------------------
+-- Please use the new names as continuing support for the old names is
+-- not guaranteed.
+
+-- Version 2.0
+
+remove = removeAt
+{-# WARNING_ON_USAGE remove
+"Warning: remove was deprecated in v2.0.
+Please use removeAt instead."
+#-}
+insert = insertAt
+{-# WARNING_ON_USAGE insert
+"Warning: insert was deprecated in v2.0.
+Please use insertAt instead."
+#-}
diff --git a/src/Data/Vec/Functional.agda b/src/Data/Vec/Functional.agda
index 091886bef5..7b217a415b 100644
--- a/src/Data/Vec/Functional.agda
+++ b/src/Data/Vec/Functional.agda
@@ -31,9 +31,8 @@ infixl 1 _>>=_
 private
   variable
     a b c : Level
-    A : Set a
-    B : Set b
-    C : Set c
+    A B C : Set a
+    m n : ℕ
 
 ------------------------------------------------------------------------
 -- Definition
@@ -44,13 +43,13 @@ Vector A n = Fin n → A
 ------------------------------------------------------------------------
 -- Conversion
 
-toVec : ∀ {n} → Vector A n → Vec A n
+toVec : Vector A n → Vec A n
 toVec = V.tabulate
 
-fromVec : ∀ {n} → Vec A n → Vector A n
+fromVec : Vec A n → Vector A n
 fromVec = V.lookup
 
-toList : ∀ {n} → Vector A n → List A
+toList : Vector A n → List A
 toList = L.tabulate
 
 fromList : ∀ (xs : List A) → Vector A (L.length xs)
@@ -62,39 +61,39 @@ fromList = L.lookup
 [] : Vector A zero
 [] ()
 
-_∷_ : ∀ {n} → A → Vector A n → Vector A (suc 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 : Vector A n → ℕ
 length {n = n} _ = n
 
-head : ∀ {n} → Vector A (suc n) → A
+head : Vector A (suc n) → A
 head xs = xs zero
 
-tail : ∀ {n} → Vector A (suc n) → Vector A n
+tail : Vector A (suc n) → Vector A n
 tail xs = xs ∘ suc
 
-uncons : ∀ {n} → Vector A (suc n) → A × Vector A n
+uncons : Vector A (suc n) → A × Vector A n
 uncons xs = head xs , tail xs
 
-replicate : ∀ {n} → A → Vector A n
+replicate : 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
+insertAt : Vector A n → Fin (suc n) → A → Vector A (suc n)
+insertAt {n = n}     xs zero    v zero    = v
+insertAt {n = n}     xs zero    v (suc j) = xs j
+insertAt {n = suc n} xs (suc i) v zero    = head xs
+insertAt {n = suc n} xs (suc i) v (suc j) = insertAt (tail xs) i v j
 
-remove : ∀ {n} → Fin (suc n) → Vector A (suc n) → Vector A n
-remove i t = t ∘ punchIn i
+removeAt : Vector A (suc n) → Fin (suc n) → Vector A n
+removeAt t i = 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
+updateAt : Vector A n → Fin n → (A → A) → Vector A n
+updateAt {n = suc n} xs zero    f zero    = f (head xs)
+updateAt {n = suc n} xs zero    f (suc j) = xs (suc j)
+updateAt {n = suc n} xs (suc i) f zero    = head xs
+updateAt {n = suc n} xs (suc i) f (suc j) = updateAt (tail xs) i f j
 
 ------------------------------------------------------------------------
 -- Transformations
@@ -102,10 +101,10 @@ updateAt {n = suc n} (suc i) f xs (suc j) = updateAt i f (tail xs) j
 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)
+_++_ : 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 : 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
@@ -116,25 +115,25 @@ 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 : (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
+_⊛_ : Vector (A → B) n → Vector A n → Vector B n
 _⊛_ = _ˢ_
 
-_>>=_ : ∀ {m n} → Vector A m → (A → Vector B n) → Vector B (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 : (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 : 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 : Vector (A × B) n → Vector A n × Vector B n
 unzip = unzipWith id
 
 take : ∀ m {n} → Vector A (m ℕ.+ n) → Vector A m
@@ -143,14 +142,35 @@ take _ {n = n} xs = xs ∘ (_↑ˡ n)
 drop : ∀ m {n} → Vector A (m ℕ.+ n) → Vector A n
 drop m xs = xs ∘ (m ↑ʳ_)
 
-reverse : ∀ {n} → Vector A n → Vector A n
+reverse : Vector A n → Vector A n
 reverse xs = xs ∘ opposite
 
-init : ∀ {n} → Vector A (suc n) → Vector A n
+init : Vector A (suc n) → Vector A n
 init xs = xs ∘ inject₁
 
-last : ∀ {n} → Vector A (suc n) → A
+last : 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 : Vector (Vector A n) m → Vector (Vector A m) n
 transpose = flip
+
+------------------------------------------------------------------------
+-- DEPRECATED
+------------------------------------------------------------------------
+-- Please use the new names as continuing support for the old names is
+-- not guaranteed.
+
+-- Version 2.0
+
+remove : Fin (suc n) → Vector A (suc n) → Vector A n
+remove = flip removeAt
+{-# WARNING_ON_USAGE remove
+"Warning: remove was deprecated in v2.0.
+Please use removeAt instead.
+NOTE: argument order has been flipped."
+#-}
+insert = insertAt
+{-# WARNING_ON_USAGE insert
+"Warning: insert was deprecated in v2.0.
+Please use insertAt instead."
+#-}
diff --git a/src/Data/Vec/Functional/Properties.agda b/src/Data/Vec/Functional/Properties.agda
index f3314754e0..93f95b423b 100644
--- a/src/Data/Vec/Functional/Properties.agda
+++ b/src/Data/Vec/Functional/Properties.agda
@@ -31,13 +31,12 @@ import Data.Fin.Properties as Finₚ
 private
   variable
     a b c : Level
-    A : Set a
-    B : Set b
-    C : Set c
+    A B C : Set a
+    m n : ℕ
 
 ------------------------------------------------------------------------
 
-module _ {n} {xs ys : Vector A (suc n)} where
+module _ {xs ys : Vector A (suc n)} where
 
   ∷-cong : head xs ≡ head ys → tail xs ≗ tail ys → xs ≗ ys
   ∷-cong eq _ zero    = eq
@@ -46,10 +45,9 @@ module _ {n} {xs ys : Vector A (suc n)} where
   ∷-injective : xs ≗ ys → head xs ≡ head ys × tail xs ≗ tail ys
   ∷-injective eq = eq zero , eq ∘ suc
 
-≗-dec : DecidableEquality A →
-        ∀ {n} → Decidable {A = Vector A n} _≗_
-≗-dec _≟_ {zero}  xs ys = yes λ ()
-≗-dec _≟_ {suc n} xs ys =
+≗-dec : DecidableEquality A → Decidable {A = Vector A n} _≗_
+≗-dec {n = zero}  _≟_ xs ys = yes λ ()
+≗-dec {n = suc n} _≟_ xs ys =
   map′ (Product.uncurry ∷-cong) ∷-injective
        (head xs ≟ head ys ×-dec ≗-dec _≟_ (tail xs) (tail ys))
 
@@ -58,15 +56,15 @@ module _ {n} {xs ys : Vector A (suc n)} where
 
 -- (+) 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 : ∀ (i : Fin n) {f : A → A} (xs : Vector A n) →
+                   updateAt xs i f 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 : ∀ (i j : Fin n) {f : A → A} (xs : Vector A n) →
+                   i ≢ j → updateAt xs j f 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
@@ -74,46 +72,46 @@ updateAt-minimal (suc i) (suc j) xs i≢j = updateAt-minimal i j (tail xs) (i≢
 
 -- updateAt i is a monoid morphism from A → A to Vector A n → Vector A n.
 
-updateAt-id-local : ∀ {n} (i : Fin n) {f : A → A} (xs : Vector A n) →
+updateAt-id-local : ∀ (i : Fin n) {f : A → A} (xs : Vector A n) →
                     f (xs i) ≡ xs i →
-                    updateAt i f xs ≗ xs
+                    updateAt xs i f ≗ xs
 updateAt-id-local zero    xs eq zero    = eq
 updateAt-id-local zero    xs eq (suc j) = refl
 updateAt-id-local (suc i) xs eq zero    = refl
 updateAt-id-local (suc i) xs eq (suc j) = updateAt-id-local i (tail xs) eq j
 
-updateAt-id : ∀ {n} (i : Fin n) (xs : Vector A n) →
-              updateAt i id xs ≗ xs
+updateAt-id : ∀ (i : Fin n) (xs : Vector A n) →
+              updateAt xs i id ≗ xs
 updateAt-id i xs = updateAt-id-local i xs refl
 
-updateAt-∘-local : ∀ {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-∘-local zero    xs eq zero    = eq
-updateAt-∘-local zero    xs eq (suc j) = refl
-updateAt-∘-local (suc i) xs eq zero    = refl
-updateAt-∘-local (suc i) xs eq (suc j) = updateAt-∘-local i (tail xs) eq j
+updateAt-updateAt-local : ∀ (i : Fin n) {f g h : A → A} (xs : Vector A n) →
+                          f (g (xs i)) ≡ h (xs i) →
+                          updateAt (updateAt xs i g) i f ≗ updateAt xs i h
+updateAt-updateAt-local zero    xs eq zero    = eq
+updateAt-updateAt-local zero    xs eq (suc j) = refl
+updateAt-updateAt-local (suc i) xs eq zero    = refl
+updateAt-updateAt-local (suc i) xs eq (suc j) = updateAt-updateAt-local i (tail xs) eq j
 
-updateAt-∘ : ∀ {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-∘ i xs = updateAt-∘-local i xs refl
+updateAt-updateAt : ∀ (i : Fin n) {f g : A → A} (xs : Vector A n) →
+                    updateAt (updateAt xs i g) i f ≗ updateAt xs i (f ∘ g)
+updateAt-updateAt i xs = updateAt-updateAt-local i xs refl
 
-updateAt-cong-local : ∀ {n} (i : Fin n) {f g : A → A} (xs : Vector A n) →
+updateAt-cong-local : ∀ (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 xs i f ≗ updateAt xs i g
 updateAt-cong-local zero    xs eq zero    = eq
 updateAt-cong-local zero    xs eq (suc j) = refl
 updateAt-cong-local (suc i) xs eq zero    = refl
 updateAt-cong-local (suc i) xs eq (suc j) = updateAt-cong-local 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 : ∀ (i : Fin n) {f g : A → A} → f ≗ g → (xs : Vector A n) →
+                updateAt xs i f ≗ updateAt xs i g
 updateAt-cong i eq xs = updateAt-cong-local i xs (eq (xs i))
 
 -- 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 : ∀ (i j : Fin n) {f g : A → A} → i ≢ j → (xs : Vector A n) →
+                    updateAt (updateAt xs j g) i f ≗ updateAt (updateAt xs i f) j g
 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
@@ -125,59 +123,59 @@ updateAt-commutes (suc i) (suc j) i≢j xs (suc k) = updateAt-commutes i j (i≢
 ------------------------------------------------------------------------
 -- map
 
-map-id : ∀ {n} → (xs : Vector A n) → map id xs ≗ xs
+map-id : (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 : 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-∘ : ∀ {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) →
+lookup-map : ∀ (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-local : ∀ {n} {f : A → B} {g : A → A} {h : B → B}
+map-updateAt-local : ∀ {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 f (updateAt xs i g) ≗ updateAt (map f xs) i h
 map-updateAt-local {n = suc n}       {f = f} xs zero    eq zero    = eq
 map-updateAt-local {n = suc n}       {f = f} xs zero    eq (suc j) = refl
 map-updateAt-local {n = suc (suc n)} {f = f} xs (suc i) eq zero    = refl
 map-updateAt-local {n = suc (suc n)} {f = f} xs (suc i) eq (suc j) = map-updateAt-local {f = f} (tail xs) i eq j
 
-map-updateAt : ∀ {n} {f : A → B} {g : A → A} {h : B → B} →
+map-updateAt : ∀ {f : A → B} {g : A → A} {h : B → B} →
                f ∘ g ≗ h ∘ f →
                (xs : Vector A n) (i : Fin n) →
-               map f (updateAt i g xs) ≗ updateAt i h (map f xs)
+               map f (updateAt xs i g) ≗ updateAt (map f xs) i h
 map-updateAt {f = f} {g = g} f∘g≗h∘f xs i = map-updateAt-local {f = f} {g = g} xs i (f∘g≗h∘f (xs i))
 
 ------------------------------------------------------------------------
 -- _++_
 
-lookup-++-< : ∀ {m n} (xs : Vector A m) (ys : Vector A n) →
+lookup-++-< : ∀ (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) →
+lookup-++-≥ : ∀ (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 →
+lookup-++ˡ : ∀ (xs : Vector A m) (ys : Vector A n) i →
              (xs ++ ys) (i ↑ˡ n) ≡ xs i
 lookup-++ˡ {m = m} {n = n} xs ys i = cong Sum.[ xs , ys ] (Finₚ.splitAt-↑ˡ m i n)
 
-lookup-++ʳ : ∀ {m n} (xs : Vector A m) (ys : Vector A n) i →
+lookup-++ʳ : ∀ (xs : Vector A m) (ys : Vector A n) i →
              (xs ++ ys) (m ↑ʳ i) ≡ ys i
 lookup-++ʳ {m = m} {n = n} xs ys i = cong Sum.[ xs , ys ] (Finₚ.splitAt-↑ʳ m n i)
 
-module _ {m} {ys ys′ : Vector A m} where
+module _ {ys ys′ : Vector A m} where
 
-  ++-cong : ∀ {n} (xs xs′ : Vector A n) →
+  ++-cong : ∀ (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
@@ -193,7 +191,7 @@ module _ {m} {ys ys′ : Vector A m} where
     (xs′ ++ ys′) i             ∎
     where open ≡-Reasoning
 
-  ++-injectiveˡ : ∀ {n} (xs xs′ : Vector A n) →
+  ++-injectiveˡ : ∀ (xs xs′ : Vector A n) →
                   xs ++ ys ≗ xs′ ++ ys′ → xs ≗ xs′
   ++-injectiveˡ xs xs′ eq i = begin
     xs i                   ≡˘⟨ lookup-++ˡ xs ys i ⟩
@@ -202,8 +200,7 @@ module _ {m} {ys ys′ : Vector A m} where
     xs′ i                  ∎
     where open ≡-Reasoning
 
-  ++-injectiveʳ : ∀ {n} (xs xs′ : Vector A n) →
-                  xs ++ ys ≗ xs′ ++ ys′ → ys ≗ ys′
+  ++-injectiveʳ : ∀ (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) (n ↑ʳ i)    ≡⟨ eq (n ↑ʳ i)   ⟩
@@ -211,56 +208,56 @@ module _ {m} {ys ys′ : Vector A m} where
     ys′ i                  ∎
     where open ≡-Reasoning
 
-  ++-injective : ∀ {n} (xs xs′ : Vector A n) →
+  ++-injective : ∀ (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
+-- insertAt
 
-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
+insertAt-lookup : ∀ (xs : Vector A n) (i : Fin (suc n)) (v : A) →
+                  insertAt xs i v i ≡ v
+insertAt-lookup {n = n}     xs zero    v = refl
+insertAt-lookup {n = suc n} xs (suc i) v = insertAt-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
+insertAt-punchIn : ∀ (xs : Vector A n) (i : Fin (suc n)) (v : A)
+                   (j : Fin n) →
+                   insertAt xs i v (punchIn i j) ≡ xs j
+insertAt-punchIn {n = suc n} xs zero    v j       = refl
+insertAt-punchIn {n = suc n} xs (suc i) v zero    = refl
+insertAt-punchIn {n = suc n} xs (suc i) v (suc j) = insertAt-punchIn (tail xs) i v j
 
 ------------------------------------------------------------------------
--- remove
+-- removeAt
 
-remove-punchOut : ∀ {n} (xs : Vector A (suc n))
+removeAt-punchOut : ∀ (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
+                  removeAt xs i (punchOut i≢j) ≡ xs j
+removeAt-punchOut {n = n}     xs {zero}  {zero}  i≢j = ⊥-elim (i≢j refl)
+removeAt-punchOut {n = suc n} xs {zero}  {suc j} i≢j = refl
+removeAt-punchOut {n = suc n} xs {suc i} {zero}  i≢j = refl
+removeAt-punchOut {n = suc n} xs {suc i} {suc j} i≢j = removeAt-punchOut (tail xs) (i≢j ∘ cong suc)
+
+removeAt-insertAt : ∀ (xs : Vector A n) (i : Fin (suc n)) (v : A) →
+                    removeAt (insertAt xs i v) i ≗ xs
+removeAt-insertAt xs zero    v j       = refl
+removeAt-insertAt xs (suc i) v zero    = refl
+removeAt-insertAt xs (suc i) v (suc j) = removeAt-insertAt (tail xs) i v j
+
+insertAt-removeAt : ∀ (xs : Vector A (suc n)) (i : Fin (suc n)) →
+                    insertAt (removeAt xs i) i (xs i) ≗ xs
+insertAt-removeAt {n = n}     xs zero    zero    = refl
+insertAt-removeAt {n = n}     xs zero    (suc j) = refl
+insertAt-removeAt {n = suc n} xs (suc i) zero    = refl
+insertAt-removeAt {n = suc n} xs (suc i) (suc j) = insertAt-removeAt (tail xs) i j
 
 ------------------------------------------------------------------------
 -- Conversion functions
 
-toVec∘fromVec : ∀ {n} → (xs : Vec A n) → toVec (fromVec xs) ≡ xs
+toVec∘fromVec : (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 : (xs : Vector A n) → fromVec (toVec xs) ≗ xs
 fromVec∘toVec = Vₚ.lookup∘tabulate
 
 toList∘fromList : (xs : List A) → toList (fromList xs) ≡ xs
@@ -279,21 +276,44 @@ updateAt-id-relative = updateAt-id-local
 "Warning: updateAt-id-relative was deprecated in v2.0.
 Please use updateAt-id-local instead."
 #-}
-
-updateAt-compose-relative = updateAt-∘-local
+updateAt-compose-relative = updateAt-updateAt-local
 {-# WARNING_ON_USAGE updateAt-compose-relative
 "Warning: updateAt-compose-relative was deprecated in v2.0.
-Please use updateAt-∘-local instead."
+Please use updateAt-updateAt-local instead."
 #-}
-
-updateAt-compose = updateAt-∘
+updateAt-compose = updateAt-updateAt
 {-# WARNING_ON_USAGE updateAt-compose
 "Warning: updateAt-compose was deprecated in v2.0.
-Please use updateAt-∘ instead."
+Please use updateAt-updateAt instead."
 #-}
-
 updateAt-cong-relative = updateAt-cong-local
 {-# WARNING_ON_USAGE updateAt-cong-relative
 "Warning: updateAt-cong-relative was deprecated in v2.0.
 Please use updateAt-cong-local instead."
 #-}
+
+insert-lookup = insertAt-lookup
+{-# WARNING_ON_USAGE insert-lookup
+"Warning: insert-lookup was deprecated in v2.0.
+Please use insertAt-lookup instead."
+#-}
+insert-punchIn = insertAt-punchIn
+{-# WARNING_ON_USAGE insert-punchIn
+"Warning: insert-punchIn was deprecated in v2.0.
+Please use insertAt-punchIn instead."
+#-}
+remove-punchOut = removeAt-punchOut
+{-# WARNING_ON_USAGE remove-punchOut
+"Warning: remove-punchOut was deprecated in v2.0.
+Please use removeAt-punchOut instead."
+#-}
+remove-insert = removeAt-insertAt
+{-# WARNING_ON_USAGE remove-insert
+"Warning: remove-insert was deprecated in v2.0.
+Please use removeAt-insertAt instead."
+#-}
+insert-remove = insertAt-removeAt
+{-# WARNING_ON_USAGE insert-remove
+"Warning: insert-remove was deprecated in v2.0.
+Please use insertAt-removeAt instead."
+#-}
diff --git a/src/Data/Vec/Properties.agda b/src/Data/Vec/Properties.agda
index c5b92ec2a1..3d0e3bf590 100644
--- a/src/Data/Vec/Properties.agda
+++ b/src/Data/Vec/Properties.agda
@@ -51,7 +51,7 @@ private
 ∷-injectiveʳ : x ∷ xs ≡ y ∷ ys → xs ≡ ys
 ∷-injectiveʳ refl = refl
 
-∷-injective : (x ∷ xs) ≡ (y ∷ ys) → x ≡ y × xs ≡ ys
+∷-injective : x ∷ xs ≡ y ∷ ys → x ≡ y × xs ≡ ys
 ∷-injective refl = refl , refl
 
 ≡-dec : DecidableEquality A → DecidableEquality (Vec A n)
@@ -205,14 +205,14 @@ lookup-take-inject≤ {m = m} {n = n} xs i = begin
 -- (+) updateAt i actually updates the element at index i.
 
 updateAt-updates : ∀ (i : Fin n) {f : A → A} (xs : Vec A n) →
-                   xs [ i ]= x → (updateAt i f xs) [ i ]= f x
+                   xs [ i ]= x → (updateAt xs i f) [ i ]= f x
 updateAt-updates zero    (x ∷ xs) here        = here
 updateAt-updates (suc i) (x ∷ xs) (there loc) = there (updateAt-updates i xs loc)
 
 -- (-) updateAt i does not touch the elements at other indices.
 
 updateAt-minimal : ∀ (i j : Fin n) {f : A → A} (xs : Vec A n) →
-                   i ≢ j → xs [ i ]= x → (updateAt j f xs) [ i ]= x
+                   i ≢ j → xs [ i ]= x → (updateAt xs j f) [ i ]= x
 updateAt-minimal zero    zero    (x ∷ xs) 0≢0 here        = contradiction refl 0≢0
 updateAt-minimal zero    (suc j) (x ∷ xs) _   here        = here
 updateAt-minimal (suc i) zero    (x ∷ xs) _   (there loc) = there loc
@@ -235,29 +235,29 @@ updateAt-minimal (suc i) (suc j) (x ∷ xs) i≢j (there loc) =
 
 updateAt-id-local : ∀ (i : Fin n) {f : A → A} (xs : Vec A n) →
                     f (lookup xs i) ≡ lookup xs i →
-                    updateAt i f xs ≡ xs
+                    updateAt xs i f ≡ xs
 updateAt-id-local zero    (x ∷ xs) eq = cong (_∷ xs) eq
 updateAt-id-local (suc i) (x ∷ xs) eq = cong (x ∷_) (updateAt-id-local i xs eq)
 
 -- 1b. identity:  updateAt i id ≗ id
 
-updateAt-id : ∀ (i : Fin n) (xs : Vec A n) → updateAt i id xs ≡ xs
+updateAt-id : ∀ (i : Fin n) (xs : Vec A n) → updateAt xs i id ≡ xs
 updateAt-id i xs = updateAt-id-local i xs refl
 
 -- 2a. local composition:  f ∘ g = h ↾ (lookup xs i)
 --                implies  updateAt i f ∘ updateAt i g = updateAt i h ↾ xs
 
-updateAt-∘-local : ∀ (i : Fin n) {f g h : A → A} (xs : Vec A n) →
-                         f (g (lookup xs i)) ≡ h (lookup xs i) →
-                         updateAt i f (updateAt i g xs) ≡ updateAt i h xs
-updateAt-∘-local zero    (x ∷ xs) fg=h = cong (_∷ xs) fg=h
-updateAt-∘-local (suc i) (x ∷ xs) fg=h = cong (x ∷_) (updateAt-∘-local i xs fg=h)
+updateAt-updateAt-local : ∀ (i : Fin n) {f g h : A → A} (xs : Vec A n) →
+                          f (g (lookup xs i)) ≡ h (lookup xs i) →
+                          updateAt (updateAt xs i g) i f ≡ updateAt xs i h
+updateAt-updateAt-local zero    (x ∷ xs) fg=h = cong (_∷ xs) fg=h
+updateAt-updateAt-local (suc i) (x ∷ xs) fg=h = cong (x ∷_) (updateAt-updateAt-local i xs fg=h)
 
 -- 2b. composition:  updateAt i f ∘ updateAt i g ≗ updateAt i (f ∘ g)
 
-updateAt-∘ : ∀ (i : Fin n) {f g : A → A} →
-                   updateAt i f ∘ updateAt i g ≗ updateAt i (f ∘ g)
-updateAt-∘ i xs = updateAt-∘-local i xs refl
+updateAt-updateAt : ∀ (i : Fin n) {f g : A → A} (xs : Vec A n) →
+                    updateAt (updateAt xs i g) i f ≡ updateAt xs i (f ∘ g)
+updateAt-updateAt i xs = updateAt-updateAt-local i xs refl
 
 -- 3. congruence:  updateAt i  is a congruence wrt. extensional equality.
 
@@ -266,14 +266,14 @@ updateAt-∘ i xs = updateAt-∘-local i xs refl
 
 updateAt-cong-local : ∀ (i : Fin n) {f g : A → A} (xs : Vec A n) →
                       f (lookup xs i) ≡ g (lookup xs i) →
-                      updateAt i f xs ≡ updateAt i g xs
+                      updateAt xs i f ≡ updateAt xs i g
 updateAt-cong-local zero    (x ∷ xs) f=g = cong (_∷ xs) f=g
 updateAt-cong-local (suc i) (x ∷ xs) f=g = cong (x ∷_) (updateAt-cong-local i xs f=g)
 
 -- 3b. congruence:  f ≗ g → updateAt i f ≗ updateAt i g
 
-updateAt-cong : ∀ (i : Fin n) {f g : A → A} →
-                f ≗ g → updateAt i f ≗ updateAt i g
+updateAt-cong : ∀ (i : Fin n) {f g : A → A} → f ≗ g → (xs : Vec A n) →
+                updateAt xs i f ≡ updateAt xs i g
 updateAt-cong i f≗g xs = updateAt-cong-local i xs (f≗g (lookup xs i))
 
 -- The order of updates at different indices i ≢ j does not matter.
@@ -281,13 +281,13 @@ updateAt-cong i f≗g xs = updateAt-cong-local i xs (f≗g (lookup xs i))
 -- This a consequence of updateAt-updates and updateAt-minimal
 -- but easier to prove inductively.
 
-updateAt-commutes : ∀ (i j : Fin n) {f g : A → A} → i ≢ j →
-                    updateAt i f ∘ updateAt j g ≗ updateAt j g ∘ updateAt i f
+updateAt-commutes : ∀ (i j : Fin n) {f g : A → A} → i ≢ j → (xs : Vec A n) →
+                    updateAt (updateAt xs j g) i f ≡ updateAt (updateAt xs i f) j g
 updateAt-commutes zero    zero    0≢0 (x ∷ xs) = contradiction refl 0≢0
 updateAt-commutes zero    (suc j) i≢j (x ∷ xs) = refl
 updateAt-commutes (suc i) zero    i≢j (x ∷ xs) = refl
 updateAt-commutes (suc i) (suc j) i≢j (x ∷ xs) =
-  cong (x ∷_) (updateAt-commutes i j (i≢j ∘ cong suc) xs)
+   cong (x ∷_) (updateAt-commutes i j (i≢j ∘ cong suc) xs)
 
 -- lookup after updateAt reduces.
 
@@ -295,14 +295,14 @@ updateAt-commutes (suc i) (suc j) i≢j (x ∷ xs) =
 -- using []=↔lookup.
 
 lookup∘updateAt : ∀ (i : Fin n) {f : A → A} xs →
-                  lookup (updateAt i f xs) i ≡ f (lookup xs i)
+                  lookup (updateAt xs i f) i ≡ f (lookup xs i)
 lookup∘updateAt i xs =
   []=⇒lookup (updateAt-updates i xs (lookup⇒[]= i _ refl))
 
 -- For different indices it easily follows from updateAt-minimal.
 
 lookup∘updateAt′ : ∀ (i j : Fin n) {f : A → A} → i ≢ j → ∀ xs →
-                   lookup (updateAt j f xs) i ≡ lookup xs i
+                   lookup (updateAt xs j f) i ≡ lookup xs i
 lookup∘updateAt′ i j xs i≢j =
   []=⇒lookup (updateAt-minimal i j i≢j xs (lookup⇒[]= i _ refl))
 
@@ -312,10 +312,10 @@ lookup∘updateAt′ i j xs i≢j =
 []%=-id xs i = updateAt-id i xs
 
 []%=-∘ : ∀ (xs : Vec A n) (i : Fin n) {f g : A → A} →
-     xs [ i ]%= f
-        [ i ]%= g
-   ≡ xs [ i ]%= g ∘ f
-[]%=-∘ xs i = updateAt-∘ i xs
+      xs [ i ]%= f
+         [ i ]%= g
+    ≡ xs [ i ]%= g ∘ f
+[]%=-∘ xs i = updateAt-updateAt i xs
 
 
 ------------------------------------------------------------------------
@@ -325,11 +325,11 @@ lookup∘updateAt′ i j xs i≢j =
 -- are special cases of the ones for updateAt.
 
 []≔-idempotent : ∀ (xs : Vec A n) (i : Fin n) →
-                 (xs [ i ]≔ x) [ i ]≔ y ≡ xs [ i ]≔ y
-[]≔-idempotent xs i = updateAt-∘ i xs
+                  (xs [ i ]≔ x) [ i ]≔ y ≡ xs [ i ]≔ y
+[]≔-idempotent xs i = updateAt-updateAt i xs
 
 []≔-commutes : ∀ (xs : Vec A n) (i j : Fin n) → i ≢ j →
-               (xs [ i ]≔ x) [ j ]≔ y ≡ (xs [ j ]≔ y) [ i ]≔ x
+                (xs [ i ]≔ x) [ j ]≔ y ≡ (xs [ j ]≔ y) [ i ]≔ x
 []≔-commutes xs i j i≢j = updateAt-commutes j i (i≢j ∘ sym) xs
 
 []≔-updates : ∀ (xs : Vec A n) (i : Fin n) → (xs [ i ]≔ x) [ i ]= x
@@ -423,15 +423,15 @@ lookup-map (suc i) f (x ∷ xs) = lookup-map i f xs
 map-updateAt : ∀ {f : A → B} {g : A → A} {h : B → B}
                (xs : Vec A n) (i : Fin n) →
                f (g (lookup xs i)) ≡ h (f (lookup xs i)) →
-               map f (updateAt i g xs) ≡ updateAt i h (map f xs)
+               map f (updateAt xs i g) ≡ updateAt (map f xs) i h
 map-updateAt (x ∷ xs) zero    eq = cong (_∷ _) eq
 map-updateAt (x ∷ xs) (suc i) eq = cong (_ ∷_) (map-updateAt xs i eq)
 
-map-insert : ∀ (f : A → B) (x : A) (xs : Vec A n) (i : Fin (suc n)) →
-             map f (insert xs i x) ≡ insert (map f xs) i (f x)
-map-insert f _ []        zero    = refl
-map-insert f _ (x' ∷ xs) zero    = refl
-map-insert f x (x' ∷ xs) (suc i) = cong (_ ∷_) (map-insert f x xs i)
+map-insertAt : ∀ (f : A → B) (x : A) (xs : Vec A n) (i : Fin (suc n)) →
+             map f (insertAt xs i x) ≡ insertAt (map f xs) i (f x)
+map-insertAt f _ []        Fin.zero = refl
+map-insertAt f _ (x' ∷ xs) Fin.zero = refl
+map-insertAt f x (x' ∷ xs) (Fin.suc i) = cong (_ ∷_) (map-insertAt f x xs i)
 
 map-[]≔ : ∀ (f : A → B) (xs : Vec A n) (i : Fin n) →
           map f (xs [ i ]≔ x) ≡ map f xs [ i ]≔ f x
@@ -1152,42 +1152,57 @@ module _ {P : Pred A p} (P? : Decidable P) where
   ... | false = m≤n⇒m≤1+n (count≤n xs)
 
 ------------------------------------------------------------------------
--- insert
-
-insert-lookup : ∀ (xs : Vec A n) (i : Fin (suc n)) (v : A) →
-                lookup (insert xs i v) i ≡ v
-insert-lookup xs       zero     v = refl
-insert-lookup (x ∷ xs) (suc i)  v = insert-lookup xs i v
-
-insert-punchIn : ∀ (xs : Vec A n) (i : Fin (suc n)) (v : A) (j : Fin n) →
-                 lookup (insert xs i v) (Fin.punchIn i j) ≡ lookup xs j
-insert-punchIn xs       zero     v j       = refl
-insert-punchIn (x ∷ xs) (suc i)  v zero    = refl
-insert-punchIn (x ∷ xs) (suc i)  v (suc j) = insert-punchIn xs i v j
-
-remove-punchOut : ∀ (xs : Vec A (suc n)) {i} {j} (i≢j : i ≢ j) →
-                  lookup (remove xs i) (Fin.punchOut i≢j) ≡ lookup xs j
-remove-punchOut (x ∷ xs)     {zero}  {zero}  i≢j = contradiction refl i≢j
-remove-punchOut (x ∷ xs)     {zero}  {suc j} i≢j = refl
-remove-punchOut (x ∷ y ∷ xs) {suc i} {zero}  i≢j = refl
-remove-punchOut (x ∷ y ∷ xs) {suc i} {suc j} i≢j =
-  remove-punchOut (y ∷ xs) (i≢j ∘ cong suc)
+-- length
+
+length-toList : (xs : Vec A n) → List.length (toList xs) ≡ length xs
+length-toList []       = refl
+length-toList (x ∷ xs) = cong suc (length-toList xs)
+
+------------------------------------------------------------------------
+-- insertAt
+
+insertAt-lookup : ∀ (xs : Vec A n) (i : Fin (suc n)) (v : A) →
+                  lookup (insertAt xs i v) i ≡ v
+insertAt-lookup xs       zero     v = refl
+insertAt-lookup (x ∷ xs) (suc i)  v = insertAt-lookup xs i v
+
+insertAt-punchIn : ∀ (xs : Vec A n) (i : Fin (suc n)) (v : A) (j : Fin n) →
+                   lookup (insertAt xs i v) (Fin.punchIn i j) ≡ lookup xs j
+insertAt-punchIn xs       zero     v j       = refl
+insertAt-punchIn (x ∷ xs) (suc i)  v zero    = refl
+insertAt-punchIn (x ∷ xs) (suc i)  v (suc j) = insertAt-punchIn xs i v j
+
+toList-insertAt : ∀ (xs : Vec A n) (i : Fin (suc n)) (v : A) →
+                  toList (insertAt xs i v) ≡ List.insertAt (toList xs) (Fin.cast (cong suc (sym (length-toList xs))) i) v
+toList-insertAt xs       zero    v = refl
+toList-insertAt (x ∷ xs) (suc i) v = cong (_ List.∷_) (toList-insertAt xs i v)
+
+------------------------------------------------------------------------
+-- removeAt
+
+removeAt-punchOut : ∀ (xs : Vec A (suc n)) {i} {j} (i≢j : i ≢ j) →
+                  lookup (removeAt xs i) (Fin.punchOut i≢j) ≡ lookup xs j
+removeAt-punchOut (x ∷ xs)     {zero}  {zero}  i≢j = contradiction refl i≢j
+removeAt-punchOut (x ∷ xs)     {zero}  {suc j} i≢j = refl
+removeAt-punchOut (x ∷ y ∷ xs) {suc i} {zero}  i≢j = refl
+removeAt-punchOut (x ∷ y ∷ xs) {suc i} {suc j} i≢j =
+  removeAt-punchOut (y ∷ xs) (i≢j ∘ cong suc)
 
 ------------------------------------------------------------------------
--- remove
+-- insertAt and removeAt
 
-remove-insert : ∀ (xs : Vec A n) (i : Fin (suc n)) (v : A) →
-                remove (insert xs i v) i ≡ xs
-remove-insert xs           zero           v = refl
-remove-insert (x ∷ xs)     (suc zero)     v = refl
-remove-insert (x ∷ y ∷ xs) (suc (suc i))  v =
-  cong (x ∷_) (remove-insert (y ∷ xs) (suc i) v)
+removeAt-insertAt : ∀ (xs : Vec A n) (i : Fin (suc n)) (v : A) →
+                    removeAt (insertAt xs i v) i ≡ xs
+removeAt-insertAt xs               zero           v = refl
+removeAt-insertAt (x ∷ xs)         (suc zero)     v = refl
+removeAt-insertAt (x ∷ xs@(_ ∷ _)) (suc (suc i))  v =
+  cong (x ∷_) (removeAt-insertAt xs (suc i) v)
 
-insert-remove : ∀ (xs : Vec A (suc n)) (i : Fin (suc n)) →
-                insert (remove xs i) i (lookup xs i) ≡ xs
-insert-remove (x ∷ xs)     zero     = refl
-insert-remove (x ∷ y ∷ xs) (suc i)  =
-  cong (x ∷_) (insert-remove (y ∷ xs) i)
+insertAt-removeAt : ∀ (xs : Vec A (suc n)) (i : Fin (suc n)) →
+                    insertAt (removeAt xs i) i (lookup xs i) ≡ xs
+insertAt-removeAt (x ∷ xs)         zero     = refl
+insertAt-removeAt (x ∷ xs@(_ ∷ _)) (suc i)  =
+  cong (x ∷_) (insertAt-removeAt xs i)
 
 ------------------------------------------------------------------------
 -- Conversion function
@@ -1234,16 +1249,16 @@ updateAt-id-relative = updateAt-id-local
 Please use updateAt-id-local instead."
 #-}
 
-updateAt-compose-relative = updateAt-∘-local
+updateAt-compose-relative = updateAt-updateAt-local
 {-# WARNING_ON_USAGE updateAt-compose-relative
 "Warning: updateAt-compose-relative was deprecated in v2.0.
-Please use updateAt-∘-local instead."
+Please use updateAt-updateAt-local instead."
 #-}
 
-updateAt-compose = updateAt-∘
+updateAt-compose = updateAt-updateAt
 {-# WARNING_ON_USAGE updateAt-compose
 "Warning: updateAt-compose was deprecated in v2.0.
-Please use updateAt-∘ instead."
+Please use updateAt-updateAt instead."
 #-}
 
 updateAt-cong-relative = updateAt-cong-local
@@ -1300,6 +1315,38 @@ drop-distr-map = drop-map
 "Warning: drop-distr-map was deprecated in v2.0.
 Please use drop-map instead."
 #-}
+
+map-insert = map-insertAt
+{-# WARNING_ON_USAGE map-insert
+"Warning: map-insert was deprecated in v2.0.
+Please use map-insertAt instead."
+#-}
+insert-lookup = insertAt-lookup
+{-# WARNING_ON_USAGE insert-lookup
+"Warning: insert-lookup was deprecated in v2.0.
+Please use insertAt-lookup instead."
+#-}
+insert-punchIn = insertAt-punchIn
+{-# WARNING_ON_USAGE insert-punchIn
+"Warning: insert-punchIn was deprecated in v2.0.
+Please use insertAt-punchIn instead."
+#-}
+remove-PunchOut = removeAt-punchOut
+{-# WARNING_ON_USAGE remove-PunchOut
+"Warning: remove-PunchOut was deprecated in v2.0.
+Please use removeAt-punchOut instead."
+#-}
+remove-insert = removeAt-insertAt
+{-# WARNING_ON_USAGE remove-insert
+"Warning: remove-insert was deprecated in v2.0.
+Please use removeAt-insertAt instead."
+#-}
+insert-remove = insertAt-removeAt
+{-# WARNING_ON_USAGE insert-remove
+"Warning: insert-remove was deprecated in v2.0.
+Please use insertAt-removeAt instead."
+#-}
+
 lookup-inject≤-take : ∀ m (m≤m+n : m ≤ m + n) (i : Fin m) (xs : Vec A (m + n)) →
                       lookup xs (Fin.inject≤ i m≤m+n) ≡ lookup (take m xs) i
 lookup-inject≤-take m m≤m+n i xs = sym (begin
@@ -1313,4 +1360,3 @@ lookup-inject≤-take m m≤m+n i xs = sym (begin
 "Warning: lookup-inject≤-take was deprecated in v2.0.
 Please use lookup-take-inject≤ or lookup-truncate, take≡truncate instead."
 #-}
-