From e23bb4b10594feed721b184eaad8b62b09ea0d8f Mon Sep 17 00:00:00 2001
From: e-mniang <mariam.niang.etu@gmail.com>
Date: Wed, 30 Jul 2025 14:11:38 -0400
Subject: [PATCH 1/6] adding truncate's properties

---
 src/Data/Vec/Properties.agda | 89 ++++++++++++++++++++++++++++++++++--
 1 file changed, 86 insertions(+), 3 deletions(-)

diff --git a/src/Data/Vec/Properties.agda b/src/Data/Vec/Properties.agda
index 73459b360f..ba91a76dbb 100644
--- a/src/Data/Vec/Properties.agda
+++ b/src/Data/Vec/Properties.agda
@@ -11,14 +11,14 @@ module Data.Vec.Properties where
 open import Algebra.Definitions
 open import Data.Bool.Base using (true; false)
 open import Data.Fin.Base as Fin
-  using (Fin; zero; suc; toℕ; fromℕ<; _↑ˡ_; _↑ʳ_)
+  using (Fin; zero; suc; toℕ; fromℕ<; _↑ˡ_; _↑ʳ_; inject≤)
 open import Data.List.Base as List using (List)
 import Data.List.Properties as List
 open import Data.Nat.Base
-  using (ℕ; zero; suc; _+_; _≤_; _<_; s≤s; pred; s<s⁻¹; _≥_; s≤s⁻¹; z≤n)
+  using (ℕ; zero; suc; _+_; _≤_; _<_; s≤s; pred; s<s⁻¹; _≥_; s≤s⁻¹; z≤n; _∸_)
 open import Data.Nat.Properties
   using (+-assoc; m≤n⇒m≤1+n; m≤m+n; ≤-refl; ≤-trans; ≤-irrelevant; ≤⇒≤″
-        ; suc-injective; +-comm; +-suc; +-identityʳ)
+        ; suc-injective; +-comm; +-suc; +-identityʳ; m≤n⇒∃[o]m+o≡n)
 open import Data.Product.Base as Product
   using (_×_; _,_; proj₁; proj₂; <_,_>; uncurry)
 open import Data.Sum.Base using ([_,_]′)
@@ -104,6 +104,11 @@ take-map : ∀ (f : A → B) (m : ℕ) (xs : Vec A (m + n)) →
 take-map f zero    xs       = refl
 take-map f (suc m) (x ∷ xs) = cong (f x ∷_) (take-map f m xs)
 
+take-updateAt : (f : A → A) {m n : ℕ} (xs : Vec A (m + n)) (i : Fin m) →
+                updateAt (take m xs) i f ≡ take m (updateAt xs (inject≤ i (m≤m+n m n)) f)
+take-updateAt f (_ ∷ _ ) zero    = refl
+take-updateAt f (x ∷ xs) (suc i) = cong (x ∷_) (take-updateAt f xs i)
+
 ------------------------------------------------------------------------
 -- drop
 
@@ -154,6 +159,70 @@ take≡truncate : ∀ m (xs : Vec A (m + n)) →
 take≡truncate zero    _        = refl
 take≡truncate (suc m) (x ∷ xs) = cong (x ∷_) (take≡truncate m xs)
 
