From f70dd41bf5a519ba099ebd6d9a425a022c1a111f Mon Sep 17 00:00:00 2001
From: Jacques Comeaux <jacquesrcomeaux@protonmail.com>
Date: Fri, 31 Jul 2026 20:52:41 -0700
Subject: Show wiring diagram braiding is symmetric

---
 Data/WiringDiagram/Monoidal/Core.agda      |  8 ++++++++
 Data/WiringDiagram/Monoidal/Symmetric.agda | 27 +++++++++++++++++++++++++++
 2 files changed, 35 insertions(+)
 create mode 100644 Data/WiringDiagram/Monoidal/Symmetric.agda

(limited to 'Data/WiringDiagram/Monoidal')

diff --git a/Data/WiringDiagram/Monoidal/Core.agda b/Data/WiringDiagram/Monoidal/Core.agda
index 382e188..5abd60f 100644
--- a/Data/WiringDiagram/Monoidal/Core.agda
+++ b/Data/WiringDiagram/Monoidal/Core.agda
@@ -483,6 +483,8 @@ module Directed where
 
   open Morphism DWD using (_≅_)
 
+  -- Monoidal product bifunctor
+
   -⊞- : Bifunctor DWD DWD DWD
   -⊞- = record
       { F₀ = uncurry′ _⊞_
@@ -492,6 +494,8 @@ module Directed where
       ; F-resp-≈ = uncurry′ ⊞-resp-≈-⧈
       }
 
+  -- Structure isomorphisms
+
   unitorˡ : {X : Box} → 𝟘-□ ⊞ X ≅ X
   unitorˡ {X} = record
       { from = unitorˡ⇒
@@ -532,6 +536,8 @@ module Balanced where
 
   open Morphism BWD using (_≅_)
 
+  -- Monoidal product bifunctor
+
   -⊞- : Bifunctor BWD BWD BWD
   -⊞- = record
       { F₀ = uncurry′ _⊕_
@@ -541,6 +547,8 @@ module Balanced where
       ; F-resp-≈ = uncurry′ ⊞-resp-≈-⧈
       }
 
+  -- Structure isomorphisms
+
   unitorˡ : {X : Obj} → 𝟘 ⊕ X ≅ X
   unitorˡ {X} = record
       { from = unitorˡ⇒
diff --git a/Data/WiringDiagram/Monoidal/Symmetric.agda b/Data/WiringDiagram/Monoidal/Symmetric.agda
new file mode 100644
index 0000000..3ffb458
--- /dev/null
+++ b/Data/WiringDiagram/Monoidal/Symmetric.agda
@@ -0,0 +1,27 @@
+{-# OPTIONS --without-K --safe #-}
+
+open import Categories.Category using (Category)
+open import Category.Dagger.Semiadditive using (SemiadditiveDagger)
+open import Level using (Level)
+
+module Data.WiringDiagram.Monoidal.Symmetric
+    {o ℓ e : Level}
+    {𝒞 : Category o ℓ e}
+    (S : SemiadditiveDagger 𝒞)
+  where
+
+open import Categories.Category.Monoidal.Symmetric using (Symmetric)
+open import Data.WiringDiagram.Monoidal.Braided S using (swap∘swap-⧈; DWD-Braided; BWD-Braided)
+open import Data.WiringDiagram.Monoidal.Core S using (DWD-Monoidal; BWD-Monoidal)
+
+DWD-Symmetric : Symmetric DWD-Monoidal
+DWD-Symmetric = record
+    { braided = DWD-Braided
+    ; commutative = swap∘swap-⧈
+    }
+
+BWD-Symmetric : Symmetric BWD-Monoidal
+BWD-Symmetric = record
+    { braided = BWD-Braided
+    ; commutative = swap∘swap-⧈
+    }
-- 
cgit v1.2.3