From 46f36b99c92225b374900457e02d89e9ffcffb52 Mon Sep 17 00:00:00 2001
From: Jacques Comeaux <jacquesrcomeaux@protonmail.com>
Date: Sat, 14 Mar 2026 16:49:35 -0500
Subject: Refactor wiring diagrams

---
 Data/WiringDiagram/Balanced.agda | 38 ++++++++++++++++++++++++++++++++++++++
 1 file changed, 38 insertions(+)
 create mode 100644 Data/WiringDiagram/Balanced.agda

(limited to 'Data/WiringDiagram/Balanced.agda')

diff --git a/Data/WiringDiagram/Balanced.agda b/Data/WiringDiagram/Balanced.agda
new file mode 100644
index 0000000..09656fc
--- /dev/null
+++ b/Data/WiringDiagram/Balanced.agda
@@ -0,0 +1,38 @@
+{-# OPTIONS --without-K --safe #-}
+
+open import Categories.Category using (Category)
+open import Category.Dagger.Semiadditive using (IdempotentSemiadditiveDagger)
+open import Level using (Level)
+
+module Data.WiringDiagram.Balanced
+    {o ℓ e : Level}
+    {𝒞 : Category o ℓ e}
+    (S : IdempotentSemiadditiveDagger 𝒞)
+  where
+
+open import Categories.Functor using (Functor)
+open import Data.WiringDiagram.Core S using (WiringDiagram; _□_)
+open import Data.WiringDiagram.Directed S using (DWD)
+open import Function using (id)
+
+open Category 𝒞 using (Obj)
+
+-- The category of balanced wiring diagrams
+BWD : Category o ℓ e
+BWD = record
+    { Obj = Obj
+    ; _⇒_ = λ A B → WiringDiagram (A □ A) (B □ B)
+    ; Category DWD
+    }
+
+-- Inclusion functor from BWD to DWD
+Include : Functor BWD DWD
+Include = record
+    { F₀ = λ A → A □ A
+    ; F₁ = id
+    ; identity = Equiv.refl
+    ; homomorphism = Equiv.refl
+    ; F-resp-≈ = id
+    }
+  where
+    open Category DWD using (module Equiv)
-- 
cgit v1.2.3