Show category of maps is monoidal

3 files changed, 22 insertions, 59 deletions

diff --git a/Data/WiringDiagram/Monoidal.agda b/Data/WiringDiagram/Monoidal.agda
index 3d7ea78..96ff101 100644
--- a/Data/WiringDiagram/Monoidal.agda
+++ b/Data/WiringDiagram/Monoidal.agda
@@ -28,7 +28,7 @@ open import Data.WiringDiagram.Balanced S using (BWD; Push; Pull)
 open import Data.WiringDiagram.Core S using (_□_; _⧈_; id-⧈; _≈-⧈_; _⌸_; _⌻_)
 open import Data.WiringDiagram.Directed S using (DWD; Pulsh)
 open import Data.WiringDiagram.Monoidal.Braided S using (swap-⧈; DWD-Braided) public
-open import Data.WiringDiagram.Monoidal.Core S using (DWD-Monoidal; BWD-Monoidal; _⊞_; _⊞₁_; σ₂₃; associator⇒; unitorˡ⇒; unitorʳ⇒; ⊞-identity) public
+open import Data.WiringDiagram.Monoidal.Core S using (DWD-Monoidal; BWD-Monoidal; _⊞_; _⊞₁_; associator⇒; unitorˡ⇒; unitorʳ⇒; ⊞-identity) public
 open import Data.WiringDiagram.Monoidal.Symmetric S using (DWD-Symmetric; BWD-Symmetric) public
 
 module DWD = Category DWD
@@ -141,23 +141,19 @@ module Directed where
 
   unitaryˡ
       : {A B : Obj}
-      → Pulsh.₁ (⟨ ! {A} , id {A} ⟩ , π₂ {𝟘} {B}) ⌻ id-⧈ ⌻ id-⧈ ⊞₁ id-⧈
+      → Pulsh.₁ (i₂ {𝟘} {A} , π₂ {𝟘} {B}) ⌻ id-⧈ ⌻ id-⧈ ⊞₁ id-⧈
       ≈-⧈ unitorˡ⇒
   unitaryˡ = begin
-      Pulsh.₁ (⟨ ! , id ⟩ , π₂) ⌻ id-⧈ ⌻ id-⧈ ⊞₁ id-⧈ ≈⟨ elimʳ (elimʳ ⊞-identity) ⟩
-      Pulsh.₁ (⟨ ! , id ⟩ , π₂)                       ≈⟨ Pulsh.F-resp-≈ (⟨⟩-congʳ (!-unique zero⇒) , refl) ⟩
-      Pulsh.₁ (⟨ zero⇒ , id ⟩ , π₂)                   ≈⟨ Pulsh.F-resp-≈ (⟨⟩-unique π₁∘i₂≈0 π₂∘i₂≈id , refl) ⟩
-      unitorˡ⇒                                        ∎
+      Pulsh.₁ (i₂ , π₂) ⌻ id-⧈ ⌻ id-⧈ ⊞₁ id-⧈ ≈⟨ elimʳ (elimʳ ⊞-identity) ⟩
+      unitorˡ⇒                                ∎
 
   unitaryʳ
       : {A B : Obj}
-      → Pulsh.₁ (⟨ id {A} , ! {A} ⟩ , π₁ {B} {𝟘}) ⌻ id-⧈ ⌻ id-⧈ ⊞₁ id-⧈
+      → Pulsh.₁ (i₁ {A} {𝟘} , π₁ {B} {𝟘}) ⌻ id-⧈ ⌻ id-⧈ ⊞₁ id-⧈
       ≈-⧈ unitorʳ⇒
   unitaryʳ = begin
-      Pulsh.₁ (⟨ id , ! ⟩ , π₁) ⌻ id-⧈ ⌻ id-⧈ ⊞₁ id-⧈ ≈⟨ elimʳ (elimʳ ⊞-identity) ⟩
-      Pulsh.₁ (⟨ id , ! ⟩ , π₁)                       ≈⟨ Pulsh.F-resp-≈ (⟨⟩-congˡ (!-unique zero⇒) , refl) ⟩
-      Pulsh.₁ (⟨ id , zero⇒ ⟩ , π₁)                   ≈⟨ Pulsh.F-resp-≈ (⟨⟩-unique π₁∘i₁≈id π₂∘i₁≈0 , refl) ⟩
-      unitorʳ⇒                                        ∎
+      Pulsh.₁ (i₁ , π₁) ⌻ id-⧈ ⌻ id-⧈ ⊞₁ id-⧈ ≈⟨ elimʳ (elimʳ ⊞-identity) ⟩
+      unitorʳ⇒                                ∎
 
   braiding-compat
       : {A B C D : Obj}
