From f732e32689ad3ba0ae633febf6eed1c7900b5d65 Mon Sep 17 00:00:00 2001
From: Saransh Chopra <saransh0701@gmail.com>
Date: Wed, 9 Aug 2023 11:52:49 -0400
Subject: [PATCH 01/21] Sync insert, delete, and update functions for List and
 Vec

---
 src/Data/Fin/Subset.agda                      |  2 +-
 src/Data/Fin/Subset/Properties.agda           |  2 +-
 src/Data/List/Base.agda                       | 24 +++++++++++++++----
 src/Data/List/Countdown.agda                  |  2 +-
 .../List/Relation/Unary/All/Properties.agda   |  2 +-
 src/Data/Vec/Base.agda                        |  9 ++++---
 6 files changed, 30 insertions(+), 11 deletions(-)

diff --git a/src/Data/Fin/Subset.agda b/src/Data/Fin/Subset.agda
index 01926df438..3055a8f026 100644
--- a/src/Data/Fin/Subset.agda
+++ b/src/Data/Fin/Subset.agda
@@ -14,7 +14,7 @@ open import Data.Fin.Base using (Fin; zero; suc)
 open import Data.List.Base using (List; foldr; foldl)
 open import Data.Nat.Base using (ℕ)
 open import Data.Product using (∃; _×_)
-open import Data.Vec.Base hiding (foldr; foldl)
+open import Data.Vec.Base hiding (foldr; foldl; _─_)
 open import Relation.Nullary
 
 private
diff --git a/src/Data/Fin/Subset/Properties.agda b/src/Data/Fin/Subset/Properties.agda
index 1cc8bd19f9..c7cdd0f136 100644
--- a/src/Data/Fin/Subset/Properties.agda
+++ b/src/Data/Fin/Subset/Properties.agda
@@ -25,7 +25,7 @@ open import Data.Nat.Base hiding (∣_-_∣)
 import Data.Nat.Properties as ℕₚ
 open import Data.Product as Product using (∃; ∄; _×_; _,_; proj₁)
 open import Data.Sum.Base as Sum using (_⊎_; inj₁; inj₂; [_,_]′)
-open import Data.Vec.Base
+open import Data.Vec.Base hiding (_─_)
 open import Data.Vec.Properties
 open import Function.Base using (_∘_; const; id; case_of_)
 open import Function.Bundles using (_⇔_; mk⇔)
diff --git a/src/Data/List/Base.agda b/src/Data/List/Base.agda
index 2b25ece003..12607d2472 100644
--- a/src/Data/List/Base.agda
+++ b/src/Data/List/Base.agda
@@ -195,6 +195,14 @@ tails : List A → List (List A)
 tails []       = [] ∷ []
 tails (x ∷ xs) = (x ∷ xs) ∷ tails xs
 
+insert : (xs : List A) → Fin (length xs) → A → List A
+insert (x ∷ xs) zero    v = v ∷ x ∷ xs
+insert (x ∷ xs) (suc k) v = v ∷ insert xs k 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
@@ -329,6 +337,10 @@ splitAt zero    xs       = ([] , xs)
 splitAt (suc n) []       = ([] , [])
 splitAt (suc n) (x ∷ xs) = Prod.map₁ (x ∷_) (splitAt n xs)
 
+remove : (xs : List A) → Fin (length xs) → List A
+remove (x ∷ xs) zero     = xs
+remove (x ∷ xs) (suc i)  = x ∷ remove 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
@@ -441,16 +453,20 @@ deduplicate R? = deduplicateᵇ (does ∘₂ R?)
 
 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 ─ i removes the i-th element of xs
+
 _─_ : (xs : List A) → Fin (length xs) → List A
-(x ∷ xs) ─ zero  = xs
-(x ∷ xs) ─ suc k = x ∷ (xs ─ k)
+xs ─ i = remove xs i
 
 ------------------------------------------------------------------------
 -- Conditional versions of cons and snoc
diff --git a/src/Data/List/Countdown.agda b/src/Data/List/Countdown.agda
index f1ef43ba8e..9d1ba5316a 100644
--- a/src/Data/List/Countdown.agda
+++ b/src/Data/List/Countdown.agda
@@ -20,7 +20,7 @@ open import Function.Base
 open import Function.Bundles
   using (Injection; module Injection)
 open import Data.Bool.Base using (true; false)
-open import Data.List.Base hiding (lookup)
+open import Data.List.Base hiding (lookup; insert)
 open import Data.List.Relation.Unary.Any as Any using (here; there)
 open import Data.Nat.Base using (ℕ; zero; suc)
 open import Data.Product
diff --git a/src/Data/List/Relation/Unary/All/Properties.agda b/src/Data/List/Relation/Unary/All/Properties.agda
index da3de23dd9..ead4589558 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/Vec/Base.agda b/src/Data/Vec/Base.agda
index 9f6d86b792..ccae1abfa9 100644
--- a/src/Data/Vec/Base.agda
+++ b/src/Data/Vec/Base.agda
@@ -78,18 +78,21 @@ updateAt (suc i) f (x ∷ xs) = x   ∷ updateAt i f xs
 
 -- 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 ]≔ 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
 
+-- xs ─ i removes the i-th element of xs
+
+_─_ : Vec A (suc n) → Fin (suc n) → Vec A n
+xs ─ i = remove xs i
+
 ------------------------------------------------------------------------
 -- Operations for transforming vectors
 

From f65a0e75713dc0ba5a134cdd739927049cc570c5 Mon Sep 17 00:00:00 2001
From: Saransh Chopra <saransh0701@gmail.com>
Date: Wed, 9 Aug 2023 18:12:41 -0400
Subject: [PATCH 02/21] Update CHANGELOG

