Update matrices and vectors

9 files changed, 423 insertions, 142 deletions

diff --git a/Data/Vector/Bifunctor.agda b/Data/Vector/Bifunctor.agda
new file mode 100644
index 0000000..51e8970
--- /dev/null
+++ b/Data/Vector/Bifunctor.agda
@@ -0,0 +1,57 @@
+{-# OPTIONS --without-K --safe #-}
+
+open import Level using (Level)
+
+module Data.Vector.Bifunctor {c : Level} where
+
+open import Categories.Category.Instance.Nat using (Natop)
+open import Categories.Category.Instance.Sets using (Sets)
+open import Categories.Functor.Bifunctor using (Bifunctor)
+open import Function using (_∘_)
+open import Data.Nat using (ℕ)
+open import Data.Fin using (Fin)
+open import Data.Product using (_,_)
+open import Data.Vec using (Vec; map; tabulate; lookup)
+open import Data.Vec.Properties using (map-id; map-∘; map-cong; tabulate∘lookup; lookup∘tabulate; tabulate-cong; lookup-map; tabulate-∘)
+open import Relation.Binary.PropositionalEquality as ≡ using (_≡_; module ≡-Reasoning)
+
+naturality
+    : {A B : Set c} {f : A → B} {n m : ℕ} {g : Fin m → Fin n} (v : Vec A n)
+    → map f (tabulate (λ i → lookup v (g i))) ≡ tabulate (λ i → lookup (map f v) (g i))
+naturality {A} {B} {f} {n} {m} {g} v = begin
+    map f (tabulate (λ i → lookup v (g i))) ≡⟨ tabulate-∘ f (λ i → lookup v (g i)) ⟨
+    tabulate (λ i → f (lookup v (g i)))     ≡⟨ tabulate-cong (λ i → (lookup-map (g i) f v)) ⟨
+    tabulate (λ i → lookup (map f v) (g i)) ∎
+  where
+    open ≡-Reasoning
+
+bimap : {A B : Set c} {n m : ℕ} (f : A → B) (g : Fin m → Fin n) → Vec A n → Vec B m
+bimap f g v = map f (tabulate (λ i → lookup v (g i)))
+
+Vec₂ : Bifunctor (Sets c) Natop (Sets c)
+Vec₂ = record
+    { F₀ = λ (A , n) → Vec A n
+    ; F₁ = λ (f , g) v → bimap f g v
+    ; identity = λ v → ≡.trans (map-id (tabulate (λ i → lookup v i))) (tabulate∘lookup v)
+    ; homomorphism = λ {_ _ _} {(f , f′)} {(g , g′)} → homomorphism f g f′ g′
+    ; F-resp-≈ = λ (f≗g , f′≗g′) v → ≡.trans (map-cong f≗g (tabulate (λ i → lookup v _))) (≡.cong (map _) (tabulate-cong (λ i → (≡.cong (lookup v) (f′≗g′ i)))))
+    }
+  where
+    homomorphism
+        : {X Y Z : Set c}
+          (f : X → Y)
+          (g : Y → Z)
+          {x y z : ℕ}
+          (f′ : Fin y → Fin x)
+          (g′ : Fin z → Fin y)
+          (v : Vec X x)
+        → bimap (g ∘ f) (f′ ∘ g′) v ≡ bimap g g′ (bimap f f′ v)
+    homomorphism f g f′ g′ v = begin
+        map (g ∘ f) (tabulate (λ i → lookup v (f′ (g′ i))))   ≡⟨ map-∘ g f (tabulate (λ i → lookup v (f′ (g′ i)))) ⟩
+        map g (map f (tabulate (λ i → lookup v (f′ (g′ i))))) ≡⟨ ≡.cong (map g) (naturality v) ⟩
+        map g (tabulate (λ i → lookup (map f v) (f′ (g′ i)))) ≡⟨ ≡.cong (map g) (tabulate-cong (λ i → (lookup∘tabulate (λ i₁ → lookup (map f v) (f′ i₁)) (g′ i)))) ⟨
+        map g (tabulate (λ i → lookup (tabulate (λ i₁ → lookup (map f v) (f′ i₁))) (g′ i)))
+            ≡⟨ ≡.cong (map g) (tabulate-cong (λ i → ≡.cong (λ h → lookup h (g′ i)) (naturality v))) ⟨
+        map g (tabulate (λ i → lookup (map f (tabulate (λ i₁ → lookup v (f′ i₁)))) (g′ i))) ∎
+      where
+        open ≡-Reasoning
diff --git a/Data/Vector/Bisemimodule.agda b/Data/Vector/Bisemimodule.agda
index e38536a..4121b91 100644
--- a/Data/Vector/Bisemimodule.agda
+++ b/Data/Vector/Bisemimodule.agda
@@ -32,8 +32,6 @@ private
 
 opaque
 
-  unfolding Vector
-
   -- Scaling a vector from the left
   _⟨_⟩ : Carrier → Vector n → Vector n
   _⟨_⟩ r = map (r *_)
diff --git a/Data/Vector/Core.agda b/Data/Vector/Core.agda
index a430f12..c002676 100644
--- a/Data/Vector/Core.agda
+++ b/Data/Vector/Core.agda
@@ -6,101 +6,104 @@ open import Relation.Binary using (Setoid; Rel; IsEquivalence)
 
 module Data.Vector.Core {c ℓ : Level} (S : Setoid c ℓ) where
 
-import Relation.Binary.Reasoning.Setoid as ≈-Reasoning
+open Setoid S
+
 import Data.Vec.Relation.Binary.Pointwise.Inductive as PW
 
 open import Categories.Category.Instance.Nat using (Natop)
 open import Categories.Category.Instance.Setoids using (Setoids)
 open import Categories.Functor using (Functor)
 open import Data.Fin using (Fin)
-open import Data.Nat using (ℕ; _+_)
-open import Data.Setoid using (∣_∣)
-open import Data.Vec as Vec using (Vec; lookup; tabulate)
+open import Data.Nat using (ℕ)
+open import Data.Vec using (Vec; lookup; tabulate; head; tail; map; _++_; replicate; zipWith)
 open import Data.Vec.Properties using (tabulate∘lookup; lookup∘tabulate; tabulate-cong)
 open import Data.Vec.Relation.Binary.Equality.Setoid S using (_≋_; ≋-isEquivalence)
+open import Data.Vector.Raw using (module Relation)
 open import Function using (Func; _⟶ₛ_; id; _⟨$⟩_; _∘_)
 open import Relation.Binary.PropositionalEquality as ≡ using (_≡_; _≗_)
 
 open Func
-open Setoid S
-open Fin
-open Vec.Vec
+open ℕ
+
+Vector : ℕ → Set c
+Vector = Vec Carrier
 
 private
   variable
-    n A B C : ℕ
-
-opaque
-
-  -- Vectors over the rig
-  Vector : ℕ → Set c
-  Vector = Vec ∣ S ∣
+    n m A B C : ℕ
 
-  -- Pointwise equivalence of vectors
-  _≊_ : Rel (Vector n) (c ⊔ ℓ)
-  _≊_ A B = A ≋ B
+-- Pointwise equivalence of vectors
+_≊_ : Rel (Vector n) (c ⊔ ℓ)
+_≊_ A B = A ≋ B
 
-  -- Pointwise equivalence is an equivalence relation
-  ≊-isEquiv : IsEquivalence (_≊_ {n})
-  ≊-isEquiv {n} = ≋-isEquivalence n
-
-  _++_ : Vector A → Vector B → Vector (A + B)
-  _++_ = Vec._++_
-
-  ⟨⟩ : Vector 0
-  ⟨⟩ = []
-
-  ⟨⟩-! : (V : Vector 0) → V ≡ ⟨⟩
-  ⟨⟩-! [] = ≡.refl
+infix 4 _≊_
 
-  ⟨⟩-++ : (V : Vector A) → ⟨⟩ ++ V ≡ V
-  ⟨⟩-++ V = ≡.refl
+-- Pointwise equivalence is an equivalence relation
+≊-isEquiv : IsEquivalence (_≊_ {n})
+≊-isEquiv {n} = ≋-isEquivalence n
 
 -- A setoid of vectors for every natural number
 Vectorₛ : ℕ → Setoid c (c ⊔ ℓ)
 Vectorₛ n = record
-    { Carrier = Vector n
-    ; _≈_ = _≊_
-    ; isEquivalence = ≊-isEquiv
+  { Carrier = Vector n
+  ; _≈_ = _≊_
+  ; isEquivalence = ≊-isEquiv
   }
 
 module ≊ {n} = Setoid (Vectorₛ n)
 
-infix 4 _≊_
-
-opaque
-
-  unfolding Vector
-
-  pull : (Fin B → Fin A) → Vectorₛ A ⟶ₛ Vectorₛ B
-  pull f .to v = tabulate (λ i → lookup v (f i))
-  pull f .cong ≊v = PW.tabulate⁺ (λ i → PW.lookup ≊v (f i))
+pull : (Fin B → Fin A) → Vectorₛ A ⟶ₛ Vectorₛ B
+pull f .to v = tabulate (λ i → lookup v (f i))
+pull f .cong ≊v = PW.tabulate⁺ (λ i → PW.lookup ≊v (f i))
 
-  pull-id : {v : Vector n} → pull id ⟨$⟩ v ≊ v
-  pull-id {v} = ≊.reflexive (tabulate∘lookup v)
+pull-id : {v : Vector n} → pull id ⟨$⟩ v ≊ v
+pull-id {v} = ≊.reflexive (tabulate∘lookup v)
 
-  pull-∘
-      : {f : Fin B → Fin A}
-        {g : Fin C → Fin B}
-        {v : Vector A}
-      → pull (f ∘ g) ⟨$⟩ v ≊ pull g ⟨$⟩ (pull f ⟨$⟩ v)
-  pull-∘ {f} {g} {v} = ≊.reflexive (≡.sym (tabulate-cong (λ i → lookup∘tabulate (lookup v ∘ f) (g i))))
+pull-∘
+    : {f : Fin B → Fin A}
+      {g : Fin C → Fin B}
+      {v : Vector A}
+    → pull (f ∘ g) ⟨$⟩ v ≊ pull g ⟨$⟩ (pull f ⟨$⟩ v)
+pull-∘ {f} {g} {v} = ≊.reflexive (≡.sym (tabulate-cong (λ i → lookup∘tabulate (lookup v ∘ f) (g i))))
 
-  pull-cong
-      : {f g : Fin B → Fin A}
-      → f ≗ g
-      → {v : Vector A}
-      → pull f ⟨$⟩ v ≊ pull g ⟨$⟩ v
-  pull-cong f≗g {v} = ≊.reflexive (tabulate-cong (λ i → ≡.cong (lookup v) (f≗g i)))
+pull-cong
+    : {f g : Fin B → Fin A}
+    → f ≗ g
+    → {v : Vector A}
+    → pull f ⟨$⟩ v ≊ pull g ⟨$⟩ v
+pull-cong f≗g {v} = ≊.reflexive (tabulate-cong (λ i → ≡.cong (lookup v) (f≗g i)))
 
 -- Copying, deleting, and rearranging elements
 -- of a vector according to a function on indices
 -- gives a contravariant functor from Nat to Setoids
 Pull : Functor Natop (Setoids c (c ⊔ ℓ))
 Pull = record
-    { F₀ = Vectorₛ
-    ; F₁ = pull
-    ; identity = pull-id
-    ; homomorphism = pull-∘
-    ; F-resp-≈ = pull-cong
-    }
+  { F₀ = Vectorₛ
+  ; F₁ = pull
+  ; identity = pull-id
+  ; homomorphism = λ {f = f} {g v} → pull-∘ {f = f} {g} {v}
+  ; F-resp-≈ = pull-cong
+  }
+
+module Cong where
+
+  open Relation {R = _≈_}
+
+  head-cong : {V₁ V₂ : Vector (suc n)} → V₁ ≊ V₂ → head V₁ ≈ head V₂
+  head-cong = R-head
+
+  tail-cong : {V₁ V₂ : Vector (suc n)} → V₁ ≊ V₂ → tail V₁ ≊ tail V₂
+  tail-cong = R-tail
+
+  ++-cong
+      : {V₁ V₂ : Vector m}
+        {W₁ W₂ : Vector n}
+      → V₁ ≊ V₂
+      → W₁ ≊ W₂
+      → V₁ ++ W₁ ≊ V₂ ++ W₂
+  ++-cong = R-++
+
+  replicate-cong : {n : ℕ} {x y : Carrier} → x ≈ y → replicate n x ≋ replicate n y
+  replicate-cong = R-replicate
+
+open Cong public
diff --git a/Data/Vector/Endofunctor.agda b/Data/Vector/Endofunctor.agda
deleted file mode 100644
index a9b2905..0000000
--- a/Data/Vector/Endofunctor.agda
+++ /dev/null
@@ -1,68 +0,0 @@
-{-# OPTIONS --without-K --safe #-}
-
-open import Data.Nat using (ℕ)
-open import Level using (Level; _⊔_)
-
--- The endofunctor in setoids sending A to Vector A n for a fixed n
-module Data.Vector.Endofunctor (n : ℕ) {c ℓ : Level} where
-
-import Data.Vec as Vec
-
-open import Categories.Category.Instance.Setoids using (Setoids)
-open import Categories.Functor using (Functor)
-open import Data.Vec.Properties using (map-id; map-∘)
-open import Data.Vec.Relation.Binary.Pointwise.Inductive using (map⁺)
-open import Data.Vector.Core as Core using (Vector; Vectorₛ; module ≊)
-open import Function using (Func; _⟶ₛ_; _⟨$⟩_)
-open import Function.Construct.Composition using () renaming (function to compose)
-open import Function.Construct.Identity using () renaming (function to Id)
-open import Relation.Binary using (Setoid)
-
-open Func
-
-opaque
-  unfolding Vector
-  map : {c ℓ : Level} {A B : Setoid c ℓ} → A ⟶ₛ B → Vectorₛ A n ⟶ₛ Vectorₛ B n
-  map f .to = Vec.map (to f)
-  map f .cong = map⁺ (cong f)
-
-abstract opaque
-
-  unfolding map
-
-  identity
-      : {A : Setoid c ℓ}
-        {V : Vector A n}
-        (open Core A using (_≊_))
-      → map (Id A) ⟨$⟩ V ≊ V
-  identity {A} {V} = ≊.reflexive A (map-id V)
-
-  homomorphism
-      : {X Y Z : Setoid c ℓ}
-        {f : X ⟶ₛ Y}
-        {g : Y ⟶ₛ Z}
-        {V : Vector X n}
-        (open Core Z using (_≊_))
-      → map (compose f g) ⟨$⟩ V ≊ map g ⟨$⟩ (map f ⟨$⟩ V)
-  homomorphism {_} {_} {Z} {f} {g} {V} = ≊.reflexive Z (map-∘ (to g) (to f) V)
-
-  F-resp-≈
-      : {A B : Setoid c ℓ}
-        {f g : A ⟶ₛ B}
-      → ({x : Setoid.Carrier A} → (B Setoid.≈ to f x) (to g x))
-      → {V : Vector A n}
-        (open Core B using (_≊_))
-      → map f ⟨$⟩ V ≊ map g ⟨$⟩ V
-  F-resp-≈ {A} {B} {_} {g} f≈g {V} = map⁺ (λ x≈y → B.trans f≈g (cong g x≈y)) (≊.refl A)
-    where
-      module B = Setoid B
-
--- only a true endofunctor when c ≤ ℓ
-Vec : Functor (Setoids c ℓ) (Setoids c (c ⊔ ℓ))
-Vec = record
-    { F₀ = λ A → Vectorₛ A n
-    ; F₁ = map
-    ; identity = identity
-    ; homomorphism = homomorphism
-    ; F-resp-≈ = F-resp-≈
-    }
diff --git a/Data/Vector/Endofunctor/Monoid.agda b/Data/Vector/Endofunctor/Monoid.agda
new file mode 100644
index 0000000..217c754
--- /dev/null
+++ b/Data/Vector/Endofunctor/Monoid.agda
@@ -0,0 +1,106 @@
+{-# OPTIONS --without-K --safe #-}
+
+open import Data.Nat using (ℕ)
+open import Level using (Level; _⊔_)
+
+-- The endofunctor in monoids sending A to Vectorₘ A n for a fixed n
+module Data.Vector.Endofunctor.Monoid (n : ℕ) {c ℓ : Level} where
+
+import Data.Vec as Vec
+import Relation.Binary.Reasoning.Setoid as ≈-Reasoning
+
+open import Algebra using (Monoid)
+open import Categories.Category using (Category; _[_∘_]; _[_≈_])
+open import Categories.Functor using (Functor)
+open import Category.Instance.Monoids using (Monoids; MonoidHomomorphism; mk-⇒)
+open import Data.Monoid using (toMonoid)
+open import Data.Vec.Properties using (map-replicate)
+open import Data.Vec.Relation.Binary.Pointwise.Inductive using (map⁺)
+open import Data.Vector.Core as Core using (Vector; Vectorₛ; module ≊; replicate-cong)
+open import Data.Vector.Endofunctor.Setoid as Endo using (mapₛ; zipWith-cong)
+open import Data.Vector.Monoid as Mon using (Vectorₘ; ⟨ε⟩) renaming (_⊕_ to _[_⊕_])
+open import Data.Vector.Vec using (map-zipWith; zipWith-map-map)
+open import Function using (Func; _⟶ₛ_; _⟨$⟩_)
+
+open Func
+open MonoidHomomorphism
+
+private module _ {M N : Monoid c ℓ} (f : MonoidHomomorphism c ℓ M N) where
+
+  private
+    module M = Monoid M
+    module N = Monoid N
+
+  open Core N.setoid using (_≊_)
+  open ≈-Reasoning (Vectorₛ N.setoid n)
+
+  opaque
+    unfolding _[_⊕_]
+    map-⊕
+        : (W V : Vector M.setoid n)
+        → mapₛ n (func f) ⟨$⟩ (M [ W ⊕ V ])
+        ≊ N [ mapₛ n (func f) ⟨$⟩ W ⊕ mapₛ n (func f) ⟨$⟩ V ]
+    map-⊕ W V = begin
+        Vec.map ⟦ f ⟧ (Vec.zipWith M._∙_ W V)                 ≡⟨ map-zipWith ⟦ f ⟧ M._∙_ W V ⟩
+        Vec.zipWith (λ x y → ⟦ f ⟧ (x M.∙ y)) W V             ≈⟨ zipWith-cong n N.setoid (homo f) W V ⟩
+        Vec.zipWith (λ x y → ⟦ f ⟧ x N.∙ ⟦ f ⟧ y) W V         ≡⟨ zipWith-map-map ⟦ f ⟧ ⟦ f ⟧ N._∙_ W V ⟩
+        Vec.zipWith N._∙_ (Vec.map ⟦ f ⟧ W) (Vec.map ⟦ f ⟧ V) ∎
+
+  opaque
+    unfolding ⟨ε⟩
+    map-⟨ε⟩ : mapₛ n (func f) ⟨$⟩ (Mon.⟨ε⟩ M) ≊ Mon.⟨ε⟩ N
+    map-⟨ε⟩ = begin
+        Vec.map (to (func f)) (Vec.replicate n M.ε) ≡⟨ map-replicate (to (func f)) M.ε n ⟩
+        Vec.replicate n (func f ⟨$⟩ M.ε)            ≈⟨ replicate-cong N.setoid (ε-homo f) ⟩
+        Vec.replicate n N.ε ∎
+
+mapₘ : {M N : Monoid c ℓ} → MonoidHomomorphism c ℓ M N → MonoidHomomorphism c (c ⊔ ℓ) (Vectorₘ M n) (Vectorₘ N n)
+mapₘ {M} {N} f = mk-⇒ record
+    { ⟦_⟧ = to (mapₛ n (func f))
+    ; isMonoidHomomorphism = record
+        { isMagmaHomomorphism = record
+            { isRelHomomorphism = record
+                { cong = map⁺ (⟦⟧-cong f)
+                }
+            ; homo = map-⊕ f
+            }
+        ; ε-homo = map-⟨ε⟩ f
+        }
+    }
+
+open Category using (id)
+
+abstract
+
+  identity
+      : {A : Monoid c ℓ}
+      → Monoids c (c ⊔ ℓ) [ mapₘ (id (Monoids c ℓ) {A}) ≈ id (Monoids c (c ⊔ ℓ)) ]
+  identity {A} V = Endo.identity n {c} {ℓ} {Monoid.setoid A}
+
+  homomorphism
+      : {X Y Z : Monoid c ℓ}
+        {f : MonoidHomomorphism c ℓ X Y}
+        {g : MonoidHomomorphism c ℓ Y Z}
+      → Monoids c (c ⊔ ℓ) [ mapₘ (Monoids c ℓ [ g ∘ f ]) ≈ Monoids c (c ⊔ ℓ) [ mapₘ g ∘ mapₘ f ] ]
+  homomorphism {X} {Y} {Z} {f} {g} V = Endo.homomorphism n {c} {ℓ} {setoid X} {setoid Y} {setoid Z} {func f} {func g} {V}
+    where
+      open Monoid using (setoid)
+
+  F-resp-≈
+      : {A B : Monoid c ℓ}
+        {f g : MonoidHomomorphism c ℓ A B}
+      → Monoids c ℓ [ f ≈ g ]
+      → Monoids c (c ⊔ ℓ) [ mapₘ f ≈ mapₘ g ]
+  F-resp-≈ {A} {B} {f} {g} f≈g V = Endo.F-resp-≈ n {c} {ℓ} {setoid A} {setoid B} {func f} {func g} (λ {x} → f≈g x)
+    where
+      open Monoid using (setoid)
+
+-- only a true endofunctor when c ≤ ℓ
+Vec : Functor (Monoids c ℓ) (Monoids c (c ⊔ ℓ))
+Vec = record
+    { F₀ = λ M → Vectorₘ M n
+    ; F₁ = mapₘ
+    ; identity = λ {M} → identity {M}
+    ; homomorphism = λ {f = f} {g} → homomorphism {f = f} {g}
+    ; F-resp-≈ = λ {f = f} {g} → F-resp-≈ {f = f} {g}
+    }
diff --git a/Data/Vector/Endofunctor/Setoid.agda b/Data/Vector/Endofunctor/Setoid.agda
new file mode 100644
index 0000000..09f8f69
--- /dev/null
+++ b/Data/Vector/Endofunctor/Setoid.agda
@@ -0,0 +1,81 @@
+{-# OPTIONS --without-K --safe #-}
+
+open import Data.Nat using (ℕ)
+open import Level using (Level; _⊔_)
+
+-- The endofunctor in setoids sending A to Vector A n for a fixed n
+module Data.Vector.Endofunctor.Setoid (n : ℕ) {c ℓ : Level} where
+
+import Data.Vec as Vec
+
+open import Categories.Category using (_[_≈_])
+open import Categories.Category.Instance.Setoids using (Setoids)
+open import Categories.Functor using (Functor)
+open import Data.Setoid using (∣_∣)
+open import Data.Vec.Properties using (map-id; map-∘)
+open import Data.Vec.Relation.Binary.Equality.Setoid using () renaming (_≋_ to _[_≋_])
+open import Data.Vec.Relation.Binary.Pointwise.Inductive as PW using (map⁺; Pointwise)
+open import Data.Vector.Core as Core using (Vector; Vectorₛ; module ≊)
+open import Data.Vector.Raw using (R-zipWith)
+open import Function using (Func; _⟶ₛ_; _⟨$⟩_)
+open import Function.Construct.Composition using () renaming (function to compose)
+open import Function.Construct.Identity using () renaming (function to Id)
+open import Relation.Binary using (Setoid)
+open import Relation.Binary.PropositionalEquality as ≡ using (_≡_)
+
+open Func
+open ℕ
+open Vec.Vec
+open Pointwise
+
+mapₛ : {A B : Setoid c ℓ} → A ⟶ₛ B → Vectorₛ A n ⟶ₛ Vectorₛ B n
+mapₛ f .to = Vec.map (to f)
+mapₛ f .cong = map⁺ (cong f)
+
+abstract
+
+  identity
+      : {A : Setoid c ℓ}
+        {V : Vector A n}
+        (open Core A using (_≊_))
+      → mapₛ (Id A) ⟨$⟩ V ≊ V
+  identity {A} {V} = ≊.reflexive A (map-id V)
+
+  homomorphism
+      : {X Y Z : Setoid c ℓ}
+        {f : X ⟶ₛ Y}
+        {g : Y ⟶ₛ Z}
+        {V : Vector X n}
+        (open Core Z using (_≊_))
+      → mapₛ (compose f g) ⟨$⟩ V ≊ mapₛ g ⟨$⟩ (mapₛ f ⟨$⟩ V)
+  homomorphism {_} {_} {Z} {f} {g} {V} = ≊.reflexive Z (map-∘ (to g) (to f) V)
+
+  F-resp-≈
+      : {A B : Setoid c ℓ}
+        {f g : A ⟶ₛ B}
+      → Setoids c ℓ [ f ≈ g ]
+      → Setoids c (c ⊔ ℓ) [ mapₛ f ≈ mapₛ g ]
+  F-resp-≈ {A} {B} {_} {g} f≈g {V} = map⁺ (λ x≈y → B.trans f≈g (cong g x≈y)) (≊.refl A)
+    where
+      module B = Setoid B
+
+-- only a true endofunctor when c ≤ ℓ
+Vec : Functor (Setoids c ℓ) (Setoids c (c ⊔ ℓ))
+Vec = record
+    { F₀ = λ A → Vectorₛ A n
+    ; F₁ = mapₛ
+    ; identity = λ {A} → identity {A}
+    ; homomorphism = λ {f = f} {g} → homomorphism {f = f} {g}
+    ; F-resp-≈ = λ {f = f} {g} → F-resp-≈ {f = f} {g}
+    }
+
+zipWith-cong
+    : {A B : Set c}
+      (C : Setoid c ℓ)
+      (let module C = Setoid C)
+      {f g : A → B → ∣ C ∣}
+    → (∀ x y → f x y C.≈ g x y)
+    → (xs : Vec.Vec A n)
+      (ys : Vec.Vec B n)
+    → C [ Vec.zipWith f xs ys ≋ Vec.zipWith g xs ys ]
+zipWith-cong C f≈g xs ys = R-zipWith {R = _≡_} {S = _≡_} (λ { ≡.refl ≡.refl → f≈g _ _}) (PW.refl ≡.refl) (PW.refl ≡.refl)
diff --git a/Data/Vector/Monoid.agda b/Data/Vector/Monoid.agda
index 5906bf9..da09de9 100644
--- a/Data/Vector/Monoid.agda
+++ b/Data/Vector/Monoid.agda
@@ -24,8 +24,6 @@ private
 
 opaque
 
-  unfolding Vector
-
   -- Sum the elements of a vector
   sum : Vector n → M.Carrier
   sum = foldr′ _∙_ ε
@@ -36,8 +34,6 @@ opaque
 
 opaque
 
-  unfolding Vector
-
   -- Pointwise sum of two vectors
   _⊕_ : Vector n → Vector n → Vector n
   _⊕_ = zipWith _∙_
@@ -54,8 +50,6 @@ infixl 6 _⊕_
 
 opaque
 
-  unfolding Vector
-
   -- The identity vector
   ⟨ε⟩ : Vector n
   ⟨ε⟩ {n} = replicate n ε
@@ -119,7 +113,7 @@ open ≡-Reasoning
 
 opaque
 
-  unfolding pull _⊕_
+  unfolding _⊕_
 
   pull-⊕ : {f : Fin A → Fin B} (V W : Vector B) → pull f ⟨$⟩ (V ⊕ W) ≡ (pull f ⟨$⟩ V) ⊕ (pull f ⟨$⟩ W)
   pull-⊕ {A} {B} {f} V W = begin
@@ -132,7 +126,7 @@ opaque
 
 opaque
 
-  unfolding pull ⟨ε⟩
+  unfolding ⟨ε⟩
 
   pull-⟨ε⟩ : {f : Fin A → Fin B} → pull f ⟨$⟩ ⟨ε⟩ ≡ ⟨ε⟩
   pull-⟨ε⟩ {f = f} = begin
@@ -157,7 +151,7 @@ opaque
         {g : Fin C → Fin B}
         {v : Vector A}
       → arr (pullₘ (f ∘ g)) ⟨$⟩ v ≊ arr (pullₘ g) ⟨$⟩ (arr (pullₘ f) ⟨$⟩ v)
-  pullₘ-∘ = S.pull-∘
+  pullₘ-∘ {f = f} {g} {v} = S.pull-∘ {f = f} {g} {v}
 
   pullₘ-cong
       : {f g : Fin B → Fin A}
diff --git a/Data/Vector/Raw.agda b/Data/Vector/Raw.agda
new file mode 100644
index 0000000..c333553
--- /dev/null
+++ b/Data/Vector/Raw.agda
@@ -0,0 +1,95 @@
+{-# OPTIONS --without-K --safe #-}
+
+module Data.Vector.Raw where
+
+open import Data.Nat using (ℕ; _+_)
+open import Data.Vec using (Vec; head; tail; map; _++_; replicate; zipWith)
+open import Data.Vec.Properties using (map-replicate)
+open import Data.Vec.Relation.Binary.Pointwise.Inductive using (Pointwise)
+open import Level using (Level)
+open import Relation.Binary using (REL)
+open import Relation.Binary.PropositionalEquality as ≡ using (_≡_)
+
+private
+  variable
+    n m : ℕ
+    a ℓ ℓ₁ ℓ₂ : Level
+    A B C D E F : Set a
+
+open ℕ
+open Vec
+
+⟨⟩ : Vec A 0
+⟨⟩ = []
+
+⟨⟩-! : (V : Vec A 0) → V ≡ ⟨⟩
+⟨⟩-! [] = ≡.refl
+
+⟨⟩-++ : {n : ℕ} (V : Vec A n) → ⟨⟩ ++ V ≡ V
+⟨⟩-++ V = ≡.refl
+
+module Natural {n : ℕ} (f : A → B) where
+
+  α-head : (V : Vec A (suc n)) → f (head V) ≡ head (map f V)
+  α-head (x ∷ _) = ≡.erefl (f x)
+
+  α-tail : (V : Vec A (suc n)) → map f (tail V) ≡ tail (map f V)
+  α-tail (_ ∷ V) = ≡.erefl (map f V)
+
+  α-replicate : {x : A} → map f (replicate n x) ≡ replicate n (f x)
+  α-replicate {x} = map-replicate f x n
+
+open Natural public
+
+open Pointwise
+
+module Relation {R : REL A B ℓ} where
+
+  R-head
+      : {V₁ : Vec A (suc n)}
+        {V₂ : Vec B (suc n)}
+      → Pointwise R V₁ V₂
+      → R (head V₁) (head V₂)
+  R-head (R-x ∷ _) = R-x
+
+  R-tail
+      : {V₁ : Vec A (suc n)}
+        {V₂ : Vec B (suc n)}
+      → Pointwise R V₁ V₂
+      → Pointwise R (tail V₁) (tail V₂)
+  R-tail (_ ∷ R-V) = R-V
+
+  R-++
+      : {R : REL A B ℓ}
+        {V₁ : Vec A m}
+        {V₂ : Vec B m}
+        {W₁ : Vec A n}
+        {W₂ : Vec B n}
+      → Pointwise R V₁ V₂
+      → Pointwise R W₁ W₂
+      → Pointwise R (V₁ ++ W₁) (V₂ ++ W₂)
+  R-++ [] R-W = R-W
+  R-++ (R-v ∷ R-V) R-W = R-v ∷ R-++ R-V R-W
+
+  R-replicate : {x : A} {y : B} → R x y → Pointwise R (replicate n x) (replicate n y)
+  R-replicate {n = zero} _ = []
+  R-replicate {n = suc n} xRy = xRy ∷ R-replicate xRy
+
+R-zipWith
+    : {W : Vec A n}
+      {X : Vec B n}
+      {Y : Vec C n}
+      {Z : Vec D n}
+      {R : REL A B ℓ₁}
+      {S : REL C D ℓ₂}
+      {T : REL E F ℓ}
+      {f : A → C → E}
+      {g : B → D → F}
+    → (∀ {w x y z} → R w x → S y z → T (f w y) (g x z))
+    → Pointwise R W X
+    → Pointwise S Y Z
+    → Pointwise T (zipWith f W Y) (zipWith g X Z)
+R-zipWith cong [] [] = []
+R-zipWith cong (wRx ∷ WRX) (ySz ∷ YSZ) = cong wRx ySz ∷ R-zipWith cong WRX YSZ
+
+open Relation public
diff --git a/Data/Vector/Vec.agda b/Data/Vector/Vec.agda
index 868571a..4367bdd 100644
--- a/Data/Vector/Vec.agda
+++ b/Data/Vector/Vec.agda
@@ -5,6 +5,8 @@ module Data.Vector.Vec where
 open import Data.Fin using (Fin)
 open import Data.Nat using (ℕ; _+_)
 open import Data.Vec using (Vec; tabulate; zipWith; replicate; map; _++_)
+open import Data.Vec.Relation.Binary.Pointwise.Inductive as PW using (Pointwise-≡⇒≡)
+open import Data.Vector.Raw using (R-zipWith)
 open import Function using (_∘_)
 open import Level using (Level)
 open import Relation.Binary.PropositionalEquality as ≡ using (_≡_)
@@ -71,3 +73,16 @@ zipWith-map-map
     → zipWith (λ x y → f x ⊕ g y) v w ≡ zipWith _⊕_ (map f v) (map g w)
 zipWith-map-map f g _⊕_ [] [] = ≡.refl
 zipWith-map-map f g _⊕_ (x ∷ v) (y ∷ w) = ≡.cong (f x ⊕ g y ∷_) (zipWith-map-map f g _⊕_ v w)
+
+zipWith-cong
+    : {f g : A → B → C}
+    → (∀ x y → f x y ≡ g x y)
+    → (xs : Vec A n)
+      (ys : Vec B n)
+    → zipWith f xs ys
+    ≡ zipWith g xs ys
+zipWith-cong f≗g xs ys =
+    Pointwise-≡⇒≡
+      (R-zipWith {R = _≡_} {S = _≡_} (λ { ≡.refl ≡.refl → f≗g _ _})
+      (PW.refl ≡.refl)
+      (PW.refl ≡.refl))