Add hom-set addition to semiadditive recordmain

1 files changed, 28 insertions, 1 deletions

diff --git a/Data/Matrix/Semiadditive.agda b/Data/Matrix/Semiadditive.agda
index babbdfa..dd24d15 100644
--- a/Data/Matrix/Semiadditive.agda
+++ b/Data/Matrix/Semiadditive.agda
@@ -21,7 +21,7 @@ open import Categories.Object.Product using (IsProduct)
 open import Categories.Object.Terminal using (IsTerminal)
 open import Categories.Object.Zero using (Zero)
 open import Category.Semiadditive using (Semiadditive)
-open import Data.Matrix.Category R using (Mat; _·_; ≑-·; ·-Iˡ; ·-Iʳ; ·-𝟎ˡ; ·-𝟎ʳ; ·-∥; ∥-·-≑; ·-resp-≋; ·-assoc)
+open import Data.Matrix.Category R using (Mat; _·_; ≑-·; ·-Iˡ; ·-Iʳ; ·-𝟎ˡ; ·-𝟎ʳ; ·-∥; ∥-·-≑; ·-resp-≋; ·-assoc; ·-[+]ˡ; ·-[+]ʳ)
 open import Data.Matrix.Core R.setoid using (Matrix; Matrixₛ; _≋_; module ≋; ∥-cong; ≑-cong; ᵀ-cong)
 open import Data.Matrix.Monoid R.+-monoid using (𝟎; 𝟎ᵀ; 𝟎≑𝟎; 𝟎∥𝟎; _[+]_; [+]-cong; [+]-𝟎ˡ; [+]-𝟎ʳ)
 open import Data.Matrix.Raw using (_ᵀ; _ᵀᵀ; mapₕ; []ᵥ; []ᵥ-∥; []ₕ; []ₕ-!; []ₕ-≑; _∷ᵥ_; _∷ₕ_; ∷ᵥ-ᵀ; _∥_; _≑_; ∷ₕ-ᵀ; ∷ₕ-≑; []ᵥ-ᵀ; head-∷-tailₕ; headₕ; tailₕ; ∷ₕ-∥; ∷ᵥ-≑; []ᵥ-!)
@@ -257,12 +257,39 @@ zeroObj = record
         }
     }
 
+𝟎-resp-· : {M : Matrix C D} {N : Matrix A B} → M · 𝟎 {B} {C} · N ≋ 𝟎 {A} {D}
+𝟎-resp-· {D = D} {A = A} {M = M} {N} = begin
+    M · 𝟎 · N ≈⟨ ·-resp-≋ ≋.refl (·-𝟎ˡ N) ⟩
+    M · 𝟎     ≈⟨ ·-𝟎ʳ M ⟩
+    𝟎         ∎
+  where
+    open ≈-Reasoning (Matrixₛ A D)
+
+[+]-resp-·
+    : {M N : Matrix B C}
+      {H : Matrix A B}
+      {K : Matrix C D}
+    → K · (M [+] N) · H ≋ (K · M · H) [+] (K · N · H)
+[+]-resp-· {A = A} {D = D} {M = M} {N} {H} {K} = begin
+    K · (M [+] N) · H           ≈⟨ ·-resp-≋ ≋.refl (·-[+]ʳ H M N) ⟩
+    K · ((M · H) [+] (N · H))   ≈⟨ ·-[+]ˡ K (M · H) (N · H) ⟩
+    (K · M · H) [+] (K · N · H) ∎
+  where
+    open ≈-Reasoning (Matrixₛ A D)
+
 Mat-Semiadditive : Semiadditive Mat
 Mat-Semiadditive = record
     { zero = zeroObj
     ; biproducts = record
         { biproduct = biproduct
         }
+    ; 𝟎 = 𝟎
+    ; 𝟎-resp-∘ = 𝟎-resp-·
+    ; _+_ = _[+]_
+    ; +-resp-≈ = [+]-cong
+    ; +-resp-∘ = [+]-resp-·
+    ; +-identityˡ = [+]-𝟎ˡ
+    ; +-identityʳ = [+]-𝟎ʳ
     }
 
 open Semiadditive Mat-Semiadditive