Begin separating vector concepts from matrices

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