---
 CHANGELOG.md | 17 ++++++++++-------
 1 file changed, 10 insertions(+), 7 deletions(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 3818f1a6f7..c1a8ad9290 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -2133,7 +2133,7 @@ Other minor changes
   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
@@ -2145,14 +2145,15 @@ Other minor changes
   wordsByᵇ     : (A → Bool) → List A → List (List A)
   derunᵇ       : (A → A → Bool) → List A → List A
   deduplicateᵇ : (A → A → Bool) → List A → List A
-  ```
 
-* 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 _
+
+  insert   : (xs : List A) → Fin (length xs) → A → List A
+  remove   : (xs : List A) → Fin (length xs) → List A
+  updateAt : (xs : List A) → Fin (length xs) → (A → A) → List A
   ```
 
 * Added new proofs in `Data.List.Relation.Binary.Lex.Strict`:
@@ -2558,6 +2559,8 @@ Other minor changes
   _ʳ++_              : Vec A m → Vec A n → Vec A (m + n)
 
   cast : .(eq : m ≡ n) → Vec A m → Vec A n
+
+  _─_ : Vec A (suc n) → Fin (suc n) → Vec A n
   ```
 
 * Added new instance in `Data.Vec.Categorical`:

From 2bf741c3142c7f924ed0d54640de941ccf612263 Mon Sep 17 00:00:00 2001
From: Saransh Chopra <saransh0701@gmail.com>
Date: Sun, 13 Aug 2023 19:05:16 -0400
Subject: [PATCH 03/21] Fix tests

---
 src/Data/Fin/Subset.agda | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/Data/Fin/Subset.agda b/src/Data/Fin/Subset.agda
index b3d53106ff..5b27cb7576 100644
--- a/src/Data/Fin/Subset.agda
+++ b/src/Data/Fin/Subset.agda
@@ -14,7 +14,7 @@ open import Data.Fin.Base using (Fin; zero; suc)
 open import Data.List.Base using (List; foldr; foldl)
 open import Data.Nat.Base using (ℕ)
 open import Data.Product.Base using (∃; _×_)
-open import Data.Vec.Base hiding (foldr; foldl)
+open import Data.Vec.Base hiding (foldr; foldl; _─_)
 open import Relation.Nullary
 
 private

From 3fe528b1c455ada35e75d5310e4c01e8c15079e1 Mon Sep 17 00:00:00 2001
From: Saransh Chopra <saransh0701@gmail.com>
Date: Mon, 21 Aug 2023 19:49:17 -0400
Subject: [PATCH 04/21] Update the definition of insert + add insert-remove,
 remove-insert, toList-insert

---
 src/Data/List/Base.agda       |  5 +++--
 src/Data/List/Properties.agda | 42 +++++++++++++++++++++++++++--------
 src/Data/Vec/Properties.agda  | 25 +++++++++++++++------
 3 files changed, 54 insertions(+), 18 deletions(-)

diff --git a/src/Data/List/Base.agda b/src/Data/List/Base.agda
index 12607d2472..ad16e098b2 100644
--- a/src/Data/List/Base.agda
+++ b/src/Data/List/Base.agda
@@ -195,9 +195,10 @@ tails : List A → List (List A)
 tails []       = [] ∷ []
 tails (x ∷ xs) = (x ∷ xs) ∷ tails xs
 
-insert : (xs : List A) → Fin (length xs) → A → List A
+insert : (xs : List A) → Fin (suc (length xs)) → A → List A
+insert []       zero    v = [ v ]
 insert (x ∷ xs) zero    v = v ∷ x ∷ xs
-insert (x ∷ xs) (suc k) v = v ∷ insert xs k v
+insert (x ∷ xs) (suc i) v = x ∷ insert xs i v
 
 updateAt : (xs : List A) → Fin (length xs) → (A → A) → List A
 updateAt (x ∷ xs) zero    f = f x ∷ xs
diff --git a/src/Data/List/Properties.agda b/src/Data/List/Properties.agda
index dd4326a749..0fcbcccc87 100644
--- a/src/Data/List/Properties.agda
+++ b/src/Data/List/Properties.agda
@@ -742,17 +742,41 @@ map-∷= (x ∷ xs) zero    v f = refl
 map-∷= (x ∷ xs) (suc k) v f = cong (f x ∷_) (map-∷= xs k v f)
 
 ------------------------------------------------------------------------
--- _─_
+-- insert
 
-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-insert : ∀ (xs : List A) (i : Fin (suc (length xs))) v → length (insert xs i v) ≡ suc (length xs)
+length-insert []       zero    v = refl
+length-insert (x ∷ xs) zero    v = refl
+length-insert (x ∷ xs) (suc i) v = cong suc (length-insert 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)
+------------------------------------------------------------------------
+-- remove
+
+length-remove : ∀ (xs : List A) k → suc (length (remove xs k)) ≡ length xs
+length-remove (x ∷ xs) zero        = refl
+length-remove (x ∷ y ∷ xs) (suc k) = cong suc (length-remove (y ∷ xs) k)
+
+map-remove : ∀ xs k (f : A → B) →
+            let eq = sym (length-map f xs) in
+            map f (remove xs k) ≡ remove (map f xs) (cast eq k)
+map-remove (x ∷ xs) zero    f = refl
+map-remove (x ∷ xs) (suc k) f = cong (f x ∷_) (map-remove xs k f)
+
+------------------------------------------------------------------------
+ -- insert and remove
+
+remove-insert : ∀ (xs : List A) (i : Fin (suc (length xs))) v → remove (insert xs i v) ((cast (sym (length-insert xs i v)) i)) ≡ xs
+remove-insert []       zero    v = refl
+remove-insert (x ∷ xs) zero    v = refl
+remove-insert (x ∷ xs) (suc i) v = cong (_ ∷_) (remove-insert xs i v)
+
+insert-remove : (xs : List A) (i : Fin (length xs)) → insert (remove xs i) (cast (sym (length-remove xs i)) i) (lookup xs i) ≡ xs
+insert-remove (x ∷ xs) zero = h xs x
+  where
+  h : ∀ (xs : List A) v → insert xs zero v ≡ v ∷ xs
+  h []       v = refl
+  h (x ∷ xs) v = refl
+insert-remove (x ∷ xs) (suc i) = cong (_ ∷_) (insert-remove xs i)
 
 ------------------------------------------------------------------------
 -- take
diff --git a/src/Data/Vec/Properties.agda b/src/Data/Vec/Properties.agda
index 49924a7b31..e9af8317de 100644
--- a/src/Data/Vec/Properties.agda
+++ b/src/Data/Vec/Properties.agda
@@ -1069,13 +1069,16 @@ 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)
+-- where should this go? Or can I write this proof without this? Or does
+-- something similar already exist?
+length-length : (xs : Vec A n) → length xs ≡ List.length (toList xs)
+length-length []       = refl
+length-length (x ∷ xs) = cong suc (length-length xs)
+
+toList-insert : ∀ (xs : Vec A n) (i : Fin (suc n)) (v : A) → toList (insert xs i v) ≡ List.insert (toList xs) (Fin.cast (cong suc (length-length xs)) i) v
+toList-insert []       zero    v = refl
+toList-insert (x ∷ xs) zero    v = refl
+toList-insert (x ∷ xs) (suc i) v = cong (_ List.∷_) (toList-insert xs i v)
 
 ------------------------------------------------------------------------
 -- remove
@@ -1093,6 +1096,14 @@ insert-remove (x ∷ xs)     zero     = refl
 insert-remove (x ∷ y ∷ xs) (suc i)  =
   cong (x ∷_) (insert-remove (y ∷ xs) i)
 
+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)
+
 ------------------------------------------------------------------------
 -- Conversion function
 

From 3eb4a4bc6a7a9b14ed3918488a74cf009bd8ebaa Mon Sep 17 00:00:00 2001
From: Saransh Chopra <saransh0701@gmail.com>
Date: Mon, 21 Aug 2023 20:06:54 -0400
Subject: [PATCH 05/21] Fix tests

---
 README/Nary.agda | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/README/Nary.agda b/README/Nary.agda
index b8b337832a..1ddc55f83a 100644
--- a/README/Nary.agda
+++ b/README/Nary.agda
@@ -14,7 +14,7 @@ open import Data.Nat.Base
 open import Data.Nat.Properties
 open import Data.Fin using (Fin; fromℕ; #_; inject₁)
 open import Data.List
-open import Data.List.Properties
+open import Data.List.Properties hiding (remove-insert)
 open import Data.Product.Base using (_×_; _,_)
 open import Data.Sum.Base using (inj₁; inj₂)
 open import Function.Base using (id; flip; _∘′_)

From 0b1ae971cc2960dd9cb7d317dd3def1dd23ac7bb Mon Sep 17 00:00:00 2001
From: Saransh Chopra <saransh0701@gmail.com>
Date: Mon, 21 Aug 2023 20:14:37 -0400
Subject: [PATCH 06/21] Update CHANGELOG + deprecations

---
 CHANGELOG.md                  |  9 ++++++++-
 src/Data/List/Properties.agda | 12 ++++++++++++
 src/Data/Vec/Properties.agda  | 19 +++++++++++--------
 3 files changed, 31 insertions(+), 9 deletions(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 2df0290557..a44c1c748d 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -2175,7 +2175,7 @@ Other minor changes
   ++-rawMagma     : Set a → RawMagma a _
   ++-[]-rawMonoid : Set a → RawMonoid a _
 
-  insert   : (xs : List A) → Fin (length xs) → A → List A
+  insert   : (xs : List A) → Fin (suc (length xs)) → A → List A
   remove   : (xs : List A) → Fin (length xs) → List A
   updateAt : (xs : List A) → Fin (length xs) → (A → A) → List A
   ```
@@ -2244,6 +2244,10 @@ Other minor changes
   map-replicate : map f (replicate n x) ≡ replicate n (f x)
 
   drop-drop : drop n (drop m xs) ≡ drop (m + n) xs
+
+  length-insert : length (insert xs i v) ≡ suc (length xs)
+  remove-insert : remove (insert xs i v) ((cast (sym (length-insert xs i v)) i)) ≡ xs
+  insert-remove : insert (remove xs i) (cast (sym (length-remove xs i)) i) (lookup xs i) ≡ xs
   ```
 
 * Added new patterns and definitions to `Data.Nat.Base`:
@@ -2664,6 +2668,9 @@ Other minor changes
   lookup-cast₂  : lookup xs (Fin.cast eq i) ≡ lookup (cast (sym eq) xs) i
 
   zipwith-++ : zipWith f (xs ++ ys) (xs' ++ ys') ≡ zipWith f xs xs' ++ zipWith f ys ys'
+
+  length-length : length xs ≡ List.length (toList xs)
+  toList-insert : toList (insert xs i v) ≡ List.insert (toList xs) (Fin.cast (cong suc (length-length xs)) i) v
   ```
 
 * Added new proofs in `Data.Vec.Membership.Propositional.Properties`:
diff --git a/src/Data/List/Properties.agda b/src/Data/List/Properties.agda
index 0208d88280..f94dcfc56d 100644
--- a/src/Data/List/Properties.agda
+++ b/src/Data/List/Properties.agda
@@ -1236,3 +1236,15 @@ zipWith-identityʳ = zipWith-zeroʳ
 "Warning: zipWith-identityʳ was deprecated in v2.0.
 Please use zipWith-zeroʳ instead."
 #-}
+
+length-─ = length-remove
+{-# WARNING_ON_USAGE length-─
+"Warning: length-─ was deprecated in v2.0.
+Please use length-remove instead."
+#-}
+
+map-─ = map-remove
+{-# WARNING_ON_USAGE map-─
+"Warning: map-─ was deprecated in v2.0.
+Please use map-remove instead."
+#-}
diff --git a/src/Data/Vec/Properties.agda b/src/Data/Vec/Properties.agda
index a6a204a588..b9d5debbfc 100644
--- a/src/Data/Vec/Properties.agda
+++ b/src/Data/Vec/Properties.agda
@@ -1113,6 +1113,17 @@ toList-insert (x ∷ xs) (suc i) v = cong (_ List.∷_) (toList-insert xs i v)
 ------------------------------------------------------------------------
 -- remove
 
+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)
+
+------------------------------------------------------------------------
+-- insert and remove
+
 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
@@ -1126,14 +1137,6 @@ insert-remove (x ∷ xs)     zero     = refl
 insert-remove (x ∷ y ∷ xs) (suc i)  =
   cong (x ∷_) (insert-remove (y ∷ xs) i)
 
-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)
-
 ------------------------------------------------------------------------
 -- Conversion function
 

From a36b6b0654dd25d28e526b889a45778cbddba08f Mon Sep 17 00:00:00 2001
From: Saransh Chopra <saransh0701@gmail.com>
Date: Mon, 21 Aug 2023 20:30:21 -0400
Subject: [PATCH 07/21] Quick comment for reviewers

---
 src/Data/Vec/Properties.agda | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/Data/Vec/Properties.agda b/src/Data/Vec/Properties.agda
index b9d5debbfc..979dec5404 100644
--- a/src/Data/Vec/Properties.agda
+++ b/src/Data/Vec/Properties.agda
@@ -1099,7 +1099,7 @@ 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
 
--- where should this go? Or can I write this proof without this? Or does
+-- where should this go? Or can I write toList-insert without this? Or does
 -- something similar already exist?
 length-length : (xs : Vec A n) → length xs ≡ List.length (toList xs)
 length-length []       = refl

From 2dce69cb3fe2974c4ec4b5865e03368b61735c06 Mon Sep 17 00:00:00 2001
From: Saransh Chopra <saransh0701@gmail.com>
Date: Mon, 21 Aug 2023 20:35:20 -0400
Subject: [PATCH 08/21] More CHANGELOG updates

---
 CHANGELOG.md | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index a44c1c748d..6519f22e41 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -1246,6 +1246,9 @@ Deprecated names
 
   zipWith-identityˡ  ↦  zipWith-zeroˡ
   zipWith-identityʳ  ↦  zipWith-zeroʳ
+
+  length-─  ↦  length-remove
+  map-─     ↦  map-remove
   ```
 
 * In `Data.List.NonEmpty.Properties`:

From 259aaf7b4dc602131fd03544dffdcabe4e2bc3ba Mon Sep 17 00:00:00 2001
From: Saransh Chopra <saransh0701@gmail.com>
Date: Thu, 14 Sep 2023 12:59:40 +0530
Subject: [PATCH 09/21] insert -> insertAt , remove -> removeAt

---
 CHANGELOG.md                          | 29 ++++++---
 README/Nary.agda                      |  2 +-
 src/Data/List/Base.agda               | 30 +++++----
 src/Data/List/Countdown.agda          |  2 +-
 src/Data/List/Properties.agda         | 46 +++++++-------
 src/Data/List/Relation/Unary/Any.agda |  4 +-
 src/Data/Vec/Base.agda                | 44 +++++++++----
 src/Data/Vec/Properties.agda          | 90 +++++++++++++++++----------
 8 files changed, 154 insertions(+), 93 deletions(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 6519f22e41..e0c7bd41b3 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -1247,8 +1247,8 @@ Deprecated names
   zipWith-identityˡ  ↦  zipWith-zeroˡ
   zipWith-identityʳ  ↦  zipWith-zeroʳ
 
-  length-─  ↦  length-remove
-  map-─     ↦  map-remove
+  length-─  ↦  length-removeAt
+  map-─     ↦  map-removeAt
   ```
 
 * In `Data.List.NonEmpty.Properties`:
@@ -1391,6 +1391,13 @@ Deprecated names
   map-compose     ↦  map-∘
   ```
 
+* In `Data.Vec.Base`:
+  ```
+  _─_     ↦ removeAt
+  remove  ↦ removeAt
+  insert  ↦ insertAt
+  ```
+
 * In `Data.Vec.Properties`:
   ```
   updateAt-id-relative      ↦  updateAt-id-local
@@ -1412,6 +1419,12 @@ Deprecated names
   to
   ```
   zipWith-comm : ∀ {f : A → B → C} {g : B → A → C}  (comm : ∀ x y → f x y ≡ g y x) (xs : Vec A n) ys → zipWith f xs ys ≡ zipWith g ys xs
+
+  map-insert      ↦ map-insertAt
+  insert-lookup   ↦ insertAt-lookup
+  insert-punchIn  ↦ insertAt-punchIn
+  remove-insert   ↦ removeAt-insertAt
+  insert-remove   ↦ insertAt-removeAt
   ```
 
 * In `Data.Vec.Functional.Properties`:
@@ -2178,8 +2191,8 @@ Other minor changes
   ++-rawMagma     : Set a → RawMagma a _
   ++-[]-rawMonoid : Set a → RawMonoid a _
 
-  insert   : (xs : List A) → Fin (suc (length xs)) → A → List A
-  remove   : (xs : List A) → Fin (length xs) → List A
+  insertAt : (xs : List A) → Fin (suc (length xs)) → A → List A
+  removeAt : (xs : List A) → Fin (length xs) → List A
   updateAt : (xs : List A) → Fin (length xs) → (A → A) → List A
   ```
 
@@ -2248,9 +2261,9 @@ Other minor changes
 
   drop-drop : drop n (drop m xs) ≡ drop (m + n) xs
 
-  length-insert : length (insert xs i v) ≡ suc (length xs)
-  remove-insert : remove (insert xs i v) ((cast (sym (length-insert xs i v)) i)) ≡ xs
-  insert-remove : insert (remove xs i) (cast (sym (length-remove xs i)) i) (lookup xs i) ≡ xs
+  length-insertAt   : ∀ (xs : List A) (i : Fin (suc (length xs))) v → length (insertAt xs i v) ≡ suc (length xs)
+  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
+  insertAt-removeAt : (xs : List A) (i : Fin (length xs)) → insertAt (removeAt xs i) (cast (sym (lengthAt-removeAt xs i)) i) (lookup xs i) ≡ xs
   ```
 
 * Added new patterns and definitions to `Data.Nat.Base`:
@@ -2595,8 +2608,6 @@ Other minor changes
   _ʳ++_              : Vec A m → Vec A n → Vec A (m + n)
 
   cast : .(eq : m ≡ n) → Vec A m → Vec A n
-
-  _─_ : Vec A (suc n) → Fin (suc n) → Vec A n
   ```
 
 * Added new instance in `Data.Vec.Categorical`:
diff --git a/README/Nary.agda b/README/Nary.agda
index 1ddc55f83a..f5194a0426 100644
--- a/README/Nary.agda
+++ b/README/Nary.agda
@@ -14,7 +14,7 @@ open import Data.Nat.Base
 open import Data.Nat.Properties
 open import Data.Fin using (Fin; fromℕ; #_; inject₁)
 open import Data.List
-open import Data.List.Properties hiding (remove-insert)
+open import Data.List.Properties hiding (removeAt-insertAt)
 open import Data.Product.Base using (_×_; _,_)
 open import Data.Sum.Base using (inj₁; inj₂)
 open import Function.Base using (id; flip; _∘′_)
diff --git a/src/Data/List/Base.agda b/src/Data/List/Base.agda
index ad16e098b2..5345ae5233 100644
--- a/src/Data/List/Base.agda
+++ b/src/Data/List/Base.agda
@@ -195,10 +195,10 @@ tails : List A → List (List A)
 tails []       = [] ∷ []
 tails (x ∷ xs) = (x ∷ xs) ∷ tails xs
 
-insert : (xs : List A) → Fin (suc (length xs)) → A → List A
-insert []       zero    v = [ v ]
-insert (x ∷ xs) zero    v = v ∷ x ∷ xs
-insert (x ∷ xs) (suc i) v = x ∷ insert xs i v
+insertAt : (xs : List A) → Fin (suc (length xs)) → A → List A
+insertAt []       zero    v = [ v ]
+insertAt (x ∷ xs) zero    v = v ∷ x ∷ 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
@@ -338,9 +338,9 @@ splitAt zero    xs       = ([] , xs)
 splitAt (suc n) []       = ([] , [])
 splitAt (suc n) (x ∷ xs) = Prod.map₁ (x ∷_) (splitAt n xs)
 
-remove : (xs : List A) → Fin (length xs) → List A
-remove (x ∷ xs) zero     = xs
-remove (x ∷ xs) (suc i)  = x ∷ remove xs i
+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
@@ -452,7 +452,7 @@ deduplicate R? = deduplicateᵇ (does ∘₂ R?)
 ------------------------------------------------------------------------
 -- Actions on single elements
 
-infixl 5 _[_]%=_ _[_]∷=_ _─_
+infixl 5 _[_]%=_ _[_]∷=_
 
 -- xs [ i ]%= f  modifies the i-th element of xs according to f
 
@@ -464,11 +464,6 @@ xs [ i ]%= f = updateAt xs i f
 _[_]∷=_ : (xs : List A) → Fin (length xs) → A → List A
 xs [ k ]∷= v = xs [ k ]%= const v
 
--- xs ─ i removes the i-th element of xs
-
-_─_ : (xs : List A) → Fin (length xs) → List A
-xs ─ i = remove xs i
-
 ------------------------------------------------------------------------
 -- Conditional versions of cons and snoc
 
@@ -514,3 +509,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/Countdown.agda b/src/Data/List/Countdown.agda
index 31ea8a86cb..90a0cb49d2 100644
--- a/src/Data/List/Countdown.agda
+++ b/src/Data/List/Countdown.agda
@@ -20,7 +20,7 @@ open import Function.Base
 open import Function.Bundles
   using (Injection; module Injection)
 open import Data.Bool.Base using (true; false)
-open import Data.List.Base hiding (lookup; insert)
+open import Data.List.Base hiding (lookup; insertAt)
 open import Data.List.Relation.Unary.Any as Any using (here; there)
 open import Data.Nat.Base using (ℕ; zero; suc)
 open import Data.Product.Base using (∃; _,_; _×_)
diff --git a/src/Data/List/Properties.agda b/src/Data/List/Properties.agda
index f94dcfc56d..1c2aeb469c 100644
--- a/src/Data/List/Properties.agda
+++ b/src/Data/List/Properties.agda
@@ -748,39 +748,39 @@ map-∷= (x ∷ xs) (suc k) v f = cong (f x ∷_) (map-∷= xs k v f)
 ------------------------------------------------------------------------
 -- insert
 
-length-insert : ∀ (xs : List A) (i : Fin (suc (length xs))) v → length (insert xs i v) ≡ suc (length xs)
-length-insert []       zero    v = refl
-length-insert (x ∷ xs) zero    v = refl
-length-insert (x ∷ xs) (suc i) v = cong suc (length-insert xs i v)
+length-insertAt : ∀ (xs : List A) (i : Fin (suc (length xs))) v → length (insertAt xs i v) ≡ suc (length xs)
+length-insertAt []       zero    v = refl
+length-insertAt (x ∷ xs) zero    v = refl
+length-insertAt (x ∷ xs) (suc i) v = cong suc (length-insertAt xs i v)
 
 ------------------------------------------------------------------------
 -- remove
 
-length-remove : ∀ (xs : List A) k → suc (length (remove xs k)) ≡ length xs
-length-remove (x ∷ xs) zero        = refl
-length-remove (x ∷ y ∷ xs) (suc k) = cong suc (length-remove (y ∷ xs) k)
+length-removeAt : ∀ (xs : List A) k → suc (length (removeAt xs k)) ≡ length xs
+length-removeAt (x ∷ xs) zero        = refl
+length-removeAt (x ∷ y ∷ xs) (suc k) = cong suc (length-removeAt (y ∷ xs) k)
 
-map-remove : ∀ xs k (f : A → B) →
+map-removeAt : ∀ xs k (f : A → B) →
             let eq = sym (length-map f xs) in
-            map f (remove xs k) ≡ remove (map f xs) (cast eq k)
-map-remove (x ∷ xs) zero    f = refl
-map-remove (x ∷ xs) (suc k) f = cong (f x ∷_) (map-remove xs k f)
+            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)
 
 ------------------------------------------------------------------------
  -- insert and remove
 
-remove-insert : ∀ (xs : List A) (i : Fin (suc (length xs))) v → remove (insert xs i v) ((cast (sym (length-insert xs i v)) i)) ≡ xs
-remove-insert []       zero    v = refl
-remove-insert (x ∷ xs) zero    v = refl
-remove-insert (x ∷ xs) (suc i) v = cong (_ ∷_) (remove-insert xs i v)
+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 []       zero    v = refl
+removeAt-insertAt (x ∷ xs) zero    v = refl
+removeAt-insertAt (x ∷ xs) (suc i) v = cong (_ ∷_) (removeAt-insertAt xs i v)
 
-insert-remove : (xs : List A) (i : Fin (length xs)) → insert (remove xs i) (cast (sym (length-remove xs i)) i) (lookup xs i) ≡ xs
-insert-remove (x ∷ xs) zero = h xs x
+insertAt-removeAt : (xs : List A) (i : Fin (length xs)) → insertAt (removeAt xs i) (cast (sym (length-removeAt xs i)) i) (lookup xs i) ≡ xs
+insertAt-removeAt (x ∷ xs) zero = h xs x
   where
-  h : ∀ (xs : List A) v → insert xs zero v ≡ v ∷ xs
+  h : ∀ (xs : List A) v → insertAt xs zero v ≡ v ∷ xs
   h []       v = refl
   h (x ∷ xs) v = refl
-insert-remove (x ∷ xs) (suc i) = cong (_ ∷_) (insert-remove xs i)
+insertAt-removeAt (x ∷ xs) (suc i) = cong (_ ∷_) (insertAt-removeAt xs i)
 
 ------------------------------------------------------------------------
 -- take
@@ -1237,14 +1237,14 @@ zipWith-identityʳ = zipWith-zeroʳ
 Please use zipWith-zeroʳ instead."
 #-}
 
-length-─ = length-remove
+length-─ = length-removeAt
 {-# WARNING_ON_USAGE length-─
 "Warning: length-─ was deprecated in v2.0.
-Please use length-remove instead."
+Please use length-removeAt instead."
 #-}
 
-map-─ = map-remove
+map-─ = map-removeAt
 {-# WARNING_ON_USAGE map-─
 "Warning: map-─ was deprecated in v2.0.
-Please use map-remove instead."
+Please use map-removeAt instead."
 #-}
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 ccae1abfa9..cc10e53026 100644
--- a/src/Data/Vec/Base.agda
+++ b/src/Data/Vec/Base.agda
@@ -64,13 +64,13 @@ 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 (_ ∷ xs)     zero     = xs
+removeAt (x ∷ y ∷ xs) (suc i)  = x ∷ removeAt (y ∷ xs) i
 
 updateAt : Fin n → (A → A) → Vec A n → Vec A n
 updateAt zero    f (x ∷ xs) = f x ∷ xs
@@ -78,7 +78,7 @@ updateAt (suc i) f (x ∷ xs) = x   ∷ updateAt i f xs
 
 -- 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
@@ -88,11 +88,6 @@ xs [ i ]%= f = updateAt i f xs
 _[_]≔_ : Vec A n → Fin n → A → Vec A n
 xs [ i ]≔ y = xs [ i ]%= const y
 
--- xs ─ i removes the i-th element of xs
-
-_─_ : Vec A (suc n) → Fin (suc n) → Vec A n
-xs ─ i = remove xs i
-
 ------------------------------------------------------------------------
 -- Operations for transforming vectors
 
@@ -361,3 +356,28 @@ last xs with initLast xs
 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
+
+infixl 6 _─_
+_─_ = removeAt
+{-# WARNING_ON_USAGE _─_
+"Warning: _─_ was deprecated in v2.0.
+Please use removeAt instead."
+#-}
+remove = removeAt
+{-# WARNING_ON_USAGE _─_
+"Warning: remove was deprecated in v2.0.
+Please use removeAt instead."
+#-}
+insert = insertAt
+{-# WARNING_ON_USAGE _─_
+"Warning: insert was deprecated in v2.0.
+Please use insertAt instead."
+#-}
diff --git a/src/Data/Vec/Properties.agda b/src/Data/Vec/Properties.agda
index 979dec5404..0b6f6855a8 100644
--- a/src/Data/Vec/Properties.agda
+++ b/src/Data/Vec/Properties.agda
@@ -448,11 +448,11 @@ map-updateAt : ∀ {f : A → B} {g : A → A} {h : B → B}
 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 _ []        Fin.zero = refl
-map-insert f _ (x' ∷ xs) Fin.zero = refl
-map-insert f x (x' ∷ xs) (Fin.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
@@ -1086,29 +1086,29 @@ module _ {P : Pred A p} (P? : Decidable P) where
   ... | false = m≤n⇒m≤1+n (count≤n xs)
 
 ------------------------------------------------------------------------
--- insert
+-- insertAt
 
-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
+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
 
-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
+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
 
--- where should this go? Or can I write toList-insert without this? Or does
+-- where should this go? Or can I write toList-insertAt without this? Or does
 -- something similar already exist?
 length-length : (xs : Vec A n) → length xs ≡ List.length (toList xs)
 length-length []       = refl
 length-length (x ∷ xs) = cong suc (length-length xs)
 
-toList-insert : ∀ (xs : Vec A n) (i : Fin (suc n)) (v : A) → toList (insert xs i v) ≡ List.insert (toList xs) (Fin.cast (cong suc (length-length xs)) i) v
-toList-insert []       zero    v = refl
-toList-insert (x ∷ xs) zero    v = refl
-toList-insert (x ∷ xs) (suc i) v = cong (_ List.∷_) (toList-insert xs i v)
+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 (length-length xs)) i) v
+toList-insertAt []       zero    v = refl
+toList-insertAt (x ∷ xs) zero    v = refl
+toList-insertAt (x ∷ xs) (suc i) v = cong (_ List.∷_) (toList-insertAt xs i v)
 
 ------------------------------------------------------------------------
 -- remove
@@ -1122,20 +1122,20 @@ remove-punchOut (x ∷ y ∷ xs) {suc i} {suc j} i≢j =
   remove-punchOut (y ∷ xs) (i≢j ∘ cong suc)
 
 ------------------------------------------------------------------------
--- insert and 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 ∷ y ∷ xs) (suc (suc i))  v =
+  cong (x ∷_) (removeAt-insertAt (y ∷ 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 ∷ y ∷ xs) (suc i)  =
+  cong (x ∷_) (insertAt-removeAt (y ∷ xs) i)
 
 ------------------------------------------------------------------------
 -- Conversion function
@@ -1200,3 +1200,29 @@ sum-++-commute = sum-++
 "Warning: sum-++-commute was deprecated in v2.0.
 Please use sum-++ 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-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."
+#-}

From fef90196a78f8a58541d44c4985f7d0bc399e220 Mon Sep 17 00:00:00 2001
From: Saransh Chopra <saransh0701@gmail.com>
Date: Thu, 14 Sep 2023 13:22:26 +0530
Subject: [PATCH 10/21] add length-toList

---
 CHANGELOG.md                 |  2 ++
 src/Data/Vec/Properties.agda | 15 ++++++++-------
 2 files changed, 10 insertions(+), 7 deletions(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index e0c7bd41b3..4d7905fd7e 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -915,6 +915,8 @@ Non-backwards compatible changes
     ```
   * `excluded-middle` in `Relation.Nullary.Decidable.Core` has been renamed to
     `¬¬-excluded-middle`.
+  * `length-─` in `Data.List.Properties` has been renamed to `length-removeAt`
+     with a new type `suc (length (removeAt xs k)) ≡ length xs`
 
 Major improvements
 ------------------
diff --git a/src/Data/Vec/Properties.agda b/src/Data/Vec/Properties.agda
index 0b6f6855a8..029ca2add0 100644
--- a/src/Data/Vec/Properties.agda
+++ b/src/Data/Vec/Properties.agda
@@ -1085,6 +1085,13 @@ module _ {P : Pred A p} (P? : Decidable P) where
   ... | true  = s≤s (count≤n xs)
   ... | false = m≤n⇒m≤1+n (count≤n xs)
 
+------------------------------------------------------------------------
+-- 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
 
@@ -1099,13 +1106,7 @@ 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
 
--- where should this go? Or can I write toList-insertAt without this? Or does
--- something similar already exist?
-length-length : (xs : Vec A n) → length xs ≡ List.length (toList xs)
-length-length []       = refl
-length-length (x ∷ xs) = cong suc (length-length xs)
-
-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 (length-length xs)) i) v
+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 []       zero    v = refl
 toList-insertAt (x ∷ xs) zero    v = refl
 toList-insertAt (x ∷ xs) (suc i) v = cong (_ List.∷_) (toList-insertAt xs i v)