+truncate-zipWith : (f : A → B → C) (m≤n : m ≤ n) (xs : Vec A n) (ys : Vec B n) →
+  truncate m≤n (zipWith f xs ys) ≡ zipWith f (truncate m≤n xs) (truncate m≤n ys)
+truncate-zipWith f z≤n xs ys = refl
+truncate-zipWith f (s≤s m≤n) (x ∷ xs) (y ∷ ys) =
+  cong (f x y ∷_) (truncate-zipWith f m≤n xs ys)
+
+truncate-zipWith-truncate : ∀ (f : A → B → C) (o≤m : o ≤ m) (m≤n : m ≤ n)
+  (xs : Vec A n) (ys : Vec B m) →
+  let o≤n = ≤-trans o≤m m≤n in
+  truncate o≤m (zipWith f (truncate m≤n xs) ys) ≡
+  zipWith f (truncate o≤n xs) (truncate o≤m ys)
+truncate-zipWith-truncate f o≤m m≤n xs ys =
+  let o≤n = ≤-trans o≤m m≤n in
+  trans (truncate-zipWith f o≤m (truncate m≤n xs) ys)
+  (cong (λ zs → zipWith f zs (truncate o≤m ys)) ((sym (truncate-trans o≤m m≤n xs))))
+
+zipWith-truncate : ∀ (f : A → B → C) {p q : ℕ} (xs : Vec A (p + q)) (ys : Vec B (p + q)) →
+  let p≤p+q = m≤m+n p q in
+  zipWith f (truncate p≤p+q xs) (truncate p≤p+q ys) ≡ truncate p≤p+q (zipWith f xs ys)
+zipWith-truncate f {p} {q} xs ys =
+  let p≤p+q = m≤m+n p q in
+  begin
+    zipWith f (truncate p≤p+q xs) (truncate p≤p+q ys) ≡⟨ cong₂ (zipWith f) (take≡truncate p xs) (take≡truncate p ys) ⟨
+    zipWith f (take p xs) (take p ys)                 ≡⟨ take-zipWith f xs ys ⟨
+    take p (zipWith f xs ys)                          ≡⟨ take≡truncate p (zipWith f xs ys) ⟩
+    truncate p≤p+q (zipWith f xs ys) ∎ where open ≡-Reasoning
+
+module _  (f : A → B → C) {o m n : ℕ} (xs : Vec A (o + m + n)) (ys : Vec B (o + m)) where
+  private
+    o≤o+m = m≤m+n o m
+    o+m≤o+m+n = m≤m+n (o + m) n
+    o≤o+m+n = ≤-trans (m≤m+n o m) (m≤m+n (o + m) n)
+
+  zipWith-truncate₁ : zipWith f (truncate o≤o+m+n xs) (truncate (o≤o+m) ys) ≡
+    truncate (o≤o+m) (zipWith f (truncate (o+m≤o+m+n) xs) ys)
+  zipWith-truncate₁ =
+    trans (cong (λ zs → zipWith f zs (truncate (o≤o+m) ys)) (truncate-trans (o≤o+m) (o+m≤o+m+n) xs))
+    (zipWith-truncate f (truncate (o+m≤o+m+n) xs) ys)
+
+truncate-updateAt : (f : A → A) (m≤n : m ≤ n) (xs : Vec A n) (i : Fin m) →
+                    updateAt (truncate m≤n xs) i f ≡ truncate m≤n (updateAt xs (inject≤ i m≤n) f)
+truncate-updateAt f (s≤s _  ) (_ ∷ _ ) zero = refl
+truncate-updateAt f (s≤s m≤n) (x ∷ xs) (suc i) = cong (x ∷_) (truncate-updateAt f m≤n xs i)
+
+module _  (f : A → A) {p q : ℕ} (xs : Vec A (p + q)) (i : Fin p) where
+  private
+    p≤p+q : p ≤ p + q
+    p≤p+q = m≤m+n p q
+    i′ : Fin (p + q)
+    i′ = inject≤ i p≤p+q
+  
+  updateAt-truncate : updateAt (truncate p≤p+q xs) i f ≡ truncate p≤p+q (updateAt xs i′ f)
+  updateAt-truncate = begin
+    updateAt (truncate p≤p+q xs) i f ≡⟨ cong (λ l → updateAt l i f) (sym (take≡truncate p xs)) ⟩
+    updateAt (take p xs) i f          ≡⟨ take-updateAt f xs i ⟩
+    take p (updateAt xs i′ f)         ≡⟨ take≡truncate p (updateAt xs i′ f) ⟩
+    truncate p≤p+q (updateAt xs i′ f) ∎ where open ≡-Reasoning
+
+truncate++drop≡id : (xs : Vec A (m + n)) → truncate (m≤m+n m n) xs ++ drop m xs ≡ xs
+truncate++drop≡id {m = m} {n} xs = begin
+  truncate (m≤m+n m n) xs ++ drop m xs ≡⟨ cong (_++ drop m xs) (take≡truncate m xs) ⟨
+  take m xs ++ drop m xs               ≡⟨ take++drop≡id m xs ⟩
+  xs ∎ where open ≡-Reasoning
+
 ------------------------------------------------------------------------
 -- pad
 
@@ -472,6 +541,20 @@ toList-map : ∀ (f : A → B) (xs : Vec A n) →
 toList-map f [] = refl
 toList-map f (x ∷ xs) = cong (f x List.∷_) (toList-map f xs)
 
