Show wiring diagram braiding is symmetric

1 files changed, 27 insertions, 0 deletions

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