From a50b5d37b433377c47a44b724770870beeadbcfb Mon Sep 17 00:00:00 2001
From: Saransh Chopra <saransh0701@gmail.com>
Date: Thu, 14 Sep 2023 16:40:42 +0530
Subject: [PATCH 11/21] Simplify proofs

Co-authored-by: jamesmckinna <31931406+jamesmckinna@users.noreply.github.com>
---
 CHANGELOG.md                  |  2 +-
 src/Data/List/Base.agda       |  3 +--
 src/Data/List/Properties.agda | 34 ++++++++++++++++------------------
 src/Data/Vec/Properties.agda  | 10 +++++-----
 4 files changed, 23 insertions(+), 26 deletions(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 4d7905fd7e..d3618e6134 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -2685,7 +2685,7 @@ Other minor changes
 
   zipwith-++ : zipWith f (xs ++ ys) (xs' ++ ys') ≡ zipWith f xs xs' ++ zipWith f ys ys'
 
-  length-length : length xs ≡ List.length (toList xs)
+  length-toList : List.length (toList xs) ≡ length xs
   toList-insert : toList (insert xs i v) ≡ List.insert (toList xs) (Fin.cast (cong suc (length-length xs)) i) v
   ```
 
diff --git a/src/Data/List/Base.agda b/src/Data/List/Base.agda
index 5345ae5233..3403608529 100644
--- a/src/Data/List/Base.agda
+++ b/src/Data/List/Base.agda
@@ -196,8 +196,7 @@ tails []       = [] ∷ []
 tails (x ∷ xs) = (x ∷ xs) ∷ tails xs
 
 insertAt : (xs : List A) → Fin (suc (length xs)) → A → List A
-insertAt []       zero    v = [ v ]
-insertAt (x ∷ xs) zero    v = v ∷ x ∷ xs
+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
diff --git a/src/Data/List/Properties.agda b/src/Data/List/Properties.agda
index 1c2aeb469c..d953ce3496 100644
--- a/src/Data/List/Properties.agda
+++ b/src/Data/List/Properties.agda
@@ -746,19 +746,20 @@ map-∷= (x ∷ xs) zero    v f = refl
 map-∷= (x ∷ xs) (suc k) v f = cong (f x ∷_) (map-∷= xs k v f)
 
 ------------------------------------------------------------------------
--- insert
+-- insertAt
 
-length-insertAt : ∀ (xs : List A) (i : Fin (suc (length xs))) v → length (insertAt xs i v) ≡ suc (length xs)
-length-insertAt []       zero    v = refl
-length-insertAt (x ∷ xs) zero    v = refl
+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)
 
 ------------------------------------------------------------------------
--- remove
+-- removeAt
 
-length-removeAt : ∀ (xs : List A) k → suc (length (removeAt xs k)) ≡ length xs
-length-removeAt (x ∷ xs) zero        = refl
-length-removeAt (x ∷ y ∷ xs) (suc k) = cong suc (length-removeAt (y ∷ xs) k)
+length-removeAt : ∀ (xs : List A) k →
+                  suc (length (removeAt xs k)) ≡ length xs
+length-removeAt (x ∷ xs) zero    = refl
+length-removeAt (x ∷ xs) (suc k) = cong suc (length-removeAt xs k)
 
 map-removeAt : ∀ xs k (f : A → B) →
             let eq = sym (length-map f xs) in
@@ -767,19 +768,16 @@ map-removeAt (x ∷ xs) zero    f = refl
 map-removeAt (x ∷ xs) (suc k) f = cong (f x ∷_) (map-removeAt xs k f)
 
 ------------------------------------------------------------------------
- -- insert and remove
+ -- 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 []       zero    v = refl
-removeAt-insertAt (x ∷ xs) zero    v = refl
+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 (sym (length-removeAt xs i)) i) (lookup xs i) ≡ xs
-insertAt-removeAt (x ∷ xs) zero = h xs x
-  where
-  h : ∀ (xs : List A) v → insertAt xs zero v ≡ v ∷ xs
-  h []       v = refl
-  h (x ∷ xs) v = refl
+insertAt-removeAt : (xs : List A) (i : Fin (length xs)) →
+  insertAt (removeAt xs i) (cast (sym (length-removeAt xs i)) i) (lookup xs i) ≡ xs
+insertAt-removeAt (x ∷ xs) zero = refl
 insertAt-removeAt (x ∷ xs) (suc i) = cong (_ ∷_) (insertAt-removeAt xs i)
 
 ------------------------------------------------------------------------
diff --git a/src/Data/Vec/Properties.agda b/src/Data/Vec/Properties.agda
index 029ca2add0..5ff14424de 100644
--- a/src/Data/Vec/Properties.agda
+++ b/src/Data/Vec/Properties.agda
@@ -1096,19 +1096,19 @@ 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
+                  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
+                   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 []       zero    v = refl
-toList-insertAt (x ∷ xs) zero    v = refl
+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)
 
 ------------------------------------------------------------------------

From 3b4d66625746ca61be0232721f5e64f8cac3180e Mon Sep 17 00:00:00 2001
From: Saransh Chopra <saransh0701@gmail.com>
Date: Thu, 14 Sep 2023 16:44:23 +0530
Subject: [PATCH 12/21] Update CHANGELOG

---
 CHANGELOG.md | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index d3618e6134..da54e2fb8b 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -2686,7 +2686,7 @@ Other minor changes
   zipwith-++ : zipWith f (xs ++ ys) (xs' ++ ys') ≡ zipWith f xs xs' ++ zipWith f ys ys'
 
   length-toList : List.length (toList xs) ≡ length xs
-  toList-insert : toList (insert xs i v) ≡ List.insert (toList xs) (Fin.cast (cong suc (length-length xs)) i) v
+  toList-insertAt : toList (insertAt xs i v) ≡ List.insertAt (toList xs) (Fin.cast (cong suc (sym (length-toList xs))) i) v
   ```
 
 * Added new proofs in `Data.Vec.Membership.Propositional.Properties`:

From ee6bd4de2662112297274cda0e28fc2c1c9f9d69 Mon Sep 17 00:00:00 2001
From: Saransh Chopra <saransh0701@gmail.com>
Date: Fri, 15 Sep 2023 16:41:31 +0530
Subject: [PATCH 13/21] More deprecations

---
 CHANGELOG.md | 24 +++++++++++-------------
 1 file changed, 11 insertions(+), 13 deletions(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index e1086cf879..877a75fe5c 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -930,8 +930,6 @@ Non-backwards compatible changes
     ```
   * `excluded-middle` in `Relation.Nullary.Decidable.Core` has been renamed to
     `¬¬-excluded-middle`.
-  * `length-─` in `Data.List.Properties` has been renamed to `length-removeAt`
-     with a new type `suc (length (removeAt xs k)) ≡ length xs`
 
 Major improvements
 ------------------
@@ -1266,7 +1264,7 @@ Deprecated names
 
   ʳ++-++  ↦  ++-ʳ++
 
-  take++drop ↦ take++drop≡id
+  take++drop  ↦  take++drop≡id
 
   length-─  ↦  length-removeAt
   map-─     ↦  map-removeAt
@@ -1414,9 +1412,9 @@ Deprecated names
 
 * In `Data.Vec.Base`:
   ```
-  _─_     ↦ removeAt
-  remove  ↦ removeAt
-  insert  ↦ insertAt
+  _─_     ↦   removeAt
+  remove  ↦  removeAt
+  insert  ↦  insertAt
   ```
 
 * In `Data.Vec.Properties`:
@@ -1433,7 +1431,13 @@ 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-insert   ↦ removeAt-insertAt
+  insert-remove   ↦ insertAt-removeAt
   ```
   and the type of the proof `zipWith-comm` has been generalised from:
   ```
@@ -1442,12 +1446,6 @@ Deprecated names
   to
   ```
   zipWith-comm : ∀ {f : A → B → C} {g : B → A → C}  (comm : ∀ x y → f x y ≡ g y x) (xs : Vec A n) ys → zipWith f xs ys ≡ zipWith g ys xs
-
-  map-insert      ↦ map-insertAt
-  insert-lookup   ↦ insertAt-lookup
-  insert-punchIn  ↦ insertAt-punchIn
-  remove-insert   ↦ removeAt-insertAt
-  insert-remove   ↦ insertAt-removeAt
   ```
 
 * In `Data.Vec.Functional.Properties`:

From bf756ad2575d29c31271e0bbcb7c9c6d7726ff5a Mon Sep 17 00:00:00 2001
From: Saransh Chopra <saransh0701@gmail.com>
Date: Fri, 15 Sep 2023 16:57:28 +0530
Subject: [PATCH 14/21] Simplify proofs more

---
 CHANGELOG.md                  | 19 ++++++++++---------
 README/Nary.agda              |  2 +-
 src/Data/List/Countdown.agda  |  2 +-
 src/Data/List/Properties.agda | 16 +++++++++-------
 src/Data/Vec/Properties.agda  | 14 +++++++-------
 5 files changed, 28 insertions(+), 25 deletions(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 877a75fe5c..2e1a811aac 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -1412,7 +1412,7 @@ Deprecated names
 
 * In `Data.Vec.Base`:
   ```
-  _─_     ↦   removeAt
+  _─_     ↦  removeAt
   remove  ↦  removeAt
   insert  ↦  insertAt
   ```
@@ -1433,11 +1433,11 @@ Deprecated names
 
   take-drop-id  ↦  take++drop≡id
 
-  map-insert      ↦ map-insertAt
-  insert-lookup   ↦ insertAt-lookup
-  insert-punchIn  ↦ insertAt-punchIn
-  remove-insert   ↦ removeAt-insertAt
-  insert-remove   ↦ insertAt-removeAt
+  map-insert      ↦  map-insertAt
+  insert-lookup   ↦  insertAt-lookup
+  insert-punchIn  ↦  insertAt-punchIn
+  remove-insert   ↦  removeAt-insertAt
+  insert-remove   ↦  insertAt-removeAt
   ```
   and the type of the proof `zipWith-comm` has been generalised from:
   ```
@@ -2289,9 +2289,10 @@ Other minor changes
 
   drop-drop : drop n (drop m xs) ≡ drop (m + n) xs
 
-  length-insertAt   : ∀ (xs : List A) (i : Fin (suc (length xs))) v → length (insertAt xs i v) ≡ suc (length xs)
-  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
-  insertAt-removeAt : (xs : List A) (i : Fin (length xs)) → insertAt (removeAt xs i) (cast (sym (lengthAt-removeAt xs i)) i) (lookup xs i) ≡ 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`:
diff --git a/README/Nary.agda b/README/Nary.agda
index f5194a0426..b8b337832a 100644
--- a/README/Nary.agda
+++ b/README/Nary.agda
@@ -14,7 +14,7 @@ open import Data.Nat.Base
 open import Data.Nat.Properties
 open import Data.Fin using (Fin; fromℕ; #_; inject₁)
 open import Data.List
-open import Data.List.Properties hiding (removeAt-insertAt)
+open import Data.List.Properties
 open import Data.Product.Base using (_×_; _,_)
 open import Data.Sum.Base using (inj₁; inj₂)
 open import Function.Base using (id; flip; _∘′_)
diff --git a/src/Data/List/Countdown.agda b/src/Data/List/Countdown.agda
index f2bd770359..8d6761de27 100644
--- a/src/Data/List/Countdown.agda
+++ b/src/Data/List/Countdown.agda
@@ -20,7 +20,7 @@ open import Function.Base
 open import Function.Bundles
   using (Injection; module Injection)
 open import Data.Bool.Base using (true; false)
-open import Data.List.Base hiding (lookup; insertAt)
+open import Data.List.Base hiding (lookup)
 open import Data.List.Relation.Unary.Any as Any using (here; there)
 open import Data.Nat.Base using (ℕ; zero; suc)
 open import Data.Product.Base using (∃; _,_; _×_)
diff --git a/src/Data/List/Properties.agda b/src/Data/List/Properties.agda
index eb6b463b66..48f533f08d 100644
--- a/src/Data/List/Properties.agda
+++ b/src/Data/List/Properties.agda
@@ -756,10 +756,12 @@ length-insertAt (x ∷ xs) (suc i) v = cong suc (length-insertAt xs i v)
 ------------------------------------------------------------------------
 -- removeAt
 
-length-removeAt : ∀ (xs : List A) k →
-                  suc (length (removeAt xs k)) ≡ 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 (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
@@ -776,9 +778,9 @@ 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 (sym (length-removeAt xs i)) i) (lookup xs i) ≡ xs
-insertAt-removeAt (x ∷ xs) zero = refl
-insertAt-removeAt (x ∷ xs) (suc i) = cong (_ ∷_) (insertAt-removeAt xs i)
+  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
diff --git a/src/Data/Vec/Properties.agda b/src/Data/Vec/Properties.agda
index 63727b8907..707cffa2cb 100644
--- a/src/Data/Vec/Properties.agda
+++ b/src/Data/Vec/Properties.agda
@@ -1158,16 +1158,16 @@ remove-punchOut (x ∷ y ∷ xs) {suc i} {suc j} i≢j =
 
 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 ∷ y ∷ xs) (suc (suc i))  v =
-  cong (x ∷_) (removeAt-insertAt (y ∷ xs) (suc i) v)
+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)
 
 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 ∷ y ∷ xs) (suc i)  =