+truncate-map : (f : A → B) (m : ℕ) (m≤n : m ≤ n) (xs : Vec A n) →
+  map f (truncate m≤n xs) ≡ truncate m≤n (map f xs)
+truncate-map {n = n} f m m≤n xs =
+  begin
+    map f (truncate m≤n xs)     ≡⟨ cong (map f) (truncate≡take m≤n xs eq) ⟩
+    map f (take m (cast eq xs)) ≡⟨ take-map f m _ ⟨
+    take m (map f (cast eq xs)) ≡⟨ cong (take m) (map-cast f eq xs) ⟩
+    take m (cast eq (map f xs)) ≡⟨ truncate≡take m≤n (map f xs) eq ⟨
+    truncate m≤n (map f xs) ∎
+ where
+   .eq : n ≡ m + (n ∸ m)
+   eq = sym (proj₂ (m≤n⇒∃[o]m+o≡n m≤n))
+   open ≡-Reasoning
+
 ------------------------------------------------------------------------
 -- _++_
 

From ead92ababd201ef2c8b7ef69465ee2a95c19aac0 Mon Sep 17 00:00:00 2001
From: e-mniang <mariam.niang.etu@gmail.com>
Date: Wed, 30 Jul 2025 14:42:57 -0400
Subject: [PATCH 2/6] update changelog

