From 514bb6e3e235f37c4e49bd703ad02a5ab31e8c0a Mon Sep 17 00:00:00 2001
From: Jacques Comeaux <jacquesrcomeaux@protonmail.com>
Date: Mon, 3 Aug 2026 19:08:47 -0500
Subject: Show category of maps is monoidal

---
 Data/WiringDiagram/Monoidal/Core.agda | 24 ++----------------------
 1 file changed, 2 insertions(+), 22 deletions(-)

(limited to 'Data/WiringDiagram/Monoidal/Core.agda')

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}
-- 
cgit v1.2.3