2 files changed, 187 insertions, 0 deletions
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)