---
 CHANGELOG.md                 | 28 ++++++++++++++++++++++++++++
 src/Data/Vec/Properties.agda |  4 ++--
 2 files changed, 30 insertions(+), 2 deletions(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 2ebee679df..402ea28068 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -43,3 +43,31 @@ Additions to existing modules
   ∸-suc : m ≤ n → suc n ∸ m ≡ suc (n ∸ m)
   ```
 
+* In `Data.Vec.Properties`:
+  ```agda
+  take-updateAt : (f : A → A) {m n : ℕ} (xs : Vec A (m + n)) (i : Fin m) →
+    updateAt (take m xs) i f ≡ take m (updateAt xs (inject≤ i (m≤m+n m n)) f)
+  
+  truncate-zipWith : (f : A → B → C) (m≤n : m ≤ n) (xs : Vec A n) (ys : Vec B n) →
+    truncate m≤n (zipWith f xs ys) ≡ zipWith f (truncate m≤n xs) (truncate m≤n ys)
+  
+  truncate-zipWith-truncate : truncate o≤m (zipWith f (truncate m≤n xs) ys) ≡
+    zipWith f (truncate o≤n xs) (truncate o≤m ys)
+
+  zipWith-truncate : zipWith f (truncate p≤p+q xs) (truncate p≤p+q ys) ≡
+    truncate p≤p+q (zipWith f xs ys)
+
+  zipWith-truncate₁ : zipWith f (truncate o≤o+m+n xs) (truncate (o≤o+m) ys) ≡
+    truncate (o≤o+m) (zipWith f (truncate (o+m≤o+m+n) xs) ys)
+  
+  truncate-updateAt : (f : A → A) (m≤n : m ≤ n) (xs : Vec A n) (i : Fin m) →
+    updateAt (truncate m≤n xs) i f ≡ truncate m≤n (updateAt xs (inject≤ i m≤n) f)
+
+  updateAt-truncate : updateAt (truncate p≤p+q xs) i f ≡ truncate p≤p+q (updateAt xs i′ f)
+
+  truncate++drop≡id : (xs : Vec A (m + n)) → truncate (m≤m+n m n) xs ++ drop m xs ≡ xs
+
+  truncate-map : (f : A → B) (m : ℕ) (m≤n : m ≤ n) (xs : Vec A n) →
+  map f (truncate m≤n xs) ≡ truncate m≤n (map f xs)
+
+  ```
\ No newline at end of file
diff --git a/src/Data/Vec/Properties.agda b/src/Data/Vec/Properties.agda
index ba91a76dbb..034f95a820 100644
--- a/src/Data/Vec/Properties.agda
+++ b/src/Data/Vec/Properties.agda
@@ -213,8 +213,8 @@ module _  (f : A → A) {p q : ℕ} (xs : Vec A (p + q)) (i : Fin p) where
   updateAt-truncate : updateAt (truncate p≤p+q xs) i f ≡ truncate p≤p+q (updateAt xs i′ f)
   updateAt-truncate = begin
     updateAt (truncate p≤p+q xs) i f ≡⟨ cong (λ l → updateAt l i f) (sym (take≡truncate p xs)) ⟩
-    updateAt (take p xs) i f          ≡⟨ take-updateAt f xs i ⟩
-    take p (updateAt xs i′ f)         ≡⟨ take≡truncate p (updateAt xs i′ f) ⟩
+    updateAt (take p xs) i f         ≡⟨ take-updateAt f xs i ⟩
+    take p (updateAt xs i′ f)        ≡⟨ take≡truncate p (updateAt xs i′ f) ⟩
     truncate p≤p+q (updateAt xs i′ f) ∎ where open ≡-Reasoning
 
 truncate++drop≡id : (xs : Vec A (m + n)) → truncate (m≤m+n m n) xs ++ drop m xs ≡ xs

From d2e46d8e3744bb0e93b53c9e1e7b826b872d13ab Mon Sep 17 00:00:00 2001
From: e-mniang <mariam.niang.etu@gmail.com>
Date: Thu, 31 Jul 2025 14:00:50 -0400
Subject: [PATCH 3/6] cleaning whitespaces

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

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 402ea28068..5659e7e36b 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -47,10 +47,10 @@ Additions to existing modules
   ```agda
   take-updateAt : (f : A → A) {m n : ℕ} (xs : Vec A (m + n)) (i : Fin m) →
     updateAt (take m xs) i f ≡ take m (updateAt xs (inject≤ i (m≤m+n m n)) f)
-  
+
   truncate-zipWith : (f : A → B → C) (m≤n : m ≤ n) (xs : Vec A n) (ys : Vec B n) →
     truncate m≤n (zipWith f xs ys) ≡ zipWith f (truncate m≤n xs) (truncate m≤n ys)
-  
+
   truncate-zipWith-truncate : truncate o≤m (zipWith f (truncate m≤n xs) ys) ≡
     zipWith f (truncate o≤n xs) (truncate o≤m ys)
 
@@ -59,7 +59,7 @@ Additions to existing modules
 
   zipWith-truncate₁ : zipWith f (truncate o≤o+m+n xs) (truncate (o≤o+m) ys) ≡
     truncate (o≤o+m) (zipWith f (truncate (o+m≤o+m+n) xs) ys)
-  
+
   truncate-updateAt : (f : A → A) (m≤n : m ≤ n) (xs : Vec A n) (i : Fin m) →
     updateAt (truncate m≤n xs) i f ≡ truncate m≤n (updateAt xs (inject≤ i m≤n) f)
 
diff --git a/src/Data/Vec/Properties.agda b/src/Data/Vec/Properties.agda
index 034f95a820..d12988ac9d 100644
--- a/src/Data/Vec/Properties.agda
+++ b/src/Data/Vec/Properties.agda
@@ -209,7 +209,7 @@ module _  (f : A → A) {p q : ℕ} (xs : Vec A (p + q)) (i : Fin p) where
     p≤p+q = m≤m+n p q
     i′ : Fin (p + q)
     i′ = inject≤ i p≤p+q
-  
+
   updateAt-truncate : updateAt (truncate p≤p+q xs) i f ≡ truncate p≤p+q (updateAt xs i′ f)
   updateAt-truncate = begin
     updateAt (truncate p≤p+q xs) i f ≡⟨ cong (λ l → updateAt l i f) (sym (take≡truncate p xs)) ⟩

From fd1d7f206e3d40e99a205fab0ea7679816e3f9d9 Mon Sep 17 00:00:00 2001
From: e-mniang <mariam.niang.etu@gmail.com>
Date: Fri, 1 Aug 2025 20:37:39 -0400
Subject: [PATCH 4/6] Recleaning

---
 CHANGELOG.md | 12 ++++++------
 1 file changed, 6 insertions(+), 6 deletions(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 5659e7e36b..bd67221cd4 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -46,22 +46,22 @@ Additions to existing modules
 * In `Data.Vec.Properties`:
   ```agda
   take-updateAt : (f : A → A) {m n : ℕ} (xs : Vec A (m + n)) (i : Fin m) →
-    updateAt (take m xs) i f ≡ take m (updateAt xs (inject≤ i (m≤m+n m n)) f)
+  updateAt (take m xs) i f ≡ take m (updateAt xs (inject≤ i (m≤m+n m n)) f)
 
   truncate-zipWith : (f : A → B → C) (m≤n : m ≤ n) (xs : Vec A n) (ys : Vec B n) →
-    truncate m≤n (zipWith f xs ys) ≡ zipWith f (truncate m≤n xs) (truncate m≤n ys)
+  truncate m≤n (zipWith f xs ys) ≡ zipWith f (truncate m≤n xs) (truncate m≤n ys)
 
   truncate-zipWith-truncate : truncate o≤m (zipWith f (truncate m≤n xs) ys) ≡
-    zipWith f (truncate o≤n xs) (truncate o≤m ys)
+  zipWith f (truncate o≤n xs) (truncate o≤m ys)
 
   zipWith-truncate : zipWith f (truncate p≤p+q xs) (truncate p≤p+q ys) ≡
-    truncate p≤p+q (zipWith f xs ys)
+  truncate p≤p+q (zipWith f xs ys)
 
   zipWith-truncate₁ : zipWith f (truncate o≤o+m+n xs) (truncate (o≤o+m) ys) ≡
-    truncate (o≤o+m) (zipWith f (truncate (o+m≤o+m+n) xs) ys)
+  truncate (o≤o+m) (zipWith f (truncate (o+m≤o+m+n) xs) ys)
 
   truncate-updateAt : (f : A → A) (m≤n : m ≤ n) (xs : Vec A n) (i : Fin m) →
-    updateAt (truncate m≤n xs) i f ≡ truncate m≤n (updateAt xs (inject≤ i m≤n) f)
+  updateAt (truncate m≤n xs) i f ≡ truncate m≤n (updateAt xs (inject≤ i m≤n) f)
 
   updateAt-truncate : updateAt (truncate p≤p+q xs) i f ≡ truncate p≤p+q (updateAt xs i′ f)
 

From ac32928e798b5deda1e5ba3804eb99579a789ecb Mon Sep 17 00:00:00 2001
From: e-mniang <mariam.niang.etu@gmail.com>
Date: Wed, 6 Aug 2025 14:47:59 -0400
Subject: [PATCH 5/6] corrections after reviews

---
 CHANGELOG.md                 | 34 ++++++-------
 src/Data/Vec/Properties.agda | 98 ++++++++++++------------------------
 2 files changed, 47 insertions(+), 85 deletions(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index bd67221cd4..30b9ceccc8 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -45,29 +45,25 @@ Additions to existing modules
 
 * In `Data.Vec.Properties`:
   ```agda
-  take-updateAt : (f : A → A) {m n : ℕ} (xs : Vec A (m + n)) (i : Fin m) →
-  updateAt (take m xs) i f ≡ take m (updateAt xs (inject≤ i (m≤m+n m n)) f)
+  updateAt-take : (xs : Vec A (m + n)) (i : Fin m) (f : A → A) →
+                  updateAt (take m xs) i f ≡ take m (updateAt xs (inject≤ i (m≤m+n m n)) f)
 
-  truncate-zipWith : (f : A → B → C) (m≤n : m ≤ n) (xs : Vec A n) (ys : Vec B n) →
-  truncate m≤n (zipWith f xs ys) ≡ zipWith f (truncate m≤n xs) (truncate m≤n ys)
+  truncate-zipWith : (m≤n : m ≤ n) (xs : Vec A n) (ys : Vec B n) (f : A → B → C) →
+                    truncate m≤n (zipWith f xs ys) ≡ zipWith f (truncate m≤n xs) (truncate m≤n ys)
 
-  truncate-zipWith-truncate : truncate o≤m (zipWith f (truncate m≤n xs) ys) ≡
-  zipWith f (truncate o≤n xs) (truncate o≤m ys)
+  truncate-zipWith-truncate : (f : A → B → C) (m≤n : m ≤ n) (n≤o : n ≤ o) (xs : Vec A o) (ys : Vec B n) →
+                              truncate m≤n (zipWith f (truncate n≤o xs) ys) ≡
+                              zipWith f (truncate (≤-trans m≤n n≤o) xs) (truncate m≤n ys)
 
-  zipWith-truncate : zipWith f (truncate p≤p+q xs) (truncate p≤p+q ys) ≡
-  truncate p≤p+q (zipWith f xs ys)
+  truncate-updateAt : (m≤n : m ≤ n) (xs : Vec A n) (i : Fin m) (f : A → A) →
+                      updateAt (truncate m≤n xs) i f ≡
+                      truncate m≤n (updateAt xs (inject≤ i m≤n) f)
 
-  zipWith-truncate₁ : zipWith f (truncate o≤o+m+n xs) (truncate (o≤o+m) ys) ≡
-  truncate (o≤o+m) (zipWith f (truncate (o+m≤o+m+n) xs) ys)
+  updateAt-truncate : (xs : Vec A (m + n)) (i : Fin m) (f : A → A) →
+                      updateAt (truncate (m≤m+n m n) xs) i f ≡
+                      truncate (m≤m+n m n) (updateAt xs (inject≤ i (m≤m+n m n)) f)
 
-  truncate-updateAt : (f : A → A) (m≤n : m ≤ n) (xs : Vec A n) (i : Fin m) →
-  updateAt (truncate m≤n xs) i f ≡ truncate m≤n (updateAt xs (inject≤ i m≤n) f)
-
-  updateAt-truncate : updateAt (truncate p≤p+q xs) i f ≡ truncate p≤p+q (updateAt xs i′ f)
-
-  truncate++drop≡id : (xs : Vec A (m + n)) → truncate (m≤m+n m n) xs ++ drop m xs ≡ xs
-
-  truncate-map : (f : A → B) (m : ℕ) (m≤n : m ≤ n) (xs : Vec A n) →
-  map f (truncate m≤n xs) ≡ truncate m≤n (map f xs)
+  map-truncate : (f : A → B) (m≤n : m ≤ n) (xs : Vec A n) →
+                map f (truncate m≤n xs) ≡ truncate m≤n (map f xs)
 
   ```
\ No newline at end of file
diff --git a/src/Data/Vec/Properties.agda b/src/Data/Vec/Properties.agda
index d12988ac9d..05c3763aad 100644
--- a/src/Data/Vec/Properties.agda
+++ b/src/Data/Vec/Properties.agda
@@ -104,10 +104,10 @@ take-map : ∀ (f : A → B) (m : ℕ) (xs : Vec A (m + n)) →
 take-map f zero    xs       = refl
 take-map f (suc m) (x ∷ xs) = cong (f x ∷_) (take-map f m xs)
 
-take-updateAt : (f : A → A) {m n : ℕ} (xs : Vec A (m + n)) (i : Fin m) →
+updateAt-take : (xs : Vec A (m + n)) (i : Fin m) (f : A → A) →
                 updateAt (take m xs) i f ≡ take m (updateAt xs (inject≤ i (m≤m+n m n)) f)
-take-updateAt f (_ ∷ _ ) zero    = refl
-take-updateAt f (x ∷ xs) (suc i) = cong (x ∷_) (take-updateAt f xs i)
+updateAt-take (_ ∷ _ ) zero    f = refl
+updateAt-take (x ∷ xs) (suc i) f = cong (x ∷_) (updateAt-take xs i f)
 
 ------------------------------------------------------------------------
 -- drop
@@ -165,63 +165,30 @@ truncate-zipWith f z≤n xs ys = refl
 truncate-zipWith f (s≤s m≤n) (x ∷ xs) (y ∷ ys) =
   cong (f x y ∷_) (truncate-zipWith f m≤n xs ys)
 
-truncate-zipWith-truncate : ∀ (f : A → B → C) (o≤m : o ≤ m) (m≤n : m ≤ n)
-  (xs : Vec A n) (ys : Vec B m) →
-  let o≤n = ≤-trans o≤m m≤n in
-  truncate o≤m (zipWith f (truncate m≤n xs) ys) ≡
-  zipWith f (truncate o≤n xs) (truncate o≤m ys)
-truncate-zipWith-truncate f o≤m m≤n xs ys =
-  let o≤n = ≤-trans o≤m m≤n in
-  trans (truncate-zipWith f o≤m (truncate m≤n xs) ys)
-  (cong (λ zs → zipWith f zs (truncate o≤m ys)) ((sym (truncate-trans o≤m m≤n xs))))
-
-zipWith-truncate : ∀ (f : A → B → C) {p q : ℕ} (xs : Vec A (p + q)) (ys : Vec B (p + q)) →
-  let p≤p+q = m≤m+n p q in
-  zipWith f (truncate p≤p+q xs) (truncate p≤p+q ys) ≡ truncate p≤p+q (zipWith f xs ys)
-zipWith-truncate f {p} {q} xs ys =
-  let p≤p+q = m≤m+n p q in
-  begin
-    zipWith f (truncate p≤p+q xs) (truncate p≤p+q ys) ≡⟨ cong₂ (zipWith f) (take≡truncate p xs) (take≡truncate p ys) ⟨
-    zipWith f (take p xs) (take p ys)                 ≡⟨ take-zipWith f xs ys ⟨
-    take p (zipWith f xs ys)                          ≡⟨ take≡truncate p (zipWith f xs ys) ⟩
-    truncate p≤p+q (zipWith f xs ys) ∎ where open ≡-Reasoning
-
-module _  (f : A → B → C) {o m n : ℕ} (xs : Vec A (o + m + n)) (ys : Vec B (o + m)) where
-  private
-    o≤o+m = m≤m+n o m
-    o+m≤o+m+n = m≤m+n (o + m) n
-    o≤o+m+n = ≤-trans (m≤m+n o m) (m≤m+n (o + m) n)
+truncate-zipWith-truncate : ∀ (f : A → B → C) (m≤n : m ≤ n) (n≤o : n ≤ o)
+  (xs : Vec A o) (ys : Vec B n) →
+  truncate m≤n (zipWith f (truncate n≤o xs) ys) ≡
+  zipWith f (truncate (≤-trans m≤n n≤o) xs) (truncate m≤n ys)
+truncate-zipWith-truncate f m≤n n≤o xs ys =
+  trans (truncate-zipWith f m≤n (truncate n≤o xs) ys)
+  (cong (λ zs → zipWith f zs (truncate m≤n ys)) ((sym (truncate-trans m≤n n≤o xs))))
 
-  zipWith-truncate₁ : zipWith f (truncate o≤o+m+n xs) (truncate (o≤o+m) ys) ≡
-    truncate (o≤o+m) (zipWith f (truncate (o+m≤o+m+n) xs) ys)
-  zipWith-truncate₁ =
-    trans (cong (λ zs → zipWith f zs (truncate (o≤o+m) ys)) (truncate-trans (o≤o+m) (o+m≤o+m+n) xs))
-    (zipWith-truncate f (truncate (o+m≤o+m+n) xs) ys)
-
-truncate-updateAt : (f : A → A) (m≤n : m ≤ n) (xs : Vec A n) (i : Fin m) →
+truncate-updateAt : (m≤n : m ≤ n) (xs : Vec A n) (i : Fin m) (f : A → A) →
                     updateAt (truncate m≤n xs) i f ≡ truncate m≤n (updateAt xs (inject≤ i m≤n) f)
-truncate-updateAt f (s≤s _  ) (_ ∷ _ ) zero = refl
-truncate-updateAt f (s≤s m≤n) (x ∷ xs) (suc i) = cong (x ∷_) (truncate-updateAt f m≤n xs i)
+truncate-updateAt (s≤s _  ) (_ ∷ _ ) zero f = refl
+truncate-updateAt (s≤s m≤n) (x ∷ xs) (suc i) f = cong (x ∷_) (truncate-updateAt m≤n xs i f)
 
-module _  (f : A → A) {p q : ℕ} (xs : Vec A (p + q)) (i : Fin p) where
+module _ (xs : Vec A (m + n)) (i : Fin m) (f : A → A) where
   private
-    p≤p+q : p ≤ p + q
-    p≤p+q = m≤m+n p q
-    i′ : Fin (p + q)
-    i′ = inject≤ i p≤p+q
+    i′ = inject≤ i (m≤m+n m n)
 
-  updateAt-truncate : updateAt (truncate p≤p+q xs) i f ≡ truncate p≤p+q (updateAt xs i′ f)
+  updateAt-truncate : updateAt (truncate (m≤m+n m n) xs) i f ≡ truncate (m≤m+n m n) (updateAt xs i′ f)
   updateAt-truncate = begin
-    updateAt (truncate p≤p+q xs) i f ≡⟨ cong (λ l → updateAt l i f) (sym (take≡truncate p xs)) ⟩
-    updateAt (take p xs) i f         ≡⟨ take-updateAt f xs i ⟩
-    take p (updateAt xs i′ f)        ≡⟨ take≡truncate p (updateAt xs i′ f) ⟩
-    truncate p≤p+q (updateAt xs i′ f) ∎ where open ≡-Reasoning
-
-truncate++drop≡id : (xs : Vec A (m + n)) → truncate (m≤m+n m n) xs ++ drop m xs ≡ xs
-truncate++drop≡id {m = m} {n} xs = begin
-  truncate (m≤m+n m n) xs ++ drop m xs ≡⟨ cong (_++ drop m xs) (take≡truncate m xs) ⟨
-  take m xs ++ drop m xs               ≡⟨ take++drop≡id m xs ⟩
-  xs ∎ where open ≡-Reasoning
+    updateAt (truncate (m≤m+n m n) xs) i f ≡⟨ cong (λ l → updateAt l i f) (take≡truncate m xs) ⟨
+    updateAt (take m xs) i f         ≡⟨ updateAt-take xs i f ⟩
+    take m (updateAt xs i′ f)        ≡⟨ take≡truncate m (updateAt xs i′ f) ⟩
+    truncate (m≤m+n m n) (updateAt xs i′ f) ∎
+    where open ≡-Reasoning
 
 ------------------------------------------------------------------------
 -- pad
@@ -541,19 +508,18 @@ toList-map : ∀ (f : A → B) (xs : Vec A n) →
 toList-map f [] = refl
 toList-map f (x ∷ xs) = cong (f x List.∷_) (toList-map f xs)
 
-truncate-map : (f : A → B) (m : ℕ) (m≤n : m ≤ n) (xs : Vec A n) →
+map-truncate : (f : A → B) (m≤n : m ≤ n) (xs : Vec A n) →
   map f (truncate m≤n xs) ≡ truncate m≤n (map f xs)
-truncate-map {n = n} f m m≤n xs =
-  begin
-    map f (truncate m≤n xs)     ≡⟨ cong (map f) (truncate≡take m≤n xs eq) ⟩
-    map f (take m (cast eq xs)) ≡⟨ take-map f m _ ⟨
-    take m (map f (cast eq xs)) ≡⟨ cong (take m) (map-cast f eq xs) ⟩
-    take m (cast eq (map f xs)) ≡⟨ truncate≡take m≤n (map f xs) eq ⟨
-    truncate m≤n (map f xs) ∎
- where
-   .eq : n ≡ m + (n ∸ m)
-   eq = sym (proj₂ (m≤n⇒∃[o]m+o≡n m≤n))
-   open ≡-Reasoning
+map-truncate {m = m} {n = n} f m≤n xs =
+  let _ , n≡m+o = m≤n⇒∃[o]m+o≡n m≤n
+  in begin
+    map f (truncate m≤n xs)              ≡⟨ cong (map f) (truncate≡take m≤n xs (sym n≡m+o)) ⟩
+    map f (take m (cast (sym n≡m+o) xs)) ≡⟨ sym (take-map f m _) ⟩
+    take m (map f (cast (sym n≡m+o) xs)) ≡⟨ cong (take m) (map-cast f (sym n≡m+o) xs) ⟩
+    take m (cast (sym n≡m+o) (map f xs)) ≡⟨ sym (truncate≡take m≤n (map f xs) (sym n≡m+o)) ⟩
+    truncate m≤n (map f xs)              ∎
+  where
+    open ≡-Reasoning
 
 ------------------------------------------------------------------------
 -- _++_

From 56b9f0b790bef6a5b02d4749bca6f7bca570edc3 Mon Sep 17 00:00:00 2001
From: e-mniang <mariam.niang.etu@gmail.com>
Date: Sun, 10 Aug 2025 08:30:38 -0400
Subject: [PATCH 6/6] correction of changelog

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

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 30b9ceccc8..7fab16fe8f 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -48,7 +48,7 @@ Additions to existing modules
   updateAt-take : (xs : Vec A (m + n)) (i : Fin m) (f : A → A) →
                   updateAt (take m xs) i f ≡ take m (updateAt xs (inject≤ i (m≤m+n m n)) f)
 
-  truncate-zipWith : (m≤n : m ≤ n) (xs : Vec A n) (ys : Vec B n) (f : A → B → C) →
+  truncate-zipWith : (f : A → B → C) (m≤n : m ≤ n) (xs : Vec A n) (ys : Vec B n) →
                     truncate m≤n (zipWith f xs ys) ≡ zipWith f (truncate m≤n xs) (truncate m≤n ys)
 
   truncate-zipWith-truncate : (f : A → B → C) (m≤n : m ≤ n) (n≤o : n ≤ o) (xs : Vec A o) (ys : Vec B n) →