@@ -302,25 +298,21 @@ module BalancedPull where
 
   unitaryˡ
       : {A : Obj}
-      → Pull.₁ ⟨ ! {A} , id {A} ⟩ ⌻ id-⧈ ⌻ id-⧈ ⊞₁ id-⧈
+      → Pull.₁ (i₂ {𝟘} {A}) ⌻ id-⧈ ⌻ id-⧈ ⊞₁ id-⧈
       ≈-⧈ unitorˡ⇒
   unitaryˡ = begin
-      Pull.₁ ⟨ ! , id ⟩ ⌻ id-⧈ ⌻ id-⧈ ⊞₁ id-⧈ ≈⟨ elimʳ (elimʳ ⊞-identity) ⟩
-      Pull.₁ ⟨ ! , id ⟩                       ≈⟨ Pull.F-resp-≈ (⟨⟩-congʳ (!-unique zero⇒)) ⟩
-      Pull.₁ ⟨ zero⇒ , id ⟩                   ≈⟨ Pull.F-resp-≈ (⟨⟩-unique π₁∘i₂≈0 π₂∘i₂≈id) ⟩
-      Pull.₁ i₂                               ≈⟨ refl ⌸ i₂† ⟩
-      unitorˡ⇒                                ∎
+      Pull.₁ i₂ ⌻ id-⧈ ⌻ id-⧈ ⊞₁ id-⧈ ≈⟨ elimʳ (elimʳ ⊞-identity) ⟩
+      Pull.₁ i₂                       ≈⟨ refl ⌸ i₂† ⟩
+      unitorˡ⇒                        ∎
 
   unitaryʳ
       : {A : Obj}
-      → Pull.₁ ⟨ id {A} , ! {A} ⟩ ⌻ id-⧈ ⌻ id-⧈ ⊞₁ id-⧈
+      → Pull.₁ (i₁ {A} {𝟘}) ⌻ id-⧈ ⌻ id-⧈ ⊞₁ id-⧈
       ≈-⧈ unitorʳ⇒
   unitaryʳ = begin
-      Pull.₁ ⟨ id , ! ⟩ ⌻ id-⧈ ⌻ id-⧈ ⊞₁ id-⧈ ≈⟨ elimʳ (elimʳ ⊞-identity) ⟩
-      Pull.₁ ⟨ id , ! ⟩                       ≈⟨ Pull.F-resp-≈ (⟨⟩-congˡ (!-unique zero⇒)) ⟩
-      Pull.₁ ⟨ id , zero⇒ ⟩                   ≈⟨ Pull.F-resp-≈ (⟨⟩-unique π₁∘i₁≈id π₂∘i₁≈0) ⟩
-      Pull.₁ i₁                               ≈⟨ refl ⌸ i₁† ⟩
-      unitorʳ⇒                                ∎
+      Pull.₁ i₁ ⌻ id-⧈ ⌻ id-⧈ ⊞₁ id-⧈ ≈⟨ elimʳ (elimʳ ⊞-identity) ⟩
+      Pull.₁ i₁                       ≈⟨ refl ⌸ i₁† ⟩
+      unitorʳ⇒                        ∎
 
   braiding-compat
       : {A B : Obj}
diff --git a/Data/WiringDiagram/Monoidal/Braided.agda b/Data/WiringDiagram/Monoidal/Braided.agda
index 7b28d85..d45d8d2 100644
--- a/Data/WiringDiagram/Monoidal/Braided.agda
+++ b/Data/WiringDiagram/Monoidal/Braided.agda
@@ -11,6 +11,7 @@ module Data.WiringDiagram.Monoidal.Braided
   where
 
 import Categories.Morphism.Reasoning 𝒞 as ⇒-Reasoning