-  cong (x ∷_) (insertAt-removeAt (y ∷ xs) i)
+insertAt-removeAt (x ∷ xs)         zero     = refl
+insertAt-removeAt (x ∷ xs@(_ ∷ _)) (suc i)  =
+  cong (x ∷_) (insertAt-removeAt xs i)
 
 ------------------------------------------------------------------------
 -- Conversion function

From ccd7ef598d37336fc5982b484af59cf5fdd2f25e Mon Sep 17 00:00:00 2001
From: Saransh Chopra <saransh0701@gmail.com>
Date: Fri, 15 Sep 2023 17:23:43 +0530
Subject: [PATCH 15/21] Simplify imports, fix tests

---
 CHANGELOG.md                        | 17 +++++++++++------
 src/Data/Fin/Subset.agda            |  2 +-
 src/Data/Fin/Subset/Properties.agda |  2 +-
 src/Data/Vec/Base.agda              | 10 ++--------
 src/Data/Vec/Properties.agda        | 21 +++++++++++++--------
 5 files changed, 28 insertions(+), 24 deletions(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 1e4b9cafa8..7763b26331 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -1248,6 +1248,11 @@ Deprecated names
   +-isAbelianGroup ↦ +-0-isAbelianGroup
   ```
 
+* In `Data.List.Base`:
+  ```
+  _─_  ↦  removeAt
+  ```
+
 * In `Data.List.Properties`:
   ```agda
   map-id₂         ↦  map-id-local
@@ -1412,7 +1417,6 @@ Deprecated names
 
 * In `Data.Vec.Base`:
   ```
-  _─_     ↦  removeAt
   remove  ↦  removeAt
   insert  ↦  insertAt
   ```
@@ -1433,11 +1437,12 @@ Deprecated names
 
   take-drop-id  ↦  take++drop≡id
 
-  map-insert      ↦  map-insertAt
-  insert-lookup   ↦  insertAt-lookup
-  insert-punchIn  ↦  insertAt-punchIn
-  remove-insert   ↦  removeAt-insertAt
-  insert-remove   ↦  insertAt-removeAt
+  map-insert       ↦  map-insertAt
+  insert-lookup    ↦  insertAt-lookup
+  insert-punchIn   ↦  insertAt-punchIn
+  remove-PunchOut  ↦ removeAt-punchOut
+  remove-insert    ↦  removeAt-insertAt
+  insert-remove    ↦  insertAt-removeAt
   ```
   and the type of the proof `zipWith-comm` has been generalised from:
   ```
diff --git a/src/Data/Fin/Subset.agda b/src/Data/Fin/Subset.agda
index 5b27cb7576..b3d53106ff 100644
--- a/src/Data/Fin/Subset.agda
+++ b/src/Data/Fin/Subset.agda
@@ -14,7 +14,7 @@ open import Data.Fin.Base using (Fin; zero; suc)
 open import Data.List.Base using (List; foldr; foldl)
 open import Data.Nat.Base using (ℕ)
 open import Data.Product.Base using (∃; _×_)
-open import Data.Vec.Base hiding (foldr; foldl; _─_)
+open import Data.Vec.Base hiding (foldr; foldl)
 open import Relation.Nullary
 
 private
diff --git a/src/Data/Fin/Subset/Properties.agda b/src/Data/Fin/Subset/Properties.agda
index 2da2c39466..2f7246da6a 100644
--- a/src/Data/Fin/Subset/Properties.agda
+++ b/src/Data/Fin/Subset/Properties.agda
@@ -25,7 +25,7 @@ open import Data.Nat.Base hiding (∣_-_∣)
 import Data.Nat.Properties as ℕₚ
 open import Data.Product as Product using (∃; ∄; _×_; _,_; proj₁)
 open import Data.Sum.Base as Sum using (_⊎_; inj₁; inj₂; [_,_]′)
-open import Data.Vec.Base hiding (_─_)
+open import Data.Vec.Base
 open import Data.Vec.Properties
 open import Function.Base using (_∘_; const; id; case_of_)
 open import Function.Bundles using (_⇔_; mk⇔)
diff --git a/src/Data/Vec/Base.agda b/src/Data/Vec/Base.agda
index 43908c5019..d4c0d3b580 100644
--- a/src/Data/Vec/Base.agda
+++ b/src/Data/Vec/Base.agda
@@ -363,19 +363,13 @@ transpose (as ∷ ass) = replicate _∷_ ⊛ as ⊛ transpose ass
 
 -- Version 2.0
 
-infixl 6 _─_
-_─_ = removeAt
-{-# WARNING_ON_USAGE _─_
-"Warning: _─_ was deprecated in v2.0.
-Please use removeAt instead."
-#-}
 remove = removeAt
-{-# WARNING_ON_USAGE _─_
+{-# WARNING_ON_USAGE remove
 "Warning: remove was deprecated in v2.0.
 Please use removeAt instead."
 #-}
 insert = insertAt
-{-# WARNING_ON_USAGE _─_
+{-# WARNING_ON_USAGE insert
 "Warning: insert was deprecated in v2.0.
 Please use insertAt instead."
 #-}
diff --git a/src/Data/Vec/Properties.agda b/src/Data/Vec/Properties.agda
index 956ab22a23..eaea4d12e3 100644
--- a/src/Data/Vec/Properties.agda
+++ b/src/Data/Vec/Properties.agda
@@ -1195,15 +1195,15 @@ toList-insertAt xs       zero    v = refl
 toList-insertAt (x ∷ xs) (suc i) v = cong (_ List.∷_) (toList-insertAt xs i v)
 
 ------------------------------------------------------------------------
--- remove
+-- removeAt
 
-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)
+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)
 
 ------------------------------------------------------------------------
 -- insertAt and removeAt
@@ -1329,6 +1329,11 @@ insert-punchIn = insertAt-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.

From 6ce3f6ca132c437d4ad38584bd992c5684669dcf Mon Sep 17 00:00:00 2001
From: Saransh Chopra <saransh0701@gmail.com>
Date: Fri, 15 Sep 2023 17:53:26 +0530
Subject: [PATCH 16/21] Update CHANGELOG.md

---
 CHANGELOG.md | 1 -
 1 file changed, 1 deletion(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 7763b26331..c9a7c5f38a 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -2225,7 +2225,6 @@ Other minor changes
   ++-[]-rawMonoid : Set a → RawMonoid a _
 
   insertAt : (xs : List A) → Fin (suc (length xs)) → A → List A
-  removeAt : (xs : List A) → Fin (length xs) → List A
   updateAt : (xs : List A) → Fin (length xs) → (A → A) → List A
   ```
 

From 90310ea7351a7bfecb4c750b237d70454347d03c Mon Sep 17 00:00:00 2001
From: Saransh Chopra <saransh0701@gmail.com>
Date: Sun, 17 Sep 2023 13:18:56 +0530
Subject: [PATCH 17/21] Update type of Vec.updateAt

---
 CHANGELOG.md                 |  8 ++++
 src/Data/Vec/Base.agda       |  8 ++--
 src/Data/Vec/Properties.agda | 86 ++++++++++++++++++------------------
 3 files changed, 55 insertions(+), 47 deletions(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 7763b26331..3e7b6be444 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -2642,6 +2642,14 @@ Other minor changes
 
   cast : .(eq : m ≡ n) → Vec A m → Vec A n
   ```
+  and the type of `updateAt` has been updated from:
+  ```
+  updateAt : Fin n → (A → A) → Vec A n → Vec A n
+  ```
+  to:
+  ```
+  updateAt : Vec A n → Fin n → (A → A) → Vec A n
+  ```
 
 * Added new instance in `Data.Vec.Effectful`:
   ```agda
diff --git a/src/Data/Vec/Base.agda b/src/Data/Vec/Base.agda
index d4c0d3b580..2aeb176194 100644
--- a/src/Data/Vec/Base.agda
+++ b/src/Data/Vec/Base.agda
@@ -72,16 +72,16 @@ removeAt : Vec A (suc n) → Fin (suc n) → Vec A n
 removeAt (_ ∷ xs)     zero     = xs
 removeAt (x ∷ y ∷ xs) (suc i)  = x ∷ removeAt (y ∷ 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 _[_]%=_ _[_]≔_
 
 _[_]%=_ : 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
 
diff --git a/src/Data/Vec/Properties.agda b/src/Data/Vec/Properties.agda
index eaea4d12e3..eea2fe3d9b 100644
--- a/src/Data/Vec/Properties.agda
+++ b/src/Data/Vec/Properties.agda
@@ -229,14 +229,14 @@ lookup-inject≤-take (suc (suc m)) (s≤s (s≤s m≤m+n)) (suc (suc i)) (x ∷
 -- (+) 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
@@ -259,13 +259,13 @@ 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)
@@ -273,15 +273,15 @@ updateAt-id i xs = updateAt-id-local i xs refl
 
 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 (updateAt xs i g) i f ≡ updateAt xs i h
 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)
 
 -- 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-∘ : ∀ (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
 
 -- 3. congruence:  updateAt i  is a congruence wrt. extensional equality.
 
@@ -290,28 +290,28 @@ 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 f≗g xs = updateAt-cong-local i xs (f≗g (lookup xs i))
+-- updateAt-cong : ∀ (i : Fin n) {f g : A → A} →
+--                 f ≗ g → updateAt i f ≗ updateAt 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.
 
 -- 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 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)
+-- 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 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)
 
 -- lookup after updateAt reduces.
 
@@ -319,14 +319,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))
 
@@ -335,11 +335,11 @@ lookup∘updateAt′ i j xs i≢j =
 []%=-id : ∀ (xs : Vec A n) (i : Fin n) → xs [ i ]%= id ≡ xs
 []%=-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 : Vec A n) (i : Fin n) {f g : A → A} →
+--      xs [ i ]%= f
+--         [ i ]%= g
+--    ≡ xs [ i ]%= g ∘ f
+-- []%=-∘ xs i = updateAt-∘ i xs
 
 
 ------------------------------------------------------------------------
@@ -348,13 +348,13 @@ lookup∘updateAt′ i j xs i≢j =
 -- _[_]≔_ is defined in terms of updateAt, and all of its properties
 -- 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
+-- []≔-idempotent : ∀ (xs : Vec A n) (i : Fin n) →
+--                  (xs [ i ]≔ x) [ i ]≔ y ≡ xs [ i ]≔ y
+-- []≔-idempotent xs i = updateAt-∘ i xs
 
-[]≔-commutes : ∀ (xs : Vec A n) (i j : Fin n) → i ≢ j →
-               (xs [ i ]≔ x) [ j ]≔ y ≡ (xs [ j ]≔ y) [ i ]≔ x
-[]≔-commutes xs i j i≢j = updateAt-commutes j i (i≢j ∘ sym) xs
+-- []≔-commutes : ∀ (xs : Vec A n) (i j : Fin n) → i ≢ j →
+--                (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
 []≔-updates xs i = updateAt-updates i xs (lookup⇒[]= i xs refl)
@@ -440,7 +440,7 @@ 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)
 
@@ -1272,11 +1272,11 @@ updateAt-compose-relative = updateAt-∘-local
 Please use updateAt-∘-local instead."
 #-}
 
-updateAt-compose = updateAt-∘
-{-# WARNING_ON_USAGE updateAt-compose
-"Warning: updateAt-compose was deprecated in v2.0.
-Please use updateAt-∘ instead."
-#-}
+-- updateAt-compose = updateAt-∘
+-- {-# WARNING_ON_USAGE updateAt-compose
+-- "Warning: updateAt-compose was deprecated in v2.0.
+-- Please use updateAt-∘ instead."
+-- #-}
 
 updateAt-cong-relative = updateAt-cong-local
 {-# WARNING_ON_USAGE updateAt-cong-relative
@@ -1284,11 +1284,11 @@ updateAt-cong-relative = updateAt-cong-local
 Please use updateAt-cong-local instead."
 #-}
 
-[]%=-compose = []%=-∘
-{-# WARNING_ON_USAGE []%=-compose
-"Warning: []%=-compose was deprecated in v2.0.
-Please use []%=-∘ instead."
-#-}
+-- []%=-compose = []%=-∘
+-- {-# WARNING_ON_USAGE []%=-compose
+-- "Warning: []%=-compose was deprecated in v2.0.
+-- Please use []%=-∘ instead."
+-- #-}
 
 []≔-++-inject+ : ∀ {m n x} (xs : Vec A m) (ys : Vec A n) i →
                  (xs ++ ys) [ i ↑ˡ n ]≔ x ≡ (xs [ i ]≔ x) ++ ys

From fb7ce786d3b323136ffb95235fea0d1b197ff1d4 Mon Sep 17 00:00:00 2001
From: Saransh Chopra <saransh0701@gmail.com>
Date: Tue, 19 Sep 2023 19:46:41 +0530
Subject: [PATCH 18/21] Better removeAt

---
 src/Data/Vec/Base.agda | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/src/Data/Vec/Base.agda b/src/Data/Vec/Base.agda
index 92db28e33a..382955786e 100644
--- a/src/Data/Vec/Base.agda
+++ b/src/Data/Vec/Base.agda
@@ -69,8 +69,8 @@ insertAt xs       zero     v = v ∷ xs
 insertAt (x ∷ xs) (suc i)  v = x ∷ insertAt xs i v
 
 removeAt : Vec A (suc n) → Fin (suc n) → Vec A n
-removeAt (_ ∷ xs)     zero     = xs
-removeAt (x ∷ y ∷ xs) (suc i)  = x ∷ removeAt (y ∷ xs) i
+removeAt (x ∷ xs)         zero    = xs
+removeAt (x ∷ xs@(_ ∷ _)) (suc i) = x ∷ removeAt xs i
 
 updateAt : Vec A n → Fin n → (A → A) → Vec A n
 updateAt (x ∷ xs) zero    f = f x ∷ xs
@@ -270,7 +270,7 @@ drop m xs = proj₁ (proj₂ (splitAt m xs))
 group : ∀ n k (xs : Vec A (n * k)) →
         ∃ λ (xss : Vec (Vec A k) n) → xs ≡ concat xss
 group zero    k []                  = ([] , refl)
-group (suc n) k xs  = 
+group (suc n) k xs  =
   let ys , zs , eq-split = splitAt k xs in
   let zss , eq-group     = group n k zs in
    (ys ∷ zss) , trans eq-split (cong (ys ++_) eq-group)

From 5735cb12c9602ea4b94abd12f8abc0010cd19540 Mon Sep 17 00:00:00 2001
From: MatthewDaggitt <matthewdaggitt@gmail.com>
Date: Tue, 3 Oct 2023 11:20:26 +0900
Subject: [PATCH 19/21] Push through Vec.Functional as well

---
 CHANGELOG.md                                  |  72 +++++--
 .../Properties/CommutativeMonoid/Sum.agda     |   8 +-
 src/Data/Vec/Functional.agda                  |  92 ++++----
 src/Data/Vec/Functional/Properties.agda       | 202 ++++++++++--------
 src/Data/Vec/Properties.agda                  |  84 ++++----
 5 files changed, 270 insertions(+), 188 deletions(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 134e0074b5..e6daa01523 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -763,6 +763,49 @@ Non-backwards compatible changes
   IO.Instances
   ```
 
+### Standardisation of `insertAt`/`updateAt`/`removeAt`
+
+* The names and argument order of insertion, update and removal functions for various types of lists and vectors was previously wildly inconsistent.
+
+* To fix this they have all been standardised to the names `insertAt`/`updateAt`/`removeAt`.
+
+* Correspondingly the following changes have occurred:
+
+* In `Data.List.Base` we've 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 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.
+
 ### Other
 
 * In accordance with changes to the flags in Agda 2.6.3, all modules that previously used
@@ -1285,8 +1328,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
   ```
 
@@ -1429,8 +1472,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    ↦  []%=-∘
@@ -1443,9 +1486,10 @@ Deprecated names
   take-drop-id  ↦  take++drop≡id
 
   map-insert       ↦  map-insertAt
+  
   insert-lookup    ↦  insertAt-lookup
   insert-punchIn   ↦  insertAt-punchIn
-  remove-PunchOut  ↦ removeAt-punchOut
+  remove-PunchOut  ↦  removeAt-punchOut
   remove-insert    ↦  removeAt-insertAt
   insert-remove    ↦  insertAt-removeAt
   ```
@@ -1461,11 +1505,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`
 
@@ -2646,14 +2696,6 @@ Additions to existing modules
 
   cast : .(eq : m ≡ n) → Vec A m → Vec A n
   ```
-  and the type of `updateAt` has been updated from:
-  ```
-  updateAt : Fin n → (A → A) → Vec A n → Vec A n
-  ```
-  to:
-  ```
-  updateAt : Vec A n → Fin n → (A → A) → Vec A n
-  ```
 
 * Added new instance in `Data.Vec.Effectful`:
   ```agda
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/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 f0fdc3a249..0517db6c1f 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)
@@ -224,17 +224,17 @@ 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 (updateAt xs i g) i f ≡ updateAt xs i h
-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.
 
@@ -249,22 +249,22 @@ updateAt-cong-local (suc i) (x ∷ xs) f=g = cong (x ∷_) (updateAt-cong-local
 
 -- 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 f≗g xs = updateAt-cong-local i xs (f≗g (lookup xs i))
+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.
 
 -- 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 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)
+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)
 
 -- lookup after updateAt reduces.
 
@@ -288,11 +288,11 @@ lookup∘updateAt′ i j xs i≢j =
 []%=-id : ∀ (xs : Vec A n) (i : Fin n) → xs [ i ]%= id ≡ xs
 []%=-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 : Vec A n) (i : Fin n) {f g : A → A} →
+      xs [ i ]%= f
+         [ i ]%= g
+    ≡ xs [ i ]%= g ∘ f
+[]%=-∘ xs i = updateAt-updateAt i xs
 
 
 ------------------------------------------------------------------------
@@ -301,13 +301,13 @@ lookup∘updateAt′ i j xs i≢j =
 -- _[_]≔_ is defined in terms of updateAt, and all of its properties
 -- 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
+[]≔-idempotent : ∀ (xs : Vec A n) (i : Fin n) →
+                  (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
--- []≔-commutes xs i j i≢j = updateAt-commutes j i (i≢j ∘ sym) xs
+[]≔-commutes : ∀ (xs : Vec A n) (i j : Fin n) → i ≢ j →
+                (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
 []≔-updates xs i = updateAt-updates i xs (lookup⇒[]= i xs refl)
@@ -1219,17 +1219,17 @@ 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-∘
--- {-# WARNING_ON_USAGE updateAt-compose
--- "Warning: updateAt-compose was deprecated in v2.0.
--- Please use updateAt-∘ instead."
--- #-}
+updateAt-compose = updateAt-updateAt
+{-# WARNING_ON_USAGE updateAt-compose
+"Warning: updateAt-compose was deprecated in v2.0.
+Please use updateAt-updateAt instead."
+#-}
 
 updateAt-cong-relative = updateAt-cong-local
 {-# WARNING_ON_USAGE updateAt-cong-relative
@@ -1237,11 +1237,11 @@ updateAt-cong-relative = updateAt-cong-local
 Please use updateAt-cong-local instead."
 #-}
 
--- []%=-compose = []%=-∘
--- {-# WARNING_ON_USAGE []%=-compose
--- "Warning: []%=-compose was deprecated in v2.0.
--- Please use []%=-∘ instead."
--- #-}
+[]%=-compose = []%=-∘
+{-# WARNING_ON_USAGE []%=-compose
+"Warning: []%=-compose was deprecated in v2.0.
+Please use []%=-∘ instead."
+#-}
 
 []≔-++-inject+ : ∀ {m n x} (xs : Vec A m) (ys : Vec A n) i →
                  (xs ++ ys) [ i ↑ˡ n ]≔ x ≡ (xs [ i ]≔ x) ++ ys

From 9d376e6e3cdfa1a1af731bd444c1d59549a53659 Mon Sep 17 00:00:00 2001
From: MatthewDaggitt <matthewdaggitt@gmail.com>
Date: Tue, 3 Oct 2023 11:34:43 +0900
Subject: [PATCH 20/21] Fix CHANGELOG

---
 CHANGELOG.md | 14 +++++---------
 1 file changed, 5 insertions(+), 9 deletions(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 608996634f..0dc0637921 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -799,20 +799,20 @@ Non-backwards compatible changes
 
 ### Standardisation of `insertAt`/`updateAt`/`removeAt`
 
-* The names and argument order of insertion, update and removal functions for various types of lists and vectors was previously wildly inconsistent.
+* 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 they have all been standardised to the names `insertAt`/`updateAt`/`removeAt`.
+* To fix this the names have all been standardised to `insertAt`/`updateAt`/`removeAt`.
 
 * Correspondingly the following changes have occurred:
 
-* In `Data.List.Base` we've added:
+* 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 deprecated
+  and the following has been deprecated
   ```
   _─_ ↦ removeAt
   ```
@@ -1574,7 +1574,6 @@ Deprecated names
   idIsFold        ↦ id-is-foldr
   sum-++-commute  ↦ sum-++
 
-<<<<<<< HEAD
   take-drop-id  ↦  take++drop≡id
 
   map-insert       ↦  map-insertAt
@@ -1584,11 +1583,8 @@ Deprecated names
   remove-PunchOut  ↦  removeAt-punchOut
   remove-insert    ↦  removeAt-insertAt
   insert-remove    ↦  insertAt-removeAt
-=======
-  take-drop-id ↦ take++drop≡id
 
   lookup-inject≤-take ↦ lookup-take-inject≤
->>>>>>> master
   ```
   and the type of the proof `zipWith-comm` has been generalised from:
   ```

From e530fef0d64d770ba9b9e1074f19abaee22a06d8 Mon Sep 17 00:00:00 2001
From: MatthewDaggitt <matthewdaggitt@gmail.com>
Date: Tue, 3 Oct 2023 11:35:20 +0900
Subject: [PATCH 21/21] Another CHANGELOG fix

---
 CHANGELOG.md | 4 +---
 1 file changed, 1 insertion(+), 3 deletions(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 0dc0637921..f787065436 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -2918,15 +2918,13 @@ 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
 
-<<<<<<< HEAD
   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)
   lookup-take-inject≤ : lookup (take m xs) i ≡ lookup xs (Fin.inject≤ i (m≤m+n m n))
->>>>>>> master
   ```
 
 * Added new proofs in `Data.Vec.Membership.Propositional.Properties`: