1 files changed, 106 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}
+    }