1 files changed, 79 insertions, 0 deletions
diff --git a/Data/Matrix/Endofunctor.agda b/Data/Matrix/Endofunctor.agda
new file mode 100644
index 0000000..d33cdbe
--- /dev/null
+++ b/Data/Matrix/Endofunctor.agda
@@ -0,0 +1,79 @@
+{-# OPTIONS --without-K --safe #-}
+
+open import Data.Nat using (ℕ)
+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
+
+open import Categories.Category.Instance.Setoids using (Setoids)
+open import Categories.Functor using (Functor)
+open import Data.Vec.Properties using (map-id; map-∘)
+open import Data.Vec.Relation.Binary.Pointwise.Inductive using (map⁺)
+open import Data.Vector.Core using (module ≊)
+open import Data.Matrix.Core as Core using (Matrix; Matrixₛ; module ≋)
+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 Relation.Binary using (Setoid)
+open import Relation.Binary.PropositionalEquality as ≡ using (_≡_)
+
+open Func
+
+import Data.Vector.Endofunctor as Vector
+import Data.Vec as Vec
+
+opaque
+  unfolding Matrix
+  map : {A B : Setoid c ℓ} → A ⟶ₛ B → Matrixₛ A n m ⟶ₛ Matrixₛ B n m
+  map f .to = Vec.map (to (Vector.map n f))
+  map f .cong = map⁺ (cong (Vector.map n f))
+
+abstract opaque
+
+  unfolding map
+
+  identity
+      : {A : Setoid c ℓ}
+        {M : Matrix A n m}
+        (open Core A using (_≋_))
+      → map (Id A) ⟨$⟩ M ≋ M
+  identity {A} {M} = ≋.trans A (map⁺ (≊.trans A (Vector.identity n)) (≋.refl A)) (≋.reflexive A (map-id M))
+
+  homomorphism
+      : {X Y Z : Setoid c ℓ}
+        {f : X ⟶ₛ Y}
+        {g : Y ⟶ₛ Z}
+        {M : Matrix X n m}
+        (open Core Z using (_≋_))
+      → map (compose f g) ⟨$⟩ M ≋ map g ⟨$⟩ (map f ⟨$⟩ M)
+  homomorphism {X} {_} {Z} {f} {g} {M} =
+      ≋.trans
+          Z
+          (map⁺ (λ x≈y → ≊.trans Z (Vector.homomorphism n) (cong (Vector.map n g) (cong (Vector.map n f) x≈y))) (≋.refl X))
+          (≋.reflexive Z (map-∘ (to (Vector.map n g)) (to (Vector.map n f)) M))
+
+  F-resp-≈
+      : {A B : Setoid c ℓ}
+        {f g : A ⟶ₛ B}
+      → ({x : Setoid.Carrier A} → (B Setoid.≈ to f x) (to g x))
+      → {M : Matrix A n m}
+        (open Core B using (_≋_))
+      → map f ⟨$⟩ M ≋ map g ⟨$⟩ M
+  F-resp-≈ {A} {B} {f} {g} f≈g {M} =
+      ≋.trans
+          B
+          (map⁺ (λ x≈y → ≊.trans B (Vector.F-resp-≈ n f≈g) (cong (Vector.map n g) x≈y)) (≋.refl A))
+          (map⁺ (cong (Vector.map n g)) (≋.refl A))
+    where
+      module B = Setoid B
+
+-- only a true endofunctor when c ≤ ℓ
+Mat : Functor (Setoids c ℓ) (Setoids c (c ⊔ ℓ))
+Mat = record
+    { F₀ = λ A → Matrixₛ A n m
+    ; F₁ = map
+    ; identity = identity
+    ; homomorphism = homomorphism
+    ; F-resp-≈ = F-resp-≈
+    }