Show category of maps is monoidal

2 files changed, 7 insertions, 36 deletions

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}