+import Category.Semiadditive.Monoidal as SemiadditiveMonoidal
 import Data.WiringDiagram.Core as WD
 
 open import Categories.Category.Monoidal using (Monoidal)
@@ -21,12 +22,15 @@ open import Categories.Functor.Bifunctor using (flip-bifunctor)
 open import Categories.NaturalTransformation.NaturalIsomorphism using (_≃_; niHelper)
 open import Data.Product using (uncurry; _,_)
 open import Data.WiringDiagram.Monoidal.Core S
-  using (_⊞_; _⊞₁_; σ₂₃; associator⇒; associator⇐; DWD-Monoidal; BWD-Monoidal)
+  using (_⊞_; _⊞₁_; associator⇒; associator⇐; DWD-Monoidal; BWD-Monoidal)
   renaming (module Directed to D; module Balanced to B)
 open import Function using (flip)
 
 open Category 𝒞
 open SemiadditiveDagger S
+
+open SemiadditiveMonoidal semiadditive using (symmetric)
+
 open Symmetric symmetric using (braided; hexagon₁; hexagon₂)
 open WD S using (Box; WiringDiagram; _□_; _⧈_; _≈-⧈_; _⌸_; id-⧈; _⌻_; ≈-sym)
 
@@ -34,19 +38,6 @@ open HomReasoning
 open ⇒-Reasoning
 open Equiv
 
-σ₂₃-⟨⟩
-    : {X A B C D : Obj}
-      {f : X ⇒ A}
-      {g : X ⇒ B}
-      {h : X ⇒ C}
-      {i : X ⇒ D}
-    → σ₂₃ ∘ ⟨ ⟨ f , g ⟩ , ⟨ h , i ⟩ ⟩ ≈ ⟨ ⟨ f , h ⟩ , ⟨ g , i ⟩ ⟩
-σ₂₃-⟨⟩ {f = f} {g} {h} {i} = begin
-    σ₂₃ ∘ ⟨ ⟨ f , g ⟩ , ⟨ h , i ⟩ ⟩                                                 ≈⟨ ⟨⟩∘ ⟩
-    ⟨ π₁ ×₁ π₁ ∘ ⟨ ⟨ f , g ⟩ , ⟨ h , i ⟩ ⟩ , π₂ ×₁ π₂ ∘ ⟨ ⟨ f , g ⟩ , ⟨ h , i ⟩ ⟩ ⟩ ≈⟨ ⟨⟩-cong₂ ×₁∘⟨⟩ ×₁∘⟨⟩ ⟩
-    ⟨ ⟨ π₁ ∘ ⟨ f , g ⟩ , π₁ ∘ ⟨ h , i ⟩ ⟩ , ⟨ π₂ ∘ ⟨ f , g ⟩ , π₂ ∘ ⟨ h , i ⟩ ⟩ ⟩   ≈⟨ ⟨⟩-cong₂ (⟨⟩-cong₂ project₁ project₁) (⟨⟩-cong₂ project₂ project₂) ⟩
-    ⟨ ⟨ f , h ⟩ , ⟨ g , i ⟩ ⟩                                                       ∎
-
 swap-⧈ : (X Y : Box) → WiringDiagram (X ⊞ Y) (Y ⊞ X)
 swap-⧈ X Y = swap ∘ π₂ ⧈ swap
 
diff --git a/Data/WiringDiagram/Monoidal/Core.agda b/Data/WiringDiagram/Monoidal/Core.agda
index 5abd60f..daed109 100644
--- a/Data/WiringDiagram/Monoidal/Core.agda
+++ b/Data/WiringDiagram/Monoidal/Core.agda
@@ -13,33 +13,28 @@ module Data.WiringDiagram.Monoidal.Core
 import Categories.Category.Monoidal.Reasoning as ⊗-Reasoning
 import Categories.Morphism as Morphism
 import Categories.Morphism.Reasoning 𝒞 as ⇒-Reasoning
+import Category.Semiadditive.Monoidal as SemiadditiveMonoidal
 import Data.WiringDiagram.Balanced as BalancedWD
 import Data.WiringDiagram.Core as WD
 import Data.WiringDiagram.Directed as DirectedWD
 
 open import Categories.Category.Monoidal using (Monoidal)
