Add hom-set addition to semiadditive recordmain

4 files changed, 66 insertions, 29 deletions

diff --git a/Data/Matrix/Category.agda b/Data/Matrix/Category.agda
index 717926a..e1a10ec 100644
--- a/Data/Matrix/Category.agda
+++ b/Data/Matrix/Category.agda
@@ -13,8 +13,8 @@ import Relation.Binary.Reasoning.Setoid as ≈-Reasoning
 open import Categories.Category using (Category)
 open import Categories.Category.Helper using (categoryHelper)
 open import Data.Matrix.Raw using (_ᵀ; _∷ₕ_; _ᵀᵀ; _∥_; _≑_; mapₕ; mapᵥ; ∷ᵥⁿ; ∷ₕⁿ; columns-∷ₕⁿ; ∷ᵥⁿ-ᵀ)
-open import Data.Matrix.Core R.setoid using (Matrix; Matrixₛ; _≋_; ≋-isEquiv; ᵀ-cong; module ≋)
-open import Data.Matrix.Monoid R.+-monoid using (𝟎; _[+]_)
+open import Data.Matrix.Core R.setoid using (Matrix; Matrixₛ; _≋_; ≋-isEquiv; ᵀ-cong; module ≋; ∥-cong; ≑-cong)
+open import Data.Matrix.Monoid R.+-monoid using (𝟎; _[+]_; [+]-cong)
 open import Data.Matrix.Transform R using ([_]_; _[_]; -[-]-cong; [-]--cong; -[-]ᵀ; []-∙; [-]--∥; [++]-≑; I; Iᵀ; I[-]; map--[-]-I; [-]-𝟎; [⟨0⟩]-)
 open import Data.Nat using (ℕ)
 open import Data.Vec using (Vec; map)
@@ -176,6 +176,36 @@ opaque
   ·-𝟎ˡ {A} {B} {zero} M = PW.[]
   ·-𝟎ˡ {A} {B} {suc C} M = [⟨0⟩]- M PW.∷ ·-𝟎ˡ M
 
+·-[+]ˡ
+    : (W : Matrix B C)
+      (Y Z : Matrix A B)
+    → W · (Y [+] Z) ≋ (W · Y) [+] (W · Z)
+·-[+]ˡ {C = C} {A = A} W Y Z = begin
+    W · (Y [+] Z)               ≈⟨ ·-resp-≋ ≋.refl ([+]-cong ·-Iˡ ·-Iˡ) ⟨
+    W · ((I · Y) [+] (I · Z))   ≈⟨ ·-resp-≋ ≋.refl (∥-·-≑ I I Y Z) ⟨
+    W · (I ∥ I) · (Y ≑ Z)       ≈⟨ ·-assoc ⟨
+    (W · (I ∥ I)) · (Y ≑ Z)     ≡⟨ ≡.cong (_· (Y ≑ Z)) (·-∥ W I I) ⟩
+    (W · I ∥ W · I) · (Y ≑ Z)   ≈⟨ ·-resp-≋ (∥-cong ·-Iʳ ·-Iʳ) ≋.refl ⟩
+    (W ∥ W) · (Y ≑ Z)           ≈⟨ ∥-·-≑ W W Y Z ⟩
+    (W · Y) [+] (W · Z)         ∎
+  where
+    open ≈-Reasoning (Matrixₛ A C)
+
+·-[+]ʳ
+    : (W : Matrix A B)
+      (Y Z : Matrix B C)
+    → (Y [+] Z) · W ≋ (Y · W) [+] (Z · W)
+·-[+]ʳ {A = A} {C = C} W Y Z = begin
+    (Y [+] Z) · W                 ≈⟨ ·-resp-≋ ([+]-cong ·-Iʳ ·-Iʳ) ≋.refl ⟨
+    ((Y · I) [+] (Z · I)) · W     ≈⟨ ·-resp-≋ (∥-·-≑ Y Z I I) ≋.refl ⟨
+    ((Y ∥ Z) · (I ≑ I)) · W       ≈⟨ ·-assoc ⟩
+    (Y ∥ Z) · ((I ≑ I) · W)       ≡⟨ ≡.cong ((Y ∥ Z) ·_) (≑-· I I W) ⟩
+    (Y ∥ Z) · ((I · W) ≑ (I · W)) ≈⟨ ·-resp-≋ ≋.refl (≑-cong ·-Iˡ ·-Iˡ) ⟩
+    (Y ∥ Z) · (W ≑ W)             ≈⟨ ∥-·-≑ Y Z W W ⟩
+    (Y · W) [+] (Z · W)           ∎
+  where
+    open ≈-Reasoning (Matrixₛ A C)
+
 -- The category of matrices over a rig
 Mat : Category 0ℓ c (c ⊔ ℓ)
 Mat = categoryHelper record
