From 514bb6e3e235f37c4e49bd703ad02a5ab31e8c0a Mon Sep 17 00:00:00 2001 From: Jacques Comeaux Date: Mon, 3 Aug 2026 19:08:47 -0500 Subject: Show category of maps is monoidal --- Data/WiringDiagram/Monoidal/Braided.agda | 19 +++++-------------- 1 file changed, 5 insertions(+), 14 deletions(-) (limited to 'Data/WiringDiagram/Monoidal/Braided.agda') 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 -- cgit v1.2.3