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 ++++++++
 1 file changed, 8 insertions(+)

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

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ˡ⇒
-- 
cgit v1.2.3