diff --git a/Data/Matrix/Dagger-2-Poset.agda b/Data/Matrix/Dagger-2-Poset.agda
index 1b7b07f..319b4f9 100644
--- a/Data/Matrix/Dagger-2-Poset.agda
+++ b/Data/Matrix/Dagger-2-Poset.agda
@@ -45,32 +45,10 @@ opaque
   [+]-idem [] = PW.[]
   [+]-idem (M₀ ∷ M) = ⊕-idem M₀ PW.∷ [+]-idem M
 
-+-[+] : (M N : Matrix A B) → (I ∥ I) · ((M · (I ∥ 𝟎)) ≑ (N · (𝟎 ∥ I))) · (I ≑ I) ≋ M [+] N
-+-[+] M N = begin
-    (I ∥ I) · ((M · (I ∥ 𝟎)) ≑ (N · (𝟎 ∥ I))) · (I ≑ I)         ≡⟨ ≡.cong₂ (λ h₁ h₂ → (I ∥ I) · (h₁ ≑ h₂) · (I ≑ I)) (·-∥ M I 𝟎) (·-∥ N 𝟎 I) ⟩
-    (I ∥ I) · ((M · I) ∥ (M · 𝟎) ≑ (N · 𝟎) ∥ (N · I)) · (I ≑ I) ≈⟨ ·-resp-≋ ≋.refl (·-resp-≋ (≑-cong (∥-cong ·-Iʳ (·-𝟎ʳ M)) (∥-cong (·-𝟎ʳ N) ·-Iʳ)) ≋.refl) ⟩
-    (I ∥ I) · ((M ∥ 𝟎) ≑ (𝟎 ∥ N)) · (I ≑ I)                     ≡⟨ ≡.cong ((I ∥ I) ·_) (≑-· (M ∥ 𝟎) (𝟎 ∥ N) (I ≑ I)) ⟩
-    (I ∥ I) · (((M ∥ 𝟎) · (I ≑ I)) ≑ ((𝟎 ∥ N) · (I ≑ I)))       ≈⟨ ∥-·-≑ I I ((M ∥ 𝟎) · (I ≑ I)) ((𝟎 ∥ N) · (I ≑ I)) ⟩
-    (I · (M ∥ 𝟎) · (I ≑ I)) [+] (I · (𝟎 ∥ N) · (I ≑ I))         ≈⟨ [+]-cong ·-Iˡ ·-Iˡ ⟩
-    ((M ∥ 𝟎) · (I ≑ I)) [+] ((𝟎 ∥ N) · (I ≑ I))                 ≈⟨ [+]-cong (∥-·-≑ M 𝟎 I I) (∥-·-≑ 𝟎 N I I) ⟩
-    ((M · I) [+] (𝟎 · I)) [+] ((𝟎 · I) [+] (N · I))             ≈⟨ [+]-cong ([+]-cong ·-Iʳ ·-Iʳ) ([+]-cong ·-Iʳ ·-Iʳ) ⟩
-    (M [+] 𝟎) [+] (𝟎 [+] N)                                     ≈⟨ [+]-cong ([+]-𝟎ʳ M) ([+]-𝟎ˡ N) ⟩
-    M [+] N                                                     ∎
-  where
-    open ≈-Reasoning (Matrixₛ _ _)
-
-idem : (M : Matrix A B) → (I ∥ I) · ((M · (I ∥ 𝟎)) ≑ (M · (𝟎 ∥ I))) · (I ≑ I) ≋ M
-idem M = begin
-    (I ∥ I) · ((M · (I ∥ 𝟎)) ≑ (M · (𝟎 ∥ I))) · (I ≑ I) ≈⟨ +-[+] M M ⟩
-    M [+] M                                             ≈⟨ [+]-idem M ⟩
-    M                                                   ∎
-  where
-    open ≈-Reasoning (Matrixₛ _ _)
-
 Mat-IdempotentSemiadditiveDagger : IdempotentSemiadditiveDagger Mat
 Mat-IdempotentSemiadditiveDagger = record
     { semiadditiveDagger = Mat-SemiadditiveDagger
-    ; idempotent = idem _
+    ; idempotent = [+]-idem _
     }
 
 open IdempotentSemiadditiveDagger Mat-IdempotentSemiadditiveDagger
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
diff --git a/Data/WiringDiagram/Equalities.agda b/Data/WiringDiagram/Equalities.agda
index 1c3928e..a932c61 100644
--- a/Data/WiringDiagram/Equalities.agda
+++ b/Data/WiringDiagram/Equalities.agda
@@ -57,9 +57,9 @@ loop∘push∘loop≈merge f id≤f†∘f = ≈ᵢ ⌸ (identityˡ ○ identity
         ∇ ∘ id ×₁ ∇ ∘ ⟨ π₁ , (f † ∘ f) ×₁ (f †) ⟩                             ≈⟨ refl⟩∘⟨ pushʳ (sym assocˡ∘⟨⟩) ⟩
         ∇ ∘ (id ×₁ ∇ ∘ assocˡ) ∘ ⟨ ⟨ π₁ , (f † ∘ f) ∘ π₁ ⟩ , f † ∘ π₂ ⟩       ≈⟨ refl⟩∘⟨ refl⟩∘⟨ ⟨⟩-congʳ (⟨⟩-congʳ identityˡ) ⟨
         ∇ ∘ (id ×₁ ∇ ∘ assocˡ) ∘ ⟨ ⟨ id ∘ π₁ , (f † ∘ f) ∘ π₁ ⟩ , f † ∘ π₂ ⟩  ≈⟨ refl⟩∘⟨ refl⟩∘⟨ ⟨⟩-congʳ ⟨⟩∘ ⟨
-        ∇ ∘ (id ×₁ ∇ ∘ assocˡ) ∘ ⟨ id , f † ∘ f ⟩ ×₁ (f †)                    ≈⟨ refl⟩∘⟨ refl⟩∘⟨ ×₁-congʳ ×₁∘Δ ⟨
-        ∇ ∘ (id ×₁ ∇ ∘ assocˡ) ∘ (id ×₁ (f † ∘ f) ∘ Δ) ×₁ (f †)               ≈⟨ extendʳ ∇-assoc-×₁ ⟨
-        ∇ ∘ (∇ ×₁ id) ∘ (id ×₁ (f † ∘ f) ∘ Δ) ×₁ (f †)                        ≈⟨ refl⟩∘⟨ first∘×₁ ⟩
+        ∇ ∘ (id ×₁ ∇ ∘ assocˡ) ∘ ⟨ id , f † ∘ f ⟩ ×₁ (f †)                    ≈⟨ extendʳ ∇-assoc-×₁ ⟨
+        ∇ ∘ (∇ ×₁ id) ∘ ⟨ id , f † ∘ f ⟩ ×₁ (f †)                             ≈⟨ refl⟩∘⟨ first∘×₁ ⟩
+        ∇ ∘ (∇ ∘ ⟨ id , f † ∘ f ⟩) ×₁ (f †)                                   ≈⟨ refl⟩∘⟨ ×₁-congʳ +-∇∘⟨⟩ ⟨
         ∇ ∘ (id + (f † ∘ f)) ×₁ (f †)                                         ≈⟨ refl⟩∘⟨ ×₁-congʳ id≤f†∘f ⟩
         ∇ ∘ (f † ∘ f) ×₁ (f †)                                                ≈⟨ refl⟩∘⟨ ×₁∘first ⟨
         ∇ ∘ (f †) ×₁ (f †) ∘ f ×₁ id                                          ≈⟨ extendʳ ⇒∇-×₁ ⟨
@@ -93,6 +93,8 @@ loop∘pull∘loop≈split f f∘f†≤id = ≈ᵢ ⌸ (identityˡ ○ identity
         ∇ ∘ (id ×₁ ∇ ∘ assocˡ) ∘ (id ×₁ (f ∘ f †)) ×₁ f ∘ Δ ×₁ id                   ≈⟨ extendʳ ∇-assoc-×₁ ⟨
         ∇ ∘ ∇ ×₁ id ∘ (id ×₁ (f ∘ f †)) ×₁ f ∘ Δ ×₁ id                              ≈⟨ refl⟩∘⟨ refl⟩∘⟨ ×₁∘first ⟩
         ∇ ∘ ∇ ×₁ id ∘ (id ×₁ (f ∘ f †) ∘ Δ) ×₁ f                                    ≈⟨ refl⟩∘⟨ first∘×₁ ⟩
+        ∇ ∘ (∇ ∘ id ×₁ (f ∘ f †) ∘ Δ) ×₁ f                                          ≈⟨ refl⟩∘⟨ ×₁-congʳ (refl⟩∘⟨ ×₁∘Δ) ⟩
+        ∇ ∘ (∇ ∘ ⟨ id , f ∘ f † ⟩) ×₁ f                                             ≈⟨ refl⟩∘⟨ ×₁-congʳ +-∇∘⟨⟩ ⟨
         ∇ ∘ (id + (f ∘ f †)) ×₁ f                                                   ≈⟨ refl⟩∘⟨ ×₁-congʳ (+-comm id (f ∘ f †)) ⟩
         ∇ ∘ ((f ∘ f †) + id) ×₁ f                                                   ≈⟨ refl⟩∘⟨ ×₁-congʳ f∘f†≤id ⟩
         ∇ ∘ id ×₁ f                                                                 ∎