Begin separating vector concepts from matrices

1 files changed, 94 insertions, 0 deletions

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
+    }