Show wiring diagram braiding is symmetric

2 files changed, 35 insertions, 0 deletions

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-⧈
+    }