-open import Categories.Category.Monoidal.Symmetric using (module Symmetric)
 open import Categories.Category.Monoidal.Utilities using (pentagon-inv)
 open import Categories.Functor.Bifunctor using (Bifunctor)
 open import Categories.Object.Initial using (Initial; IsInitial)
 open import Data.Product using (_,_; uncurry′)
 
 open SemiadditiveDagger S
+open SemiadditiveMonoidal semiadditive using (monoidal)
 
 open BalancedWD S using (BWD)
 open Category 𝒞
 open DirectedWD S using (DWD)
 open Monoidal monoidal using (triangle; pentagon)
-open Symmetric symmetric using (braided)
 open WD S using (Box; WiringDiagram; _□_; _⧈_; _≈-⧈_; _⌸_; id-⧈; _⌻_; ≈-sym)
 
 module DWD = Category DWD
 
--- Swap middle two of four
-
-σ₂₃ : {A B C D : Obj} → (A ⊕ B) ⊕ (C ⊕ D) ⇒ (A ⊕ C) ⊕ (B ⊕ D)
-σ₂₃ = ⟨ π₁ ×₁ π₁ , π₂ ×₁ π₂ ⟩
-
 -- Monoidal unit and initial object
 
 𝟘-□ : Box
@@ -123,21 +118,6 @@ open Equiv
     ⟨ ⟨ π₁ , id ⟩ ∘ π₁ ×₁ π₁ , ⟨ π₁ , id ⟩ ∘ π₂ ×₁ π₂ ⟩                                           ≈⟨ ×₁∘⟨⟩ ⟨
     ⟨ π₁ , id ⟩ ×₁ ⟨ π₁ , id ⟩ ∘ ⟨ π₁ ×₁ π₁ , π₂ ×₁ π₂ ⟩                                          ∎
 
-σ₂₃-×₁
-    : {A A′ B B′ C C′ D D′ : Obj}
-      {f : A ⇒ A′}
-      {g : B ⇒ B′}
-      {h : C ⇒ C′}
-      {i : D ⇒ D′}
-    → (f ×₁ g) ×₁ (h ×₁ i) ∘ σ₂₃ ≈ σ₂₃ ∘ (f ×₁ h) ×₁ (g ×₁ i)
-σ₂₃-×₁ {f = f} {g} {h} {i} = begin
-    (f ×₁ g) ×₁ (h ×₁ i) ∘ ⟨ π₁ ×₁ π₁ , π₂ ×₁ π₂ ⟩                        ≈⟨ ×₁∘⟨⟩ ⟩
-    ⟨ f ×₁ g ∘ π₁ ×₁ π₁ , h ×₁ i ∘ π₂ ×₁ π₂ ⟩                             ≈⟨ ⟨⟩-cong₂ ×₁∘×₁ ×₁∘×₁ ⟩
-    ⟨ (f ∘ π₁) ×₁ (g ∘ π₁) , (h ∘ π₂) ×₁ (i ∘ π₂) ⟩                       ≈⟨ ⟨⟩-cong₂ (×₁-cong₂ π₁∘×₁ π₁∘×₁) (×₁-cong₂ π₂∘×₁ π₂∘×₁) ⟨
-    ⟨ (π₁ ∘ f ×₁ h) ×₁ (π₁ ∘ g ×₁ i) , (π₂ ∘ f ×₁ h) ×₁ (π₂ ∘ g ×₁ i) ⟩   ≈⟨ ⟨⟩-cong₂ ×₁∘×₁ ×₁∘×₁ ⟨
-    ⟨ π₁ ×₁ π₁ ∘ (f ×₁ h) ×₁ (g ×₁ i) , π₂ ×₁ π₂ ∘ (f ×₁ h) ×₁ (g ×₁ i) ⟩ ≈⟨ ⟨⟩∘ ⟨
-    σ₂₃ ∘ (f ×₁ h) ×₁ (g ×₁ i)                                            ∎
-
 ⊞-homo
     : {A B C D E F : Box}
       {f : WiringDiagram A C}