Show category of maps is monoidal

1 files changed, 5 insertions, 14 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