Refactor wiring diagrams

4 files changed, 352 insertions, 261 deletions

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)
diff --git a/Data/WiringDiagram/Core.agda b/Data/WiringDiagram/Core.agda
new file mode 100644
index 0000000..d2e01cd
--- /dev/null
+++ b/Data/WiringDiagram/Core.agda
@@ -0,0 +1,130 @@
+{-# OPTIONS --without-K --safe #-}
+
+open import Categories.Category using (Category)
+open import Level using (Level)
+open import Category.Dagger.Semiadditive using (IdempotentSemiadditiveDagger)
+
+module Data.WiringDiagram.Core
+    {o ℓ e : Level}
+    {𝒞 : Category o ℓ e}
+    (S : IdempotentSemiadditiveDagger 𝒞)
+  where
+
+open import Categories.Category.Monoidal.Utilities using (module Shorthands)
+open import Relation.Binary using (IsEquivalence)
+
+open Category 𝒞 using (Obj; _∘_; _⇒_; id; _≈_; module Equiv)
+open IdempotentSemiadditiveDagger S using (_⊕₀_; _⊕₁_; p₂; +-monoidal; △; ▽)
+open Shorthands +-monoidal using (α⇒)
+
+-- A "Box" is a pair of objects from the underlying category,
+-- representing input and output ports
+-- +-----------+
+-- |           |
+-- Aᵢ    A     Aₒ
+-- |           |
+-- +-----------+
+record Box : Set o where
+
+  constructor _□_
+
+  field
+    ᵢ : Obj
+    ₒ : Obj
+
+infix 4 _□_
+
+-- A Wiring Diagram between two boxes
+-- is a pair of morphisms from the underlying category
+-- (which can be thought of as generalized relations):
+-- 1. A relation from the output of the inner box
+--    plus the input of the outer box to the input of
+--    the inner box
+-- 2. A relation from the output of the inner box
+--    to the output of the outer box
+-- This choice of definition gives a way to represent
+-- feedback from output to input.
+--
+--          outer box (B)
+-- +--------------------------------+
+-- |                                |
+-- |     /-------------------\      |
+-- |     |                   |      |
+-- |     |    +-------+      |      |
+-- |     \----|       |      |      |
+-- |  Aₒ ⊕ Bᵢ | inner |------+------|
+-- |   ⇒ Aᵢ   |  box  |  Aₒ ⇒ Bₒ    |
+-- |----------|  (A)  |  output     |
+-- | input    |       |  relation   |
+-- | relation +-------+             |
+-- |                                |
+-- +--------------------------------+
+record WiringDiagram (A B : Box) : Set ℓ where
+
+  constructor _⧈_
+
+  private
+    module A = Box A
+    module B = Box B
+
+  field
+    input : A.ₒ ⊕₀ B.ᵢ ⇒ A.ᵢ
+    output : A.ₒ ⇒ B.ₒ
+
+infix 4 _⧈_
+
+-- Two wiring diagrams are equivalent when their
+-- input and output relations are equivalent as
+-- morphism in the underlying category.
+record _≈-⧈_ {A B : Box} (f g : WiringDiagram A B) : Set e where
+
+  constructor _⌸_
+
+  private
+
+    module f = WiringDiagram f
+    module g = WiringDiagram g
+
+  field
+    ≈i : f.input ≈ g.input
+    ≈o : f.output ≈ g.output
+
+infix 4 _≈-⧈_
+
+-- Equivalence of boxes is a legitimate equivalence relation
+module _ {A B : Box} where
+
+  open Equiv
+
+  ≈-refl : {x : WiringDiagram A B} → x ≈-⧈ x
+  ≈-refl = refl ⌸ refl
+
+  ≈-sym : {x y : WiringDiagram A B} → x ≈-⧈ y → y ≈-⧈ x
+  ≈-sym (≈i ⌸ ≈o) = sym ≈i ⌸ sym ≈o
+
+  ≈-trans : {x y z : WiringDiagram A B} → x ≈-⧈ y → y ≈-⧈ z → x ≈-⧈ z
+  ≈-trans (≈i₁ ⌸ ≈o₁) (≈i₂ ⌸ ≈o₂) = trans ≈i₁ ≈i₂ ⌸ trans ≈o₁ ≈o₂
+
+  ≈-isEquiv : IsEquivalence (_≈-⧈_ {A} {B})
+  ≈-isEquiv = record
+      { refl = ≈-refl
+      ; sym = ≈-sym
+      ; trans = ≈-trans
+      }
+
+-- The identity wiring diagram
+id-⧈ : {A : Box} → WiringDiagram A A
+id-⧈ = p₂ ⧈ id
+
+-- Composition of wiring diagrams
+_⌻_ : {A B C : Box} → WiringDiagram B C → WiringDiagram A B → WiringDiagram A C
+_⌻_ {Aᵢ □ Aₒ} {Bᵢ □ Bₒ} {Cᵢ □ Cₒ} (f′ ⧈ g′) (f ⧈ g) = f″ ⧈ g′ ∘ g
+  where
+    f″ : Aₒ ⊕₀ Cᵢ ⇒ Aᵢ
+    f″ = f ∘ id ⊕₁ (f′ ∘ g ⊕₁ id) ∘ α⇒ ∘ △ ⊕₁ id
+
+infixr 9 _⌻_
+
+-- The loop wiring diagram
+loop : {A : Obj} → WiringDiagram (A □ A) (A □ A)
+loop = ▽ ⧈ id
diff --git a/Data/WiringDiagram/Directed.agda b/Data/WiringDiagram/Directed.agda
new file mode 100644
index 0000000..88c6008
--- /dev/null
+++ b/Data/WiringDiagram/Directed.agda
@@ -0,0 +1,184 @@
+{-# 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.Directed
+    {o ℓ e : Level}
+    {𝒞 : Category o ℓ e}
+    (S : IdempotentSemiadditiveDagger 𝒞)
+  where
+
+import Categories.Category.Monoidal.Properties as ⊗-Properties
+import Categories.Category.Monoidal.Reasoning as ⊗-Reasoning
+import Categories.Morphism.Reasoning as ⇒-Reasoning
+
+open import Categories.Category.Helper using (categoryHelper)
+open import Categories.Category.Monoidal using (Monoidal)
+open import Categories.Category.Monoidal.Utilities using (module Shorthands)
+open import Data.WiringDiagram.Core S using (Box; WiringDiagram; _≈-⧈_; _□_; _⧈_; _⌸_; id-⧈; _⌻_; ≈-isEquiv)
+
+open Category 𝒞
+open IdempotentSemiadditiveDagger S
+open Monoidal +-monoidal
+open Shorthands +-monoidal using (α⇒; α⇐; λ⇒; λ⇐; ρ⇒; ρ⇐)
+open ⊗-Properties +-monoidal using (coherence₁)
+
+private
+
+  ⌻-resp-≈ : {A B C : Box} {f h : WiringDiagram B C} {g i : WiringDiagram A B} → f ≈-⧈ h → g ≈-⧈ i → f ⌻ g ≈-⧈ h ⌻ i
+  ⌻-resp-≈ {A} {B} {C} {fᵢ ⧈ fₒ} {hᵢ ⧈ hₒ} {gᵢ ⧈ gₒ} {iᵢ ⧈ iₒ} (fᵢ≈hᵢ ⌸ fₒ≈hₒ) (gᵢ≈iᵢ ⌸ gₒ≈iₒ) = ≈ᵢ ⌸ ∘-resp-≈ fₒ≈hₒ gₒ≈iₒ
+    where
+      open ⊗-Reasoning +-monoidal
+      ≈ᵢ : gᵢ ∘ id ⊕₁ (fᵢ ∘ gₒ ⊕₁ id) ∘ α⇒ ∘ △ {Box.ₒ A} ⊕₁ id
+         ≈ iᵢ ∘ id ⊕₁ (hᵢ ∘ iₒ ⊕₁ id) ∘ α⇒ ∘ △ ⊕₁ id
+      ≈ᵢ = gᵢ≈iᵢ ⟩∘⟨ refl⟩⊗⟨ (fᵢ≈hᵢ ⟩∘⟨ gₒ≈iₒ ⟩⊗⟨refl) ⟩∘⟨refl
+
+  ⌻-assoc : {A B C D : Box} {f : WiringDiagram A B} {g : WiringDiagram B C} {h : WiringDiagram C D} → (h ⌻ g) ⌻ f ≈-⧈ h ⌻ (g ⌻ f)
+  ⌻-assoc {Aᵢ □ Aₒ} {Bᵢ □ Bₒ} {Cᵢ □ Cₒ} {Dᵢ □ Dₒ} {fᵢ ⧈ fₒ} {gᵢ ⧈ gₒ} {hᵢ ⧈ hₒ} = ≈ᵢ ⌸ assoc
+    where
+      open ⊗-Reasoning +-monoidal
+
+      term₁ : Aₒ ⊕₀ Dᵢ ⇒ Cᵢ
+      term₁ = hᵢ ∘ (gₒ ∘ fₒ) ⊕₁ id
+
+      term₂ : Bₒ ⊕₀ Dᵢ ⇒ Cᵢ
+      term₂ = hᵢ ∘ gₒ ⊕₁ id
+
+      term₃ : Aₒ ⊕₀ Cᵢ ⇒ Bᵢ
+      term₃ = gᵢ ∘ fₒ ⊕₁ id
+      open ⇒-Reasoning 𝒞
+
+      lemma₁ : α⇒ {Aₒ ⊕₀ Aₒ} {Aₒ} {Dᵢ} ∘ (α⇐ ∘ id ⊕₁ △) ⊕₁ id ∘ △ ⊕₁ id ≈ △ ⊕₁ id ∘ α⇒ ∘ △ ⊕₁ id
+      lemma₁ = begin
+          α⇒ ∘ (α⇐ ∘ id ⊕₁ △) ⊕₁ id ∘ △ ⊕₁ id       ≈⟨ refl⟩∘⟨ pushˡ split₁ˡ ⟩
+          α⇒ ∘ α⇐ ⊕₁ id ∘ (id ⊕₁ △) ⊕₁ id ∘ △ ⊕₁ id ≈⟨ refl⟩∘⟨ refl⟩∘⟨ merge₁ˡ ⟩
+          α⇒ ∘ α⇐ ⊕₁ id ∘ (id ⊕₁ △ ∘ △) ⊕₁ id       ≈⟨ refl⟩∘⟨ refl⟩∘⟨ △-assoc ⟩⊗⟨refl ⟩
+          α⇒ ∘ α⇐ ⊕₁ id ∘ (α⇒ ∘ △ ⊕₁ id ∘ △) ⊕₁ id  ≈⟨ refl⟩∘⟨ merge₁ʳ ⟩
+          α⇒ ∘ (α⇐ ∘ α⇒ ∘ △ ⊕₁ id ∘ △) ⊕₁ id        ≈⟨ refl⟩∘⟨ cancelˡ associator.isoˡ ⟩⊗⟨refl ⟩
+          α⇒ ∘ (△ ⊕₁ id ∘ △) ⊕₁ id                  ≈⟨ refl⟩∘⟨ split₁ˡ ⟩
+          α⇒ ∘ (△ ⊕₁ id) ⊕₁ id ∘ △ ⊕₁ id            ≈⟨ extendʳ assoc-commute-from ⟩
+          △ ⊕₁ id ⊕₁ id ∘ α⇒ ∘ △ ⊕₁ id              ≈⟨ refl⟩⊗⟨ ⊕.identity ⟩∘⟨refl ⟩
+          △ ⊕₁ id ∘ α⇒ ∘ △ ⊕₁ id                    ∎
+
+      lemma₂ :  △ ⊕₁ id {Dᵢ} ∘ fₒ ⊕₁ id ≈ (fₒ ⊕₁ fₒ) ⊕₁ id ∘ △ ⊕₁ id
+      lemma₂ = begin
+          △ ⊕₁ id ∘ fₒ ⊕₁ id          ≈⟨ merge₁ʳ ⟩
+          (△ ∘ fₒ) ⊕₁ id              ≈⟨ ⇒△ ⟩⊗⟨refl ⟩
+          (fₒ ⊕₁ fₒ ∘ △) ⊕₁ id        ≈⟨ split₁ʳ ⟩
+          (fₒ ⊕₁ fₒ) ⊕₁ id ∘ △ ⊕₁ id  ∎
+
+      ≈ᵢ : fᵢ ∘ id ⊕₁ ((gᵢ ∘ id ⊕₁ (hᵢ ∘ gₒ ⊕₁ id) ∘ α⇒ ∘ △ ⊕₁ id) ∘ fₒ ⊕₁ id) ∘ α⇒ ∘ △ ⊕₁ id
+        ≈ (fᵢ ∘ id ⊕₁ (gᵢ ∘ fₒ ⊕₁ id) ∘ α⇒ ∘ △ ⊕₁ id) ∘ id ⊕₁ (hᵢ ∘ (gₒ ∘ fₒ) ⊕₁ id) ∘ α⇒ ∘ △ ⊕₁ id
+      ≈ᵢ = begin
+          fᵢ ∘ id ⊕₁ ((gᵢ ∘ id ⊕₁ term₂ ∘ α⇒ ∘ △ ⊕₁ id) ∘ fₒ ⊕₁ id) ∘ α⇒ ∘ △ ⊕₁ id
+              ≈⟨ refl⟩∘⟨ refl⟩⊗⟨ extendˡ (extendˡ assoc) ⟩∘⟨refl ⟩
+          fᵢ ∘ id ⊕₁ ((gᵢ ∘ id ⊕₁ term₂ ∘ α⇒) ∘ △ ⊕₁ id ∘ fₒ ⊕₁ id) ∘ α⇒ ∘ △ ⊕₁ id
+              ≈⟨ refl⟩∘⟨ refl⟩⊗⟨ (refl⟩∘⟨ lemma₂) ⟩∘⟨refl ⟩
+          fᵢ ∘ id ⊕₁ ((gᵢ ∘ id ⊕₁ term₂ ∘ α⇒) ∘ (fₒ ⊕₁ fₒ) ⊕₁ id ∘ △ ⊕₁ id) ∘ α⇒ ∘ △ ⊕₁ id
+              ≈⟨ refl⟩∘⟨ refl⟩⊗⟨ extendˡ assoc ⟩∘⟨refl ⟩
+          fᵢ ∘ id ⊕₁ ((gᵢ ∘ id ⊕₁ term₂) ∘ α⇒ ∘ (fₒ ⊕₁ fₒ) ⊕₁ id ∘ △ ⊕₁ id) ∘ α⇒ ∘ △ ⊕₁ id
+              ≈⟨ refl⟩∘⟨ refl⟩⊗⟨ (refl⟩∘⟨ extendʳ assoc-commute-from ) ⟩∘⟨refl ⟩
+          fᵢ ∘ id ⊕₁ ((gᵢ ∘ id ⊕₁ term₂) ∘ fₒ ⊕₁ fₒ ⊕₁ id ∘ α⇒ ∘ △ ⊕₁ id) ∘ α⇒ ∘ △ ⊕₁ id
+              ≈⟨ refl⟩∘⟨ refl⟩⊗⟨ assoc ⟩∘⟨refl ⟩
+          fᵢ ∘ id ⊕₁ (gᵢ ∘ id ⊕₁ term₂ ∘ fₒ ⊕₁ fₒ ⊕₁ id ∘ α⇒ ∘ △ ⊕₁ id) ∘ α⇒ ∘ △ ⊕₁ id
+              ≈⟨ refl⟩∘⟨ refl⟩⊗⟨ (refl⟩∘⟨ pullˡ merge₂ˡ ) ⟩∘⟨refl ⟩
+          fᵢ ∘ id ⊕₁ (gᵢ ∘ fₒ ⊕₁ (term₂ ∘ fₒ ⊕₁ id) ∘ α⇒ ∘ △ ⊕₁ id) ∘ α⇒ ∘ △ ⊕₁ id
+              ≈⟨ refl⟩∘⟨ refl⟩⊗⟨ (refl⟩∘⟨ refl⟩⊗⟨ pullʳ merge₁ʳ ⟩∘⟨refl) ⟩∘⟨refl ⟩
+          fᵢ ∘ id ⊕₁ (gᵢ ∘ fₒ ⊕₁ term₁ ∘ α⇒ ∘ △ ⊕₁ id) ∘ α⇒ ∘ △ ⊕₁ id
+              ≈⟨ refl⟩∘⟨ refl⟩⊗⟨ assoc ⟩∘⟨refl ⟨
+          fᵢ ∘ id ⊕₁ ((gᵢ ∘ fₒ ⊕₁ term₁) ∘ α⇒ ∘ △ ⊕₁ id) ∘ α⇒ ∘ △ ⊕₁ id
+              ≈⟨ refl⟩∘⟨ refl⟩⊗⟨ extendˡ assoc ⟩∘⟨refl ⟨
+          fᵢ ∘ id ⊕₁ ((gᵢ ∘ fₒ ⊕₁ term₁ ∘ α⇒) ∘ △ ⊕₁ id) ∘ α⇒ ∘ △ ⊕₁ id
+              ≈⟨ refl⟩∘⟨ pushˡ split₂ʳ ⟩
+          fᵢ ∘ id ⊕₁ (gᵢ ∘ fₒ ⊕₁ term₁ ∘ α⇒) ∘ id ⊕₁ △ ⊕₁ id ∘ α⇒ ∘ △ ⊕₁ id
+              ≈⟨ refl⟩∘⟨ refl⟩∘⟨ extendʳ assoc-commute-from ⟨
+          fᵢ ∘ id ⊕₁ (gᵢ ∘ fₒ ⊕₁ term₁ ∘ α⇒) ∘ α⇒ ∘ (id ⊕₁ △) ⊕₁ id ∘ △ ⊕₁ id
+              ≈⟨ refl⟩∘⟨ extendʳ (refl⟩⊗⟨ assoc ⟩∘⟨refl) ⟨
+          fᵢ ∘ id ⊕₁ ((gᵢ ∘ fₒ ⊕₁ term₁) ∘ α⇒) ∘ α⇒ ∘ (id ⊕₁ △) ⊕₁ id ∘ △ ⊕₁ id
+              ≈⟨ refl⟩∘⟨ pushˡ split₂ʳ ⟩
+          fᵢ ∘ id ⊕₁ (gᵢ ∘ fₒ ⊕₁ term₁) ∘ id ⊕₁ α⇒ ∘ α⇒ ∘ (id ⊕₁ △) ⊕₁ id ∘ △ ⊕₁ id
+              ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ insertˡ associator.isoʳ ⟩⊗⟨refl ⟩∘⟨refl ⟩
+          fᵢ ∘ id ⊕₁ (gᵢ ∘ fₒ ⊕₁ term₁) ∘ id ⊕₁ α⇒ ∘ α⇒ ∘ (α⇒ ∘ α⇐ ∘ id ⊕₁ △) ⊕₁ id ∘ △ ⊕₁ id
+              ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ pushˡ split₁ʳ ⟩
+          fᵢ ∘ id ⊕₁ (gᵢ ∘ fₒ ⊕₁ term₁) ∘ id ⊕₁ α⇒ ∘ α⇒ ∘ α⇒ ⊕₁ id ∘ (α⇐ ∘ id ⊕₁ △) ⊕₁ id ∘ △ ⊕₁ id
+              ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ assoc ⟨
+          fᵢ ∘ id ⊕₁ (gᵢ ∘ fₒ ⊕₁ term₁) ∘ id ⊕₁ α⇒ ∘ (α⇒ ∘ α⇒ ⊕₁ id) ∘ (α⇐ ∘ id ⊕₁ △) ⊕₁ id ∘ △ ⊕₁ id
+              ≈⟨ refl⟩∘⟨ refl⟩∘⟨ extendʳ pentagon ⟩
+          fᵢ ∘ id ⊕₁ (gᵢ ∘ fₒ ⊕₁ term₁) ∘ α⇒ ∘ α⇒ ∘ (α⇐ ∘ id ⊕₁ △) ⊕₁ id ∘ △ ⊕₁ id
+              ≈⟨ refl⟩∘⟨ refl⟩⊗⟨ pushʳ serialize₁₂ ⟩∘⟨refl ⟩
+          fᵢ ∘ id ⊕₁ (term₃ ∘ id ⊕₁ term₁) ∘ α⇒ ∘ α⇒ ∘ (α⇐ ∘ id ⊕₁ △) ⊕₁ id ∘ △ ⊕₁ id
+              ≈⟨ refl⟩∘⟨ pushˡ split₂ʳ ⟩
+          fᵢ ∘ id ⊕₁ term₃ ∘ id ⊕₁ id ⊕₁ term₁ ∘ α⇒ ∘ α⇒ ∘ (α⇐ ∘ id ⊕₁ △) ⊕₁ id ∘ △ ⊕₁ id
+              ≈⟨ refl⟩∘⟨ refl⟩∘⟨ extendʳ assoc-commute-from ⟨
+          fᵢ ∘ id ⊕₁ term₃ ∘ α⇒ ∘ (id ⊕₁ id) ⊕₁ term₁ ∘ α⇒ ∘ (α⇐ ∘ id ⊕₁ △) ⊕₁ id ∘ △ ⊕₁ id
+              ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ ⊕.identity ⟩⊗⟨refl ⟩∘⟨refl ⟩
+          fᵢ ∘ id ⊕₁ term₃ ∘ α⇒ ∘ id ⊕₁ term₁ ∘ α⇒ ∘ (α⇐ ∘ id ⊕₁ △) ⊕₁ id ∘ △ ⊕₁ id
+              ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ lemma₁ ⟩
+          fᵢ ∘ id ⊕₁ term₃ ∘ α⇒ ∘ id ⊕₁ term₁ ∘ △ ⊕₁ id ∘ α⇒ ∘ △ ⊕₁ id
+              ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ extendʳ (Equiv.sym serialize₂₁ ○ serialize₁₂) ⟩
+          fᵢ ∘ id ⊕₁ term₃ ∘ α⇒ ∘ △ ⊕₁ id ∘ id ⊕₁ term₁ ∘ α⇒ ∘ △ ⊕₁ id
+              ≈⟨ refl⟩∘⟨ refl⟩∘⟨ assoc ⟨
+          fᵢ ∘ id ⊕₁ term₃ ∘ (α⇒ ∘ △ ⊕₁ id) ∘ id ⊕₁ term₁ ∘ α⇒ ∘ △ ⊕₁ id
+              ≈⟨ refl⟩∘⟨ assoc ⟨
+          fᵢ ∘ (id ⊕₁ term₃ ∘ α⇒ ∘ △ ⊕₁ id) ∘ id ⊕₁ term₁ ∘ α⇒ ∘ △ ⊕₁ id
+              ≈⟨ assoc ⟨
+          (fᵢ ∘ id ⊕₁ term₃ ∘ α⇒ ∘ △ ⊕₁ id) ∘ id ⊕₁ term₁ ∘ α⇒ ∘ △ ⊕₁ id ∎
+
+  ⌻-identityˡ : {A B : Box} {f : WiringDiagram A B} → id-⧈ ⌻ f ≈-⧈ f
+  ⌻-identityˡ {Aᵢ □ Aₒ} {Bᵢ □ Bₒ} {fᵢ ⧈ fₒ} = ≈ᵢ ⌸ identityˡ
+    where
+      open ⇒-Reasoning 𝒞
+      open ⊗-Reasoning +-monoidal
+      ≈ᵢ : fᵢ ∘ id ⊕₁ (p₂ ∘ fₒ ⊕₁ id) ∘ α⇒ ∘ △ ⊕₁ id ≈ fᵢ
+      ≈ᵢ = begin
+          fᵢ ∘ id ⊕₁ (p₂ ∘ fₒ ⊕₁ id) ∘ α⇒ ∘ △ ⊕₁ id             ≈⟨ refl⟩∘⟨ refl⟩⊗⟨ (p₂-⊕ ⟩∘⟨refl) ⟩∘⟨refl ⟩
+          fᵢ ∘ id ⊕₁ ((λ⇒ ∘ ! ⊕₁ id) ∘ fₒ ⊕₁ id) ∘ α⇒ ∘ △ ⊕₁ id ≈⟨ refl⟩∘⟨ refl⟩⊗⟨ pullʳ merge₁ʳ ⟩∘⟨refl ⟩
+          fᵢ ∘ id ⊕₁ (λ⇒ ∘ (! ∘ fₒ) ⊕₁ id) ∘ α⇒ ∘ △ ⊕₁ id       ≈⟨ refl⟩∘⟨ refl⟩⊗⟨ (refl⟩∘⟨ ⇒! ⟩⊗⟨refl) ⟩∘⟨refl ⟩
+          fᵢ ∘ id ⊕₁ (λ⇒ ∘ ! ⊕₁ id) ∘ α⇒ ∘ △ ⊕₁ id              ≈⟨ refl⟩∘⟨ pushˡ split₂ʳ ⟩
+          fᵢ ∘ id ⊕₁ λ⇒ ∘ id ⊕₁ ! ⊕₁ id ∘ α⇒ ∘ △ ⊕₁ id          ≈⟨ refl⟩∘⟨ refl⟩∘⟨ extendʳ assoc-commute-from ⟨
+          fᵢ ∘ id ⊕₁ λ⇒ ∘ α⇒ ∘ (id ⊕₁ !) ⊕₁ id ∘ △ ⊕₁ id        ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ merge₁ˡ ⟩
+          fᵢ ∘ id ⊕₁ λ⇒ ∘ α⇒ ∘ (id ⊕₁ ! ∘ △) ⊕₁ id              ≈⟨ refl⟩∘⟨ pullˡ triangle ⟩
+          fᵢ ∘ ρ⇒ ⊕₁ id ∘ (id ⊕₁ ! ∘ △) ⊕₁ id                   ≈⟨ refl⟩∘⟨ merge₁ʳ ⟩
+          fᵢ ∘ (ρ⇒ ∘ id ⊕₁ ! ∘ △) ⊕₁ id                         ≈⟨ refl⟩∘⟨ (refl⟩∘⟨ △-identityʳ ) ⟩⊗⟨refl ⟩
+          fᵢ ∘ (ρ⇒ ∘ ρ⇐) ⊕₁ id                                  ≈⟨ refl⟩∘⟨ unitorʳ.isoʳ ⟩⊗⟨refl  ⟩
+          fᵢ ∘ id ⊕₁ id                                         ≈⟨ elimʳ ⊕.identity ⟩
+          fᵢ                                                    ∎
+
+  ⌻-identityʳ : {A B : Box} {f : WiringDiagram A B} → f ⌻ id-⧈ ≈-⧈ f
+  ⌻-identityʳ {Aᵢ □ Aₒ} {Bᵢ □ Bₒ} {fᵢ ⧈ fₒ} = ≈ᵢ ⌸ identityʳ
+    where
+      open ⇒-Reasoning 𝒞
+      open ⊗-Reasoning +-monoidal
+      ≈ᵢ : p₂ ∘ id ⊕₁ (fᵢ ∘ id ⊕₁ id) ∘ α⇒ ∘ △ ⊕₁ id ≈ fᵢ
+      ≈ᵢ = begin
+          p₂ ∘ id ⊕₁ (fᵢ ∘ id ⊕₁ id) ∘ α⇒ ∘ △ ⊕₁ id             ≈⟨ p₂-⊕ ⟩∘⟨refl ⟩
+          (λ⇒ ∘ ! ⊕₁ id) ∘ id ⊕₁ (fᵢ ∘ id ⊕₁ id) ∘ α⇒ ∘ △ ⊕₁ id ≈⟨ refl⟩∘⟨ refl⟩⊗⟨ elimʳ ⊕.identity ⟩∘⟨refl ⟩
+          (λ⇒ ∘ ! ⊕₁ id) ∘ id ⊕₁ fᵢ ∘ α⇒ ∘ △ ⊕₁ id              ≈⟨ pullˡ (pullʳ (Equiv.sym serialize₁₂)) ⟩
+          (λ⇒ ∘ ! ⊕₁ fᵢ) ∘ α⇒ ∘ △ ⊕₁ id                         ≈⟨ pullʳ (pushˡ serialize₂₁) ⟩
+          λ⇒ ∘ id ⊕₁ fᵢ ∘ ! ⊕₁ id ∘ α⇒ ∘ △ ⊕₁ id                ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩⊗⟨ ⊕.identity ⟩∘⟨refl ⟨
+          λ⇒ ∘ id ⊕₁ fᵢ ∘ ! ⊕₁ id ⊕₁ id ∘ α⇒ ∘ △ ⊕₁ id          ≈⟨ refl⟩∘⟨ refl⟩∘⟨ extendʳ assoc-commute-from ⟨
+          λ⇒ ∘ id ⊕₁ fᵢ ∘ α⇒ ∘ (! ⊕₁ id) ⊕₁ id ∘ △ ⊕₁ id        ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ merge₁ʳ ⟩
+          λ⇒ ∘ id ⊕₁ fᵢ ∘ α⇒ ∘ (! ⊕₁ id ∘ △) ⊕₁ id              ≈⟨ extendʳ unitorˡ-commute-from ⟩
+          fᵢ ∘ λ⇒ ∘ α⇒ ∘ (! ⊕₁ id ∘ △) ⊕₁ id                    ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ △-identityˡ ⟩⊗⟨refl ⟩
+          fᵢ ∘ λ⇒ ∘ α⇒ ∘ λ⇐ ⊕₁ id                               ≈⟨ refl⟩∘⟨ pullˡ coherence₁ ⟩
+          fᵢ ∘ λ⇒ ⊕₁ id ∘ λ⇐ ⊕₁ id                              ≈⟨ refl⟩∘⟨ merge₁ʳ ⟩
+          fᵢ ∘ (λ⇒ ∘ λ⇐) ⊕₁ id                                  ≈⟨ refl⟩∘⟨ unitorˡ.isoʳ ⟩⊗⟨refl ⟩
+          fᵢ ∘ id ⊕₁ id                                         ≈⟨ elimʳ ⊕.identity ⟩
+          fᵢ                                                    ∎
+
+-- The category of directed wiring diagrams
+DWD : Category o ℓ e
+DWD = categoryHelper record
+    { Obj = Box
+    ; _⇒_ = WiringDiagram
+    ; _≈_ = _≈-⧈_
+    ; id = id-⧈
+    ; _∘_ = _⌻_
+    ; assoc = ⌻-assoc
+    ; identityˡ = ⌻-identityˡ
+    ; identityʳ = ⌻-identityʳ
+    ; equiv = ≈-isEquiv
+    ; ∘-resp-≈ = ⌻-resp-≈
+    }
diff --git a/Data/WiringDiagram/Full.agda b/Data/WiringDiagram/Full.agda
deleted file mode 100644
index 8cfe9eb..0000000
--- a/Data/WiringDiagram/Full.agda
+++ /dev/null
@@ -1,261 +0,0 @@
-{-# OPTIONS --without-K --safe #-}
-
-open import Categories.Category using (Category)
-open import Categories.Category.Monoidal using (Monoidal)
-open import Level using (Level)
-
-module Data.WiringDiagram.Full {o ℓ e : Level} {𝒞 : Category o ℓ e} (M : Monoidal 𝒞) where
-
-open import Categories.Category.Helper using (categoryHelper)
-open import Relation.Binary using (IsEquivalence)
-
-module U = Category 𝒞
-module M = Monoidal M
-open M
-
-record Box : Set o where
-
-  constructor _□_
-
-  field
-    ᵢ : U.Obj
-    ₒ : U.Obj
-
-infix 4 _□_
-
-record WiringDiagram (A B : Box) : Set ℓ where
-
-  constructor _⧈_
-
-  private
-    module A = Box A
-    module B = Box B
-
-  field
-    input : A.ₒ ⊗₀ B.ᵢ U.⇒ A.ᵢ
-    output : A.ₒ U.⇒ B.ₒ
-
-infix 4 _⧈_
-
-record _≈_ {A B : Box} (f g : WiringDiagram A B) : Set e where
-
-  constructor _⌸_
-
-  private
-
-    module f = WiringDiagram f
-    module g = WiringDiagram g
-
-  field
-    ≈i : f.input U.≈ g.input
-    ≈o : f.output U.≈ g.output
-
-infix 4 _≈_
-
-module _ {A B : Box} where
-
-  ≈-refl : {x : WiringDiagram A B} → x ≈ x
-  ≈-refl = U.Equiv.refl ⌸ U.Equiv.refl
-
-  ≈-sym : {x y : WiringDiagram A B} → x ≈ y → y ≈ x
-  ≈-sym (≈i ⌸ ≈o) = U.Equiv.sym ≈i ⌸ U.Equiv.sym ≈o
-
-  ≈-trans : {x y z : WiringDiagram A B} → x ≈ y → y ≈ z → x ≈ z
-  ≈-trans (≈i₁ ⌸ ≈o₁) (≈i₂ ⌸ ≈o₂) = U.Equiv.trans ≈i₁ ≈i₂ ⌸ U.Equiv.trans ≈o₁ ≈o₂
-
-  ≈-isEquiv : IsEquivalence (_≈_ {A} {B})
-  ≈-isEquiv = record
-      { refl = ≈-refl
-      ; sym = ≈-sym
-      ; trans = ≈-trans
-      }
-
-open import Categories.Object.Monoid using (IsMonoid)
-open import Categories.Category.Monoidal.Properties M using (coherence₁) renaming (monoidal-Op to Mᵒᵖ)
-
-comonoid : {A : U.Obj} → IsMonoid Mᵒᵖ A
-comonoid = ?
-
-discard : {A : U.Obj} → A U.⇒ unit
-discard = IsMonoid.η comonoid
-
-copy : {A : U.Obj} → A U.⇒ A ⊗₀ A
-copy = IsMonoid.μ comonoid
-
-module _ {A B : U.Obj} {f : A U.⇒ B} where
-
-  μ⇒ : copy U.∘ f U.≈ f ⊗₁ f U.∘ copy
-  μ⇒ = ?
-
-  η⇒ : discard U.∘ f U.≈ discard
-  η⇒ = ?
-
-⊗-snd : {A B : U.Obj} → A ⊗₀ B U.⇒ B
-⊗-snd {A} {B} = unitorˡ.from U.∘ discard ⊗₁ U.id
-
-id : {A : Box} → WiringDiagram A A
-id {A} = ⊗-snd ⧈ U.id
-
-_∘_ : {A B C : Box} → WiringDiagram B C → WiringDiagram A B → WiringDiagram A C
-_∘_ {Aᵢ □ Aₒ} {Bᵢ □ Bₒ} {Cᵢ □ Cₒ} (f′ ⧈ g′) (f ⧈ g) = f″ ⧈ g′ U.∘ g
-  where
-    f″ : Aₒ ⊗₀ Cᵢ U.⇒ Aᵢ
-    f″ = f U.∘ U.id ⊗₁ (f′ U.∘ g ⊗₁ U.id) U.∘ associator.from U.∘ copy ⊗₁ U.id
-
-import Categories.Category.Monoidal.Reasoning as ⊗-Reasoning
-open import Categories.Category.Monoidal.Utilities M using (module Shorthands)
-open Shorthands using (α⇒; α⇐; λ⇒; λ⇐; ρ⇒; ρ⇐)
-import Categories.Morphism.Reasoning as ⇒-Reasoning
-
-∘-resp-≈ : {A B C : Box} {f h : WiringDiagram B C} {g i : WiringDiagram A B} → f ≈ h → g ≈ i → f ∘ g ≈ h ∘ i
-∘-resp-≈ {A} {B} {C} {fᵢ ⧈ fₒ} {hᵢ ⧈ hₒ} {gᵢ ⧈ gₒ} {iᵢ ⧈ iₒ} (fᵢ≈hᵢ ⌸ fₒ≈hₒ) (gᵢ≈iᵢ ⌸ gₒ≈iₒ) = ≈ᵢ ⌸ U.∘-resp-≈ fₒ≈hₒ gₒ≈iₒ
-  where
-    open ⊗-Reasoning M
-    ≈ᵢ : gᵢ U.∘ U.id ⊗₁ (fᵢ U.∘ gₒ ⊗₁ U.id) U.∘ α⇒ U.∘ copy {Box.ₒ A} ⊗₁ U.id
-       U.≈ iᵢ U.∘ U.id ⊗₁ (hᵢ U.∘ iₒ ⊗₁ U.id) U.∘ α⇒ U.∘ copy ⊗₁ U.id
-    ≈ᵢ = gᵢ≈iᵢ ⟩∘⟨ refl⟩⊗⟨ (fᵢ≈hᵢ ⟩∘⟨ gₒ≈iₒ ⟩⊗⟨refl) ⟩∘⟨refl
-
-assoc : {A B C D : Box} {f : WiringDiagram A B} {g : WiringDiagram B C} {h : WiringDiagram C D} → (h ∘ g) ∘ f ≈ h ∘ (g ∘ f)
-assoc {Aᵢ □ Aₒ} {Bᵢ □ Bₒ} {Cᵢ □ Cₒ} {Dᵢ □ Dₒ} {fᵢ ⧈ fₒ} {gᵢ ⧈ gₒ} {hᵢ ⧈ hₒ} = ≈ᵢ ⌸ U.assoc
-  where
-    open ⊗-Reasoning M
-
-    term₁ : Aₒ ⊗₀ Dᵢ U.⇒ Cᵢ
-    term₁ = hᵢ U.∘ (gₒ U.∘ fₒ) ⊗₁ U.id
-
-    term₂ : Bₒ ⊗₀ Dᵢ U.⇒ Cᵢ
-    term₂ = hᵢ U.∘ gₒ ⊗₁ U.id
-
-    term₃ : Aₒ ⊗₀ Cᵢ U.⇒ Bᵢ
-    term₃ = gᵢ U.∘ fₒ ⊗₁ U.id
-    open ⇒-Reasoning 𝒞
-
-    lemma₁ : α⇒ {Aₒ ⊗₀ Aₒ} {Aₒ} {Dᵢ} U.∘ (α⇐ U.∘ U.id ⊗₁ copy) ⊗₁ U.id U.∘ copy ⊗₁ U.id U.≈ copy ⊗₁ U.id U.∘ α⇒ U.∘ copy ⊗₁ U.id
-    lemma₁ = begin
-        α⇒ U.∘ (α⇐ U.∘ U.id ⊗₁ copy) ⊗₁ U.id U.∘ copy ⊗₁ U.id         ≈⟨ refl⟩∘⟨ pushˡ split₁ˡ ⟩
-        α⇒ U.∘ α⇐ ⊗₁ U.id U.∘ (U.id ⊗₁ copy) ⊗₁ U.id U.∘ copy ⊗₁ U.id ≈⟨ refl⟩∘⟨ refl⟩∘⟨ merge₁ˡ ⟩
-        α⇒ U.∘ α⇐ ⊗₁ U.id U.∘ (U.id ⊗₁ copy U.∘ copy) ⊗₁ U.id         ≈⟨ refl⟩∘⟨ merge₁ˡ ⟩
-        α⇒ U.∘ (α⇐ U.∘ U.id ⊗₁ copy U.∘ copy) ⊗₁ U.id                 ≈⟨ refl⟩∘⟨ U.assoc ⟩⊗⟨refl ⟨
-        α⇒ U.∘ ((α⇐ U.∘ U.id ⊗₁ copy) U.∘ copy) ⊗₁ U.id               ≈⟨ refl⟩∘⟨ IsMonoid.assoc comonoid ⟩⊗⟨refl ⟨
-        α⇒ U.∘ (copy ⊗₁ U.id U.∘ copy) ⊗₁ U.id                        ≈⟨ refl⟩∘⟨ split₁ˡ ⟩
-        α⇒ U.∘ (copy ⊗₁ U.id) ⊗₁ U.id U.∘ copy ⊗₁ U.id                ≈⟨ extendʳ assoc-commute-from ⟩
-        copy ⊗₁ U.id ⊗₁ U.id U.∘ α⇒ U.∘ copy ⊗₁ U.id                  ≈⟨ refl⟩⊗⟨ ⊗.identity ⟩∘⟨refl ⟩
-        copy ⊗₁ U.id U.∘ α⇒ U.∘ copy ⊗₁ U.id                          ∎
-
-    lemma₂ :  copy ⊗₁ U.id U.∘ fₒ ⊗₁ U.id U.≈ (fₒ ⊗₁ fₒ) ⊗₁ U.id U.∘ copy ⊗₁ U.id
-    lemma₂ = begin
-        copy ⊗₁ U.id U.∘ fₒ ⊗₁ U.id         ≈⟨ merge₁ʳ ⟩
-        (copy U.∘ fₒ) ⊗₁ U.id               ≈⟨ μ⇒ ⟩⊗⟨refl ⟩
-        (fₒ ⊗₁ fₒ U.∘ copy) ⊗₁ U.id         ≈⟨ split₁ʳ ⟩
-        (fₒ ⊗₁ fₒ) ⊗₁ U.id U.∘ copy ⊗₁ U.id ∎
-
-    ≈ᵢ : fᵢ U.∘ U.id ⊗₁ ((gᵢ U.∘ U.id ⊗₁ (hᵢ U.∘ gₒ ⊗₁ U.id) U.∘ α⇒ U.∘ copy ⊗₁ U.id) U.∘ fₒ ⊗₁ U.id) U.∘ α⇒ U.∘ copy ⊗₁ U.id
-      U.≈ (fᵢ U.∘ U.id ⊗₁ (gᵢ U.∘ fₒ ⊗₁ U.id) U.∘ α⇒ U.∘ copy ⊗₁ U.id) U.∘ U.id ⊗₁ (hᵢ U.∘ (gₒ U.∘ fₒ) ⊗₁ U.id) U.∘ α⇒ U.∘ copy ⊗₁ U.id
-    ≈ᵢ = begin
-        fᵢ U.∘ U.id ⊗₁ ((gᵢ U.∘ U.id ⊗₁ term₂ U.∘ α⇒ U.∘ copy ⊗₁ U.id) U.∘ fₒ ⊗₁ U.id) U.∘ α⇒ U.∘ copy ⊗₁ U.id
-            ≈⟨ refl⟩∘⟨ refl⟩⊗⟨ extendˡ (extendˡ U.assoc) ⟩∘⟨refl ⟩
-        fᵢ U.∘ U.id ⊗₁ ((gᵢ U.∘ U.id ⊗₁ term₂ U.∘ α⇒) U.∘ copy ⊗₁ U.id U.∘ fₒ ⊗₁ U.id) U.∘ α⇒ U.∘ copy ⊗₁ U.id
-            ≈⟨ refl⟩∘⟨ refl⟩⊗⟨ (refl⟩∘⟨ lemma₂) ⟩∘⟨refl ⟩
-        fᵢ U.∘ U.id ⊗₁ ((gᵢ U.∘ U.id ⊗₁ term₂ U.∘ α⇒) U.∘ (fₒ ⊗₁ fₒ) ⊗₁ U.id U.∘ copy ⊗₁ U.id) U.∘ α⇒ U.∘ copy ⊗₁ U.id
-            ≈⟨ refl⟩∘⟨ refl⟩⊗⟨ extendˡ U.assoc ⟩∘⟨refl ⟩
-        fᵢ U.∘ U.id ⊗₁ ((gᵢ U.∘ U.id ⊗₁ term₂) U.∘ α⇒ U.∘ (fₒ ⊗₁ fₒ) ⊗₁ U.id U.∘ copy ⊗₁ U.id) U.∘ α⇒ U.∘ copy ⊗₁ U.id
-            ≈⟨ refl⟩∘⟨ refl⟩⊗⟨ (refl⟩∘⟨ extendʳ assoc-commute-from ) ⟩∘⟨refl ⟩
-        fᵢ U.∘ U.id ⊗₁ ((gᵢ U.∘ U.id ⊗₁ term₂) U.∘ fₒ ⊗₁ fₒ ⊗₁ U.id U.∘ α⇒ U.∘ copy ⊗₁ U.id) U.∘ α⇒ U.∘ copy ⊗₁ U.id
-            ≈⟨ refl⟩∘⟨ refl⟩⊗⟨ U.assoc ⟩∘⟨refl ⟩
-        fᵢ U.∘ U.id ⊗₁ (gᵢ U.∘ U.id ⊗₁ term₂ U.∘ fₒ ⊗₁ fₒ ⊗₁ U.id U.∘ α⇒ U.∘ copy ⊗₁ U.id) U.∘ α⇒ U.∘ copy ⊗₁ U.id
-            ≈⟨ refl⟩∘⟨ refl⟩⊗⟨ (refl⟩∘⟨ pullˡ merge₂ˡ ) ⟩∘⟨refl ⟩
-        fᵢ U.∘ U.id ⊗₁ (gᵢ U.∘ fₒ ⊗₁ (term₂ U.∘ fₒ ⊗₁ U.id) U.∘ α⇒ U.∘ copy ⊗₁ U.id) U.∘ α⇒ U.∘ copy ⊗₁ U.id
-            ≈⟨ refl⟩∘⟨ refl⟩⊗⟨ (refl⟩∘⟨ refl⟩⊗⟨ pullʳ merge₁ʳ ⟩∘⟨refl) ⟩∘⟨refl ⟩
-        fᵢ U.∘ U.id ⊗₁ (gᵢ U.∘ fₒ ⊗₁ term₁ U.∘ α⇒ U.∘ copy ⊗₁ U.id) U.∘ α⇒ U.∘ copy ⊗₁ U.id
-            ≈⟨ refl⟩∘⟨ refl⟩⊗⟨ U.assoc ⟩∘⟨refl ⟨
-        fᵢ U.∘ U.id ⊗₁ ((gᵢ U.∘ fₒ ⊗₁ term₁) U.∘ α⇒ U.∘ copy ⊗₁ U.id) U.∘ α⇒ U.∘ copy ⊗₁ U.id
-            ≈⟨ refl⟩∘⟨ refl⟩⊗⟨ extendˡ U.assoc ⟩∘⟨refl ⟨
-        fᵢ U.∘ U.id ⊗₁ ((gᵢ U.∘ fₒ ⊗₁ term₁ U.∘ α⇒) U.∘ copy ⊗₁ U.id) U.∘ α⇒ U.∘ copy ⊗₁ U.id
-            ≈⟨ refl⟩∘⟨ pushˡ split₂ʳ ⟩
-        fᵢ U.∘ U.id ⊗₁ (gᵢ U.∘ fₒ ⊗₁ term₁ U.∘ α⇒) U.∘ U.id ⊗₁ copy ⊗₁ U.id U.∘ α⇒ U.∘ copy ⊗₁ U.id
-            ≈⟨ refl⟩∘⟨ refl⟩∘⟨ extendʳ assoc-commute-from ⟨
-        fᵢ U.∘ U.id ⊗₁ (gᵢ U.∘ fₒ ⊗₁ term₁ U.∘ α⇒) U.∘ α⇒ U.∘ (U.id ⊗₁ copy) ⊗₁ U.id U.∘ copy ⊗₁ U.id
-            ≈⟨ refl⟩∘⟨ extendʳ (refl⟩⊗⟨ U.assoc ⟩∘⟨refl) ⟨
-        fᵢ U.∘ U.id ⊗₁ ((gᵢ U.∘ fₒ ⊗₁ term₁) U.∘ α⇒) U.∘ α⇒ U.∘ (U.id ⊗₁ copy) ⊗₁ U.id U.∘ copy ⊗₁ U.id
-            ≈⟨ refl⟩∘⟨ pushˡ split₂ʳ ⟩
-        fᵢ U.∘ U.id ⊗₁ (gᵢ U.∘ fₒ ⊗₁ term₁) U.∘ U.id ⊗₁ α⇒ U.∘ α⇒ U.∘ (U.id ⊗₁ copy) ⊗₁ U.id U.∘ copy ⊗₁ U.id
-            ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ insertˡ associator.isoʳ ⟩⊗⟨refl ⟩∘⟨refl ⟩
-        fᵢ U.∘ U.id ⊗₁ (gᵢ U.∘ fₒ ⊗₁ term₁) U.∘ U.id ⊗₁ α⇒ U.∘ α⇒ U.∘ (α⇒ U.∘ α⇐ U.∘ U.id ⊗₁ copy) ⊗₁ U.id U.∘ copy ⊗₁ U.id
-            ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ pushˡ split₁ʳ ⟩
-        fᵢ U.∘ U.id ⊗₁ (gᵢ U.∘ fₒ ⊗₁ term₁) U.∘ U.id ⊗₁ α⇒ U.∘ α⇒ U.∘ α⇒ ⊗₁ U.id U.∘ (α⇐ U.∘ U.id ⊗₁ copy) ⊗₁ U.id U.∘ copy ⊗₁ U.id
-            ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ U.assoc ⟨
-        fᵢ U.∘ U.id ⊗₁ (gᵢ U.∘ fₒ ⊗₁ term₁) U.∘ U.id ⊗₁ α⇒ U.∘ (α⇒ U.∘ α⇒ ⊗₁ U.id) U.∘ (α⇐ U.∘ U.id ⊗₁ copy) ⊗₁ U.id U.∘ copy ⊗₁ U.id
-            ≈⟨ refl⟩∘⟨ refl⟩∘⟨ extendʳ pentagon ⟩
-        fᵢ U.∘ U.id ⊗₁ (gᵢ U.∘ fₒ ⊗₁ term₁) U.∘ α⇒ U.∘ α⇒ U.∘ (α⇐ U.∘ U.id ⊗₁ copy) ⊗₁ U.id U.∘ copy ⊗₁ U.id
-            ≈⟨ refl⟩∘⟨ refl⟩⊗⟨ pushʳ serialize₁₂ ⟩∘⟨refl ⟩
-        fᵢ U.∘ U.id ⊗₁ (term₃ U.∘ U.id ⊗₁ term₁) U.∘ α⇒ U.∘ α⇒ U.∘ (α⇐ U.∘ U.id ⊗₁ copy) ⊗₁ U.id U.∘ copy ⊗₁ U.id
-            ≈⟨ refl⟩∘⟨ pushˡ split₂ʳ ⟩
-        fᵢ U.∘ U.id ⊗₁ term₃ U.∘ U.id ⊗₁ U.id ⊗₁ term₁ U.∘ α⇒ U.∘ α⇒ U.∘ (α⇐ U.∘ U.id ⊗₁ copy) ⊗₁ U.id U.∘ copy ⊗₁ U.id
-            ≈⟨ refl⟩∘⟨ refl⟩∘⟨ extendʳ assoc-commute-from ⟨
-        fᵢ U.∘ U.id ⊗₁ term₃ U.∘ α⇒ U.∘ (U.id ⊗₁ U.id) ⊗₁ term₁ U.∘ α⇒ U.∘ (α⇐ U.∘ U.id ⊗₁ copy) ⊗₁ U.id U.∘ copy ⊗₁ U.id
-            ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ ⊗.identity ⟩⊗⟨refl ⟩∘⟨refl ⟩
-        fᵢ U.∘ U.id ⊗₁ term₃ U.∘ α⇒ U.∘ U.id ⊗₁ term₁ U.∘ α⇒ U.∘ (α⇐ U.∘ U.id ⊗₁ copy) ⊗₁ U.id U.∘ copy ⊗₁ U.id
-            ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ lemma₁ ⟩
-        fᵢ U.∘ U.id ⊗₁ term₃ U.∘ α⇒ U.∘ U.id ⊗₁ term₁ U.∘ copy ⊗₁ U.id U.∘ α⇒ U.∘ copy ⊗₁ U.id
-            ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ extendʳ (U.Equiv.sym serialize₂₁ ○ serialize₁₂) ⟩
-        fᵢ U.∘ U.id ⊗₁ term₃ U.∘ α⇒ U.∘ copy ⊗₁ U.id U.∘ U.id ⊗₁ term₁ U.∘ α⇒ U.∘ copy ⊗₁ U.id
-            ≈⟨ refl⟩∘⟨ refl⟩∘⟨ U.assoc ⟨
-        fᵢ U.∘ U.id ⊗₁ term₃ U.∘ (α⇒ U.∘ copy ⊗₁ U.id) U.∘ U.id ⊗₁ term₁ U.∘ α⇒ U.∘ copy ⊗₁ U.id
-            ≈⟨ refl⟩∘⟨ U.assoc ⟨
-        fᵢ U.∘ (U.id ⊗₁ term₃ U.∘ α⇒ U.∘ copy ⊗₁ U.id) U.∘ U.id ⊗₁ term₁ U.∘ α⇒ U.∘ copy ⊗₁ U.id
-            ≈⟨ U.assoc ⟨
-        (fᵢ U.∘ U.id ⊗₁ term₃ U.∘ α⇒ U.∘ copy ⊗₁ U.id) U.∘ U.id ⊗₁ term₁ U.∘ α⇒ U.∘ copy ⊗₁ U.id ∎
-
-identityˡ : {A B : Box} {f : WiringDiagram A B} → id ∘ f ≈ f
-identityˡ {Aᵢ □ Aₒ} {Bᵢ □ Bₒ} {fᵢ ⧈ fₒ} = ≈ᵢ ⌸ U.identityˡ
-  where
-    open ⇒-Reasoning 𝒞
-    open ⊗-Reasoning M
-    ≈ᵢ : fᵢ U.∘ U.id ⊗₁ ((λ⇒ U.∘ discard ⊗₁ U.id) U.∘ fₒ ⊗₁ U.id) U.∘ α⇒ U.∘ copy ⊗₁ U.id U.≈ fᵢ
-    ≈ᵢ = begin
-        fᵢ U.∘ U.id ⊗₁ ((λ⇒ U.∘ discard ⊗₁ U.id) U.∘ fₒ ⊗₁ U.id) U.∘ α⇒ U.∘ copy ⊗₁ U.id  ≈⟨ refl⟩∘⟨ refl⟩⊗⟨ pullʳ merge₁ʳ ⟩∘⟨refl ⟩
-        fᵢ U.∘ U.id ⊗₁ (λ⇒ U.∘ (discard U.∘ fₒ) ⊗₁ U.id) U.∘ α⇒ U.∘ copy ⊗₁ U.id          ≈⟨ refl⟩∘⟨ refl⟩⊗⟨ (refl⟩∘⟨ η⇒ ⟩⊗⟨refl) ⟩∘⟨refl ⟩
-        fᵢ U.∘ U.id ⊗₁ (λ⇒ U.∘ discard ⊗₁ U.id) U.∘ α⇒ U.∘ copy ⊗₁ U.id                   ≈⟨ refl⟩∘⟨ pushˡ split₂ʳ ⟩
-        fᵢ U.∘ U.id ⊗₁ λ⇒ U.∘ U.id ⊗₁ discard ⊗₁ U.id U.∘ α⇒ U.∘ copy ⊗₁ U.id             ≈⟨ refl⟩∘⟨ refl⟩∘⟨ extendʳ assoc-commute-from ⟨
-        fᵢ U.∘ U.id ⊗₁ λ⇒ U.∘ α⇒ U.∘ (U.id ⊗₁ discard) ⊗₁ U.id U.∘ copy ⊗₁ U.id           ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ merge₁ˡ ⟩
-        fᵢ U.∘ U.id ⊗₁ λ⇒ U.∘ α⇒ U.∘ (U.id ⊗₁ discard U.∘ copy) ⊗₁ U.id                   ≈⟨ refl⟩∘⟨ pullˡ triangle ⟩
-        fᵢ U.∘ ρ⇒ ⊗₁ U.id U.∘ (U.id ⊗₁ discard U.∘ copy) ⊗₁ U.id                          ≈⟨ refl⟩∘⟨ merge₁ʳ ⟩
-        fᵢ U.∘ (ρ⇒ U.∘ U.id ⊗₁ discard U.∘ copy) ⊗₁ U.id                                  ≈⟨ refl⟩∘⟨ (refl⟩∘⟨ IsMonoid.identityʳ comonoid) ⟩⊗⟨refl ⟨
-        fᵢ U.∘ (ρ⇒ U.∘ ρ⇐) ⊗₁ U.id                                                        ≈⟨ refl⟩∘⟨ unitorʳ.isoʳ ⟩⊗⟨refl  ⟩
-        fᵢ U.∘ U.id ⊗₁ U.id                                                               ≈⟨ elimʳ ⊗.identity ⟩
-        fᵢ                                                                                ∎
-
-identityʳ : {A B : Box} {f : WiringDiagram A B} → (f ∘ id) ≈ f
-identityʳ {Aᵢ □ Aₒ} {Bᵢ □ Bₒ} {fᵢ ⧈ fₒ} = ≈ᵢ ⌸ U.identityʳ
-  where
-    open ⇒-Reasoning 𝒞
-    open ⊗-Reasoning M
-    ≈ᵢ : (λ⇒ U.∘ discard ⊗₁ U.id) U.∘ U.id ⊗₁ (fᵢ U.∘ U.id ⊗₁ U.id) U.∘ α⇒ U.∘ copy ⊗₁ U.id U.≈ fᵢ
-    ≈ᵢ = begin
-        (λ⇒ U.∘ discard ⊗₁ U.id) U.∘ U.id ⊗₁ (fᵢ U.∘ U.id ⊗₁ U.id) U.∘ α⇒ U.∘ copy ⊗₁ U.id  ≈⟨ refl⟩∘⟨ refl⟩⊗⟨ elimʳ ⊗.identity ⟩∘⟨refl ⟩
-        (λ⇒ U.∘ discard ⊗₁ U.id) U.∘ U.id ⊗₁ fᵢ U.∘ α⇒ U.∘ copy ⊗₁ U.id                     ≈⟨ pullˡ (pullʳ (U.Equiv.sym serialize₁₂)) ⟩
-        (λ⇒ U.∘ discard ⊗₁ fᵢ) U.∘ α⇒ U.∘ copy ⊗₁ U.id                                      ≈⟨ pullʳ (pushˡ serialize₂₁) ⟩
-        λ⇒ U.∘ U.id ⊗₁ fᵢ U.∘ discard ⊗₁ U.id U.∘ α⇒ U.∘ copy ⊗₁ U.id                       ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩⊗⟨ ⊗.identity ⟩∘⟨refl ⟨
-        λ⇒ U.∘ U.id ⊗₁ fᵢ U.∘ discard ⊗₁ U.id ⊗₁ U.id U.∘ α⇒ U.∘ copy ⊗₁ U.id               ≈⟨ refl⟩∘⟨ refl⟩∘⟨ extendʳ assoc-commute-from ⟨
-        λ⇒ U.∘ U.id ⊗₁ fᵢ U.∘ α⇒ U.∘ (discard ⊗₁ U.id) ⊗₁ U.id U.∘ copy ⊗₁ U.id             ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ merge₁ʳ ⟩
-        λ⇒ U.∘ U.id ⊗₁ fᵢ U.∘ α⇒ U.∘ (discard ⊗₁ U.id U.∘ copy) ⊗₁ U.id                     ≈⟨ extendʳ unitorˡ-commute-from ⟩
-        fᵢ U.∘ λ⇒ U.∘ α⇒ U.∘ (discard ⊗₁ U.id U.∘ copy) ⊗₁ U.id                             ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ IsMonoid.identityˡ comonoid ⟩⊗⟨refl ⟨
-        fᵢ U.∘ λ⇒ U.∘ α⇒ U.∘ λ⇐ ⊗₁ U.id                                                     ≈⟨ refl⟩∘⟨ pullˡ coherence₁ ⟩
-        fᵢ U.∘ λ⇒ ⊗₁ U.id U.∘ λ⇐ ⊗₁ U.id                                                    ≈⟨ refl⟩∘⟨ merge₁ʳ ⟩
-        fᵢ U.∘ (λ⇒ U.∘ λ⇐) ⊗₁ U.id                                                          ≈⟨ refl⟩∘⟨ unitorˡ.isoʳ ⟩⊗⟨refl ⟩
-        fᵢ U.∘ U.id ⊗₁ U.id                                                                 ≈⟨ elimʳ ⊗.identity ⟩
-        fᵢ                                                                                  ∎
-
-WD : Category o ℓ e
-WD = categoryHelper record
-    { Obj = Box
-    ; _⇒_ = WiringDiagram
-    ; _≈_ = _≈_
-    ; id = id
-    ; _∘_ = _∘_
-    ; assoc = assoc
-    ; identityˡ = identityˡ
-    ; identityʳ = identityʳ
-    ; equiv = ≈-isEquiv
-    ; ∘-resp-≈ = ∘-resp-≈
-    }