Begin separating vector concepts from matrices

1 files changed, 175 insertions, 0 deletions

diff --git a/Data/Vector/Monoid.agda b/Data/Vector/Monoid.agda
new file mode 100644
index 0000000..5906bf9
--- /dev/null
+++ b/Data/Vector/Monoid.agda
@@ -0,0 +1,175 @@
+{-# OPTIONS --without-K --safe #-}
+
+open import Algebra using (Monoid)
+open import Level using (Level; _⊔_)
+
+module Data.Vector.Monoid {c ℓ : Level} (M : Monoid c ℓ) where
+
+module M = Monoid M
+
+import Data.Vec.Relation.Binary.Pointwise.Inductive as PW
+import Relation.Binary.Reasoning.Setoid as ≈-Reasoning
+
+open import Data.Nat using (ℕ)
+open import Data.Product using (_,_)
+open import Data.Vec using (Vec; foldr′; zipWith; replicate)
+open import Data.Vector.Core M.setoid as S using (Vector; _≊_; module ≊; pull; Vectorₛ)
+
+open M
+open Vec
+
+private
+  variable
+    n A B C : ℕ
+
+opaque
+
+  unfolding Vector
+
+  -- Sum the elements of a vector
+  sum : Vector n → M.Carrier
+  sum = foldr′ _∙_ ε
+
+  sum-cong : {V V′ : Vector n} → V ≊ V′ → sum V ≈ sum V′
+  sum-cong PW.[] = refl
+  sum-cong (≈x PW.∷ ≊V) = ∙-cong ≈x (sum-cong ≊V)
+
+opaque
+
+  unfolding Vector
+
+  -- Pointwise sum of two vectors
+  _⊕_ : Vector n → Vector n → Vector n
+  _⊕_ = zipWith _∙_
+
+  ⊕-cong : {V₁ V₂ W₁ W₂ : Vector n} → V₁ ≊ V₂ → W₁ ≊ W₂ → V₁ ⊕ W₁ ≊ V₂ ⊕ W₂
+  ⊕-cong PW.[] PW.[] = PW.[]
+  ⊕-cong (≈v PW.∷ ≊V) (≈w PW.∷ ≊W) = ∙-cong ≈v ≈w PW.∷ ⊕-cong ≊V ≊W
+
+  ⊕-assoc : (x y z : Vector n) → x ⊕ y ⊕ z ≊ x ⊕ (y ⊕ z)
+  ⊕-assoc [] [] [] = PW.[]
+  ⊕-assoc (x₀ ∷ x) (y₀ ∷ y) (z₀ ∷ z) = assoc x₀ y₀ z₀ PW.∷ ⊕-assoc x y z
+
+infixl 6 _⊕_
+
+opaque
+
+  unfolding Vector
+
+  -- The identity vector
+  ⟨ε⟩ : Vector n
+  ⟨ε⟩ {n} = replicate n ε
+
+opaque
+
+  unfolding _⊕_ ⟨ε⟩
+
+  ⊕-identityˡ : (V : Vector n) → ⟨ε⟩ ⊕ V ≊ V
+  ⊕-identityˡ [] = PW.[]
+  ⊕-identityˡ (x ∷ V) = identityˡ x PW.∷ ⊕-identityˡ V
+
+  ⊕-identityʳ : (V : Vector n) → V ⊕ ⟨ε⟩ ≊ V
+  ⊕-identityʳ [] = PW.[]
+  ⊕-identityʳ (x ∷ V) = identityʳ x PW.∷ ⊕-identityʳ V
+
+-- A monoid of vectors for each natural number
+Vectorₘ : ℕ → Monoid c (c ⊔ ℓ)
+Vectorₘ n = record
+    { Carrier = Vector n
+    ; _≈_ = _≊_
+    ; _∙_ = _⊕_
+    ; ε = ⟨ε⟩
+    ; isMonoid = record
+        { isSemigroup = record
+            { isMagma = record
+                { isEquivalence = ≊.isEquivalence
+                ; ∙-cong = ⊕-cong
+                }
+            ; assoc = ⊕-assoc
+            }
+        ; identity = ⊕-identityˡ , ⊕-identityʳ
+        }
+    }
+
+open import Category.Instance.Setoids.SymmetricMonoidal {c} {c ⊔ ℓ} using (Setoids-×; ×-monoidal′)
+
+open import Categories.Category.Construction.Monoids Setoids-×.monoidal using (Monoids)
+open import Categories.Category.Instance.Nat using (Natop)
+open import Categories.Category.Instance.Setoids using (Setoids)
+open import Categories.Functor using (Functor)
+open import Categories.Object.Monoid Setoids-×.monoidal as Obj using (Monoid⇒)
+open import Data.Fin using (Fin)
+open import Data.Monoid using (module FromMonoid)
+open import Data.Monoid {c} {c ⊔ ℓ} using (fromMonoid)
+open import Data.Vec using (tabulate; lookup)
+open import Data.Vec.Properties using (tabulate-cong; lookup-zipWith; lookup-replicate)
+open import Data.Vector.Vec using (zipWith-tabulate; replicate-tabulate)
+open import Function using (Func; _⟨$⟩_; _∘_; id)
+open import Relation.Binary.PropositionalEquality as ≡ using (module ≡-Reasoning; _≡_; _≗_)
+
+open Functor
+open Monoid⇒
+
+Vector′ : ℕ → Obj.Monoid
+Vector′ n = fromMonoid (Vectorₘ n)
+
+open ℕ
+open Fin
+open ≡-Reasoning
+
+opaque
+
+  unfolding pull _⊕_
+
+  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
+      tabulate (λ i → lookup (zipWith _∙_ V W) (f i))
+          ≡⟨ tabulate-cong (λ i → lookup-zipWith _∙_ (f i) V W) ⟩
+      tabulate (λ i → lookup V (f i) ∙ lookup W (f i))
+          ≡⟨ zipWith-tabulate _∙_ (lookup V ∘ f) (lookup W ∘ f) ⟨
+      zipWith _∙_ (tabulate (lookup V ∘ f)) (tabulate (lookup W ∘ f))
+          ∎
+
+opaque
+
+  unfolding pull ⟨ε⟩
+
+  pull-⟨ε⟩ : {f : Fin A → Fin B} → pull f ⟨$⟩ ⟨ε⟩ ≡ ⟨ε⟩
+  pull-⟨ε⟩ {f = f} = begin
+      tabulate (λ i → lookup (replicate _ ε) (f i)) ≡⟨ tabulate-cong (λ i → lookup-replicate (f i) ε) ⟩
+      tabulate (λ _ → ε)                            ≡⟨ replicate-tabulate ε ⟨
+      replicate _ ε                                 ∎
+
+opaque
+
+  unfolding FromMonoid.μ
+
+  pullₘ : (Fin A → Fin B) → Monoid⇒ (Vector′ B) (Vector′ A)
+  pullₘ f .arr = S.pull f
+  pullₘ f .preserves-μ {V , W} = ≊.reflexive (pull-⊕ V W)
+  pullₘ f .preserves-η = ≊.reflexive pull-⟨ε⟩
+
+  pullₘ-id : {V : Vector n} → arr (pullₘ id) ⟨$⟩ V ≊ V
+  pullₘ-id = S.pull-id
+
+  pullₘ-∘
+      : {f : Fin B → Fin A}
+        {g : Fin C → Fin B}
+        {v : Vector A}
+      → arr (pullₘ (f ∘ g)) ⟨$⟩ v ≊ arr (pullₘ g) ⟨$⟩ (arr (pullₘ f) ⟨$⟩ v)
+  pullₘ-∘ = S.pull-∘
+
+  pullₘ-cong
+      : {f g : Fin B → Fin A}
+      → f ≗ g
+      → {v : Vector A}
+      → arr (pullₘ f) ⟨$⟩ v ≊ arr (pullₘ g) ⟨$⟩ v
+  pullₘ-cong = S.pull-cong
+
+-- Contravariant functor from Nat to Monoids
+Pullₘ : Functor Natop Monoids
+Pullₘ .F₀ = Vector′
+Pullₘ .F₁ = pullₘ
+Pullₘ .identity = pullₘ-id
+Pullₘ .homomorphism = pullₘ-∘
+Pullₘ .F-resp-≈ = pullₘ-cong