Begin separating vector concepts from matrices

4 files changed, 342 insertions, 0 deletions

diff --git a/Data/Vector/CommutativeMonoid.agda b/Data/Vector/CommutativeMonoid.agda
new file mode 100644
index 0000000..c7b4a73
--- /dev/null
+++ b/Data/Vector/CommutativeMonoid.agda
@@ -0,0 +1,40 @@
+{-# OPTIONS --without-K --safe #-}
+
+open import Algebra using (Monoid; CommutativeMonoid)
+open import Level using (Level; _⊔_)
+
+module Data.Vector.CommutativeMonoid {c ℓ : Level} (CM : CommutativeMonoid c ℓ) where
+
+module CM = CommutativeMonoid CM
+
+import Data.Vec.Relation.Binary.Pointwise.Inductive as PW
+
+open import Data.Vector.Core CM.setoid using (Vector; _≊_; module ≊)
+open import Data.Vector.Monoid CM.monoid as M using (_⊕_)
+open import Data.Nat using (ℕ)
+open import Data.Vec using (Vec)
+
+open CM
+open Vec
+
+private
+  variable
+    n : ℕ
+
+opaque
+
+  unfolding _⊕_
+
+  ⊕-comm : (V W : Vector n) → V ⊕ W ≊ W ⊕ V
+  ⊕-comm [] [] = ≊.refl
+  ⊕-comm (v ∷ V) (w ∷ W) = comm v w PW.∷ ⊕-comm V W
+
+-- A commutative monoid of vectors for each natural number
+Vectorₘ : ℕ → CommutativeMonoid c (c ⊔ ℓ)
+Vectorₘ n = record
+    { Monoid (M.Vectorₘ n)
+    ; isCommutativeMonoid = record
+        { Monoid (M.Vectorₘ n)
+        ; comm = ⊕-comm
+        }
+    }
diff --git a/Data/Vector/Core.agda b/Data/Vector/Core.agda
new file mode 100644
index 0000000..974f672
--- /dev/null
+++ b/Data/Vector/Core.agda
@@ -0,0 +1,94 @@
+{-# OPTIONS --without-K --safe #-}
+{-# OPTIONS --hidden-argument-puns #-}
+
+open import Level using (Level; _⊔_)
+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
+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 using (Vec; lookup; tabulate)
+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 Function using (Func; _⟶ₛ_; id; _⟨$⟩_; _∘_)
+open import Relation.Binary.PropositionalEquality as ≡ using (_≗_)
+
+open Func
+open Setoid S
+open Vec
+open Fin
+
+private
+  variable
+    n A B C : ℕ
+
+opaque
+
+  -- Vectors over the rig
+  Vector : ℕ → Set c
+  Vector = Vec ∣ S ∣
+
+  -- 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
+
+-- A setoid of vectors for every natural number
+Vectorₛ : ℕ → Setoid c (c ⊔ ℓ)
+Vectorₛ n = record
+    { 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-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-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
+    }
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
diff --git a/Data/Vector/Vec.agda b/Data/Vector/Vec.agda
new file mode 100644
index 0000000..ae87737
--- /dev/null
+++ b/Data/Vector/Vec.agda
@@ -0,0 +1,33 @@
+{-# OPTIONS --without-K --safe #-}
+
+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)
+open import Function using (_∘_)
+open import Level using (Level)
+open import Relation.Binary.PropositionalEquality as ≡ using (_≡_)
+
+open Vec
+open ℕ
+open Fin
+
+zipWith-tabulate
+    : {a : Level}
+      {A : Set a}
+      {n : ℕ}
+      (_⊕_ : A → A → A)
+      (f g : Fin n → A)
+    → zipWith _⊕_ (tabulate f) (tabulate g) ≡ tabulate (λ i → f i ⊕ g i)
+zipWith-tabulate {n = zero} _⊕_ f g = ≡.refl
+zipWith-tabulate {n = suc n} _⊕_ f g = ≡.cong (f zero ⊕ g zero ∷_) (zipWith-tabulate _⊕_ (f ∘ suc) (g ∘ suc))
+
+replicate-tabulate
+    : {a : Level}
+      {A : Set a}
+      {n : ℕ}
+      (x : A)
+    → replicate n x ≡ tabulate (λ _ → x)
+replicate-tabulate {n = zero} x = ≡.refl
+replicate-tabulate {n = suc n} x = ≡.cong (x ∷_) (replicate-tabulate x)