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/Symmetric.agda | 27 +++++++++++++++++++++++++++
 1 file changed, 27 insertions(+)
 create mode 100644 Data/WiringDiagram/Monoidal/Symmetric.agda

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

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