Update matrices and vectors

1 files changed, 19 insertions, 13 deletions

diff --git a/Data/Matrix/Endofunctor.agda b/Data/Matrix/Endofunctor.agda
index 25703ce..ac3638f 100644
--- a/Data/Matrix/Endofunctor.agda
+++ b/Data/Matrix/Endofunctor.agda
@@ -6,13 +6,14 @@ open import Level using (Level; _⊔_)
 -- The endofunctor in setoids sending A to Matrix A n m for fixed n and m
 module Data.Matrix.Endofunctor (n m : ℕ) {c ℓ : Level} where
 
-import Data.Vector.Endofunctor as Vector
+import Data.Vector.Endofunctor.Setoid as Vector
 
 open import Categories.Category.Instance.Setoids using (Setoids)
 open import Categories.Functor using (Functor; _∘F_)
+open import Data.Matrix.Raw as Raw using (map; map₂)
 open import Data.Matrix.Core as Core using (Matrix; Matrixₛ)
 open import Data.Vector.Core using (Vector)
-open import Function using (_⟶ₛ_; _⟨$⟩_)
+open import Function using (_⟶ₛ_; _⟨$⟩_; Func)
 open import Function.Construct.Composition using () renaming (function to compose)
 open import Function.Construct.Identity using () renaming (function to Id)
 open import Function.Construct.Setoid using (setoid)
@@ -25,21 +26,26 @@ private
 
   module Vec∘Vec = Functor Vec∘Vec
 
+open Func
+
 opaque
-  unfolding Matrix Vector
-  map : {A B : Setoid c ℓ} → A ⟶ₛ B → Matrixₛ A n m ⟶ₛ Matrixₛ B n m
-  map = Vec∘Vec.₁
+
+  unfolding Core._≋_
+
+  mapₛ : {A B : Setoid c ℓ} → A ⟶ₛ B → Matrixₛ A n m ⟶ₛ Matrixₛ B n m
+  to (mapₛ f) = map (to f)
+  cong (mapₛ f) = map₂ (cong f)
 
 abstract opaque
 
-  unfolding map
+  unfolding mapₛ
 
   identity
       : {A : Setoid c ℓ}
         {M : Matrix A n m}
         (open Core A using (_≋_))
-      → map (Id A) ⟨$⟩ M ≋ M
-  identity = Vec∘Vec.identity
+      → mapₛ (Id A) ⟨$⟩ M ≋ M
+  identity {A} = Vec∘Vec.identity {A}
 
   homomorphism
       : {X Y Z : Setoid c ℓ}
@@ -47,8 +53,8 @@ abstract opaque
         {g : Y ⟶ₛ Z}
         {M : Matrix X n m}
         (open Core Z using (_≋_))
-      → map (compose f g) ⟨$⟩ M ≋ map g ⟨$⟩ (map f ⟨$⟩ M)
-  homomorphism = Vec∘Vec.homomorphism
+      → mapₛ (compose f g) ⟨$⟩ M ≋ mapₛ g ⟨$⟩ (mapₛ f ⟨$⟩ M)
+  homomorphism {f = f} {g} = Vec∘Vec.homomorphism {f = f} {g}
 
   F-resp-≈
       : {A B : Setoid c ℓ}
@@ -57,14 +63,14 @@ abstract opaque
       → (f ≈ g)
       → {M : Matrix A n m}
         (open Core B using (_≋_))
-      → map f ⟨$⟩ M ≋ map g ⟨$⟩ M
-  F-resp-≈ = Vec∘Vec.F-resp-≈
+      → mapₛ f ⟨$⟩ M ≋ mapₛ g ⟨$⟩ M
+  F-resp-≈ {f = f} {g} = Vec∘Vec.F-resp-≈ {f = f} {g}
 
 -- only a true endofunctor when c ≤ ℓ
 Mat : Functor (Setoids c ℓ) (Setoids c (c ⊔ ℓ))
 Mat = record
     { F₀ = λ A → Matrixₛ A n m
-    ; F₁ = map
+    ; F₁ = mapₛ
     ; identity = identity
     ; homomorphism = homomorphism
     ; F-resp-≈ = F-resp-≈