Add braiding to wiring diagram monoidal structure

2 files changed, 375 insertions, 160 deletions

diff --git a/Data/WiringDiagram/Monoidal/Braided.agda b/Data/WiringDiagram/Monoidal/Braided.agda
new file mode 100644
index 0000000..7b28d85
--- /dev/null
+++ b/Data/WiringDiagram/Monoidal/Braided.agda
@@ -0,0 +1,182 @@
+{-# 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.Braided
+    {o ℓ e : Level}
+    {𝒞 : Category o ℓ e}
+    (S : SemiadditiveDagger 𝒞)
+  where
+
+import Categories.Morphism.Reasoning 𝒞 as ⇒-Reasoning
+import Data.WiringDiagram.Core as WD
+
+open import Categories.Category.Monoidal using (Monoidal)
+open import Categories.Category.Monoidal.Braided using (Braided)
+open import Categories.Category.Monoidal.Braided.Properties using (hexagon₁-inv; hexagon₂-inv)
+open import Categories.Category.Monoidal.Symmetric using (module Symmetric)
+open import Categories.Functor.Bifunctor using (flip-bifunctor)
+open import Categories.NaturalTransformation.NaturalIsomorphism using (_≃_; niHelper)
+open import Data.Product using (uncurry; _,_)
+open import Data.WiringDiagram.Monoidal.Core S
+  using (_⊞_; _⊞₁_; σ₂₃; associator⇒; associator⇐; DWD-Monoidal; BWD-Monoidal)
+  renaming (module Directed to D; module Balanced to B)
+open import Function using (flip)
+
+open Category 𝒞
+open SemiadditiveDagger S
+open Symmetric symmetric using (braided; hexagon₁; hexagon₂)
+open WD S using (Box; WiringDiagram; _□_; _⧈_; _≈-⧈_; _⌸_; id-⧈; _⌻_; ≈-sym)
+
+open HomReasoning
+open ⇒-Reasoning
+open Equiv
+
+σ₂₃-⟨⟩
+    : {X A B C D : Obj}
+      {f : X ⇒ A}
+      {g : X ⇒ B}
+      {h : X ⇒ C}
+      {i : X ⇒ D}
+    → σ₂₃ ∘ ⟨ ⟨ f , g ⟩ , ⟨ h , i ⟩ ⟩ ≈ ⟨ ⟨ f , h ⟩ , ⟨ g , i ⟩ ⟩
+σ₂₃-⟨⟩ {f = f} {g} {h} {i} = begin
+    σ₂₃ ∘ ⟨ ⟨ f , g ⟩ , ⟨ h , i ⟩ ⟩                                                 ≈⟨ ⟨⟩∘ ⟩
+    ⟨ π₁ ×₁ π₁ ∘ ⟨ ⟨ f , g ⟩ , ⟨ h , i ⟩ ⟩ , π₂ ×₁ π₂ ∘ ⟨ ⟨ f , g ⟩ , ⟨ h , i ⟩ ⟩ ⟩ ≈⟨ ⟨⟩-cong₂ ×₁∘⟨⟩ ×₁∘⟨⟩ ⟩
+    ⟨ ⟨ π₁ ∘ ⟨ f , g ⟩ , π₁ ∘ ⟨ h , i ⟩ ⟩ , ⟨ π₂ ∘ ⟨ f , g ⟩ , π₂ ∘ ⟨ h , i ⟩ ⟩ ⟩   ≈⟨ ⟨⟩-cong₂ (⟨⟩-cong₂ project₁ project₁) (⟨⟩-cong₂ project₂ project₂) ⟩
+    ⟨ ⟨ f , h ⟩ , ⟨ g , i ⟩ ⟩                                                       ∎
+
+swap-⧈ : (X Y : Box) → WiringDiagram (X ⊞ Y) (Y ⊞ X)
+swap-⧈ X Y = swap ∘ π₂ ⧈ swap
+
+swap-commute
+    : {X X′ Y Y′ : Box}
+      (f : WiringDiagram X X′)
+      (g : WiringDiagram Y Y′)
+    → swap-⧈ X′ Y′ ⌻ f ⊞₁ g ≈-⧈ g ⊞₁ f ⌻ swap-⧈ X Y
+swap-commute (fᵢ ⧈ fₒ) (gᵢ ⧈ gₒ) = eqᵢ ⌸ swap∘×₁  
+  where
+    eqᵢ : (fᵢ ×₁ gᵢ ∘ σ₂₃) ∘ ⟨ π₁ , (swap ∘ π₂) ∘ (fₒ ×₁ gₒ) ×₁ id ⟩ ≈ (swap ∘ π₂) ∘ ⟨ π₁ , (gᵢ ×₁ fᵢ ∘ σ₂₃) ∘ swap ×₁ id ⟩
+    eqᵢ = begin
+        (fᵢ ×₁ gᵢ ∘ σ₂₃) ∘ ⟨ π₁ , (swap ∘ π₂) ∘ (fₒ ×₁ gₒ) ×₁ id ⟩  ≈⟨ refl⟩∘⟨ ⟨⟩-congˡ (pullʳ π₂∘first) ⟩
+        (fᵢ ×₁ gᵢ ∘ σ₂₃) ∘ ⟨ π₁ , swap ∘ π₂ ⟩                       ≈⟨ pullʳ ⟨⟩∘ ⟩
+        fᵢ ×₁ gᵢ ∘ ⟨ π₁ ×₁ π₁ ∘ _ , π₂ ×₁ π₂ ∘ ⟨ π₁ , swap ∘ π₂ ⟩ ⟩ ≈⟨ refl⟩∘⟨ ⟨⟩-cong₂ ×₁∘⟨⟩ ×₁∘⟨⟩ ⟩
+        fᵢ ×₁ gᵢ ∘ ⟨ ⟨ _ , _ ⟩ , ⟨ π₂ ∘ π₁ , π₂ ∘ swap ∘ π₂ ⟩ ⟩     ≈⟨ refl⟩∘⟨ ⟨⟩-cong₂ (⟨⟩-congˡ (pullˡ project₁)) (⟨⟩-congˡ (pullˡ project₂)) ⟩
+        fᵢ ×₁ gᵢ ∘ ⟨ π₁ ×₁ π₂ , π₂ ×₁ π₁ ⟩                          ≈⟨ refl⟩∘⟨ swap∘⟨⟩ ⟨
+        fᵢ ×₁ gᵢ ∘ swap ∘ ⟨ π₂ ×₁ π₁ , π₁ ×₁ π₂ ⟩                   ≈⟨ refl⟩∘⟨ pushʳ (sym σ₂₃-⟨⟩) ⟩
+        fᵢ ×₁ gᵢ ∘ (swap ∘ σ₂₃) ∘ ⟨ _ , ⟨ π₁ ∘ π₂ , π₂ ∘ π₂ ⟩ ⟩     ≈⟨ refl⟩∘⟨ refl⟩∘⟨ ⟨⟩-cong₂ ⟨⟩∘ ⟨⟩∘ ⟨
+        fᵢ ×₁ gᵢ ∘ (swap ∘ σ₂₃) ∘ ⟨ _ ∘ π₁ , ⟨ π₁ , π₂ ⟩ ∘ π₂ ⟩     ≈⟨ refl⟩∘⟨ refl⟩∘⟨ ⟨⟩-congˡ (η ⟩∘⟨refl) ⟩
+        fᵢ ×₁ gᵢ ∘ (swap ∘ σ₂₃) ∘ swap ×₁ id                        ≈⟨ extendʳ (extendʳ swap∘×₁) ⟨
+        swap ∘ (gᵢ ×₁ fᵢ ∘ σ₂₃) ∘ swap ×₁ id                        ≈⟨ pushʳ (sym project₂) ⟩
+        (swap ∘ π₂) ∘ ⟨ π₁ , (gᵢ ×₁ fᵢ ∘ σ₂₃) ∘ swap ×₁ id ⟩        ∎
+
+swap∘swap-⧈
+    : {X Y : Box}
+    → swap-⧈ Y X ⌻ swap-⧈ X Y ≈-⧈ id-⧈
+swap∘swap-⧈ = eqᵢ ⌸ swap∘swap
+  where
+    eqᵢ : (swap ∘ π₂) ∘ ⟨ π₁ , (swap ∘ π₂) ∘ swap ×₁ id ⟩ ≈ π₂
+    eqᵢ = begin
+        (swap ∘ π₂) ∘ ⟨ π₁ , (swap ∘ π₂) ∘ swap ×₁ id ⟩ ≈⟨ pullʳ project₂ ⟩
+        swap ∘ (swap ∘ π₂) ∘ swap ×₁ id                 ≈⟨ refl⟩∘⟨ pullʳ π₂∘first ⟩
+        swap ∘ swap ∘ π₂                                ≈⟨ cancelˡ swap∘swap ⟩
+        π₂                                              ∎
+
+hex₁
+    : {X Y Z : Box}
+    → id-⧈ ⊞₁ swap-⧈ X Z ⌻ associator⇒ ⌻ swap-⧈ X Y ⊞₁ id-⧈ {Z}
+    ≈-⧈ associator⇒ ⌻ swap-⧈ X (Y ⊞ Z) ⌻ associator⇒
+hex₁ = eqᵢ ⌸ hexagon₁
+  where
+    eqᵢ : (((swap ∘ π₂) ×₁ π₂ ∘ σ₂₃) ∘ ⟨ π₁ , (assocʳ ∘ π₂) ∘ (swap ×₁ id) ×₁ id ⟩) ∘ ⟨ π₁ , (π₂ ×₁ (swap ∘ π₂) ∘ σ₂₃) ∘ (assocˡ ∘ swap ×₁ id) ×₁ id ⟩
+        ≈ ((assocʳ ∘ π₂) ∘ ⟨ π₁ , (swap ∘ π₂) ∘ assocˡ ×₁ id ⟩) ∘ ⟨ π₁ , (assocʳ ∘ π₂) ∘ (swap ∘ assocˡ) ×₁ id ⟩
+    eqᵢ = begin
+        (((swap ∘ π₂) ×₁ π₂ ∘ σ₂₃) ∘ ⟨ π₁ , (assocʳ ∘ π₂) ∘ (swap ×₁ id) ×₁ id ⟩) ∘ _ ≈⟨ (refl⟩∘⟨ ⟨⟩-congˡ (pullʳ π₂∘first)) ⟩∘⟨refl ⟩
+        (((swap ∘ π₂) ×₁ π₂ ∘ ⟨ π₁ ×₁ π₁ , π₂ ×₁ π₂ ⟩) ∘ ⟨ π₁ , assocʳ ∘ π₂ ⟩) ∘ _    ≈⟨ ×₁∘⟨⟩ ⟩∘⟨refl ⟩∘⟨refl ⟩
+        ((⟨ (swap ∘ π₂) ∘ π₁ ×₁ π₁ , π₂ ∘ π₂ ×₁ π₂ ⟩) ∘ ⟨ π₁ , assocʳ ∘ π₂ ⟩) ∘ _     ≈⟨ ⟨⟩-cong₂ (extendˡ π₂∘×₁) π₂∘×₁ ⟩∘⟨refl ⟩∘⟨refl ⟩
+        ((⟨ (swap ∘ π₁) ∘ π₂ , π₂ ∘ π₂ ⟩) ∘ ⟨ π₁ , assocʳ ∘ π₂ ⟩) ∘ _                 ≈⟨ ⟨⟩∘ ⟩∘⟨refl ⟩∘⟨refl ⟨
+        ((⟨ swap ∘ π₁ , π₂ ⟩ ∘ π₂) ∘ ⟨ π₁ , assocʳ ∘ π₂ ⟩) ∘ _                        ≈⟨ pullʳ project₂ ⟩∘⟨refl ⟩
+        (⟨ swap ∘ π₁ , π₂ ⟩ ∘ assocʳ ∘ π₂) ∘ _                                        ≈⟨ pullʳ (pullʳ project₂) ⟩
+        ⟨ swap ∘ π₁ , π₂ ⟩ ∘ assocʳ ∘ (π₂ ×₁ (swap ∘ π₂) ∘ σ₂₃) ∘ _ ×₁ id             ≈⟨ refl⟩∘⟨ refl⟩∘⟨ ×₁∘⟨⟩ ⟩∘⟨refl ⟩
+        ⟨ _ ∘ π₁ , π₂ ⟩ ∘ _ ∘ ⟨ π₂ ∘ π₁ ×₁ π₁ , (swap ∘ π₂) ∘ π₂ ×₁ π₂ ⟩ ∘ _ ×₁ id    ≈⟨ refl⟩∘⟨ refl⟩∘⟨ ⟨⟩-cong₂ π₂∘×₁ (extendˡ π₂∘×₁) ⟩∘⟨refl ⟩
+        ⟨ swap ∘ π₁ , π₂ ⟩ ∘ assocʳ ∘ ⟨ π₁ ∘ π₂ , (swap ∘ π₂) ∘ π₂ ⟩ ∘ _ ×₁ id        ≈⟨ refl⟩∘⟨ refl⟩∘⟨ pushˡ (sym ⟨⟩∘) ⟩
+        ⟨ swap ∘ π₁ , π₂ ⟩ ∘ assocʳ ∘ ⟨ π₁ , swap ∘ π₂ ⟩ ∘ π₂ ∘ _ ×₁ id               ≈⟨ pushʳ (refl⟩∘⟨ refl⟩∘⟨ π₂∘first) ⟩
+        (⟨ swap ∘ π₁ , π₂ ⟩ ∘ assocʳ) ∘ ⟨ π₁ , swap ∘ π₂ ⟩ ∘ π₂                       ≈⟨ (⟨⟩-congˡ identityˡ ⟩∘⟨refl) ⟩∘⟨ ⟨⟩-congʳ identityˡ ⟩∘⟨refl ⟨
+        (swap ×₁ id ∘ assocʳ) ∘ id ×₁ swap ∘ π₂                                       ≈⟨ extendʳ (hexagon₁-inv braided) ⟩
+        (assocʳ ∘ swap) ∘ assocʳ ∘ π₂                                                 ≈⟨ refl⟩∘⟨ pushʳ (sym π₂∘first) ⟩
+        (assocʳ ∘ swap) ∘ (assocʳ ∘ π₂) ∘ _ ×₁ id                                     ≈⟨ pushʳ (sym project₂) ⟩
+        ((assocʳ ∘ swap) ∘ π₂) ∘ ⟨ π₁ , (assocʳ ∘ π₂) ∘ _ ×₁ id ⟩                     ≈⟨ pullʳ (pushʳ (sym π₂∘first)) ⟩∘⟨refl ⟩
+        (assocʳ ∘ (swap ∘ π₂) ∘ assocˡ ×₁ id) ∘ ⟨ π₁ , (assocʳ ∘ π₂) ∘ _ ×₁ id ⟩      ≈⟨ pushʳ (sym project₂) ⟩∘⟨refl ⟩
+        ((assocʳ ∘ π₂) ∘ ⟨ π₁ , (swap ∘ π₂) ∘ assocˡ ×₁ id ⟩) ∘ ⟨ π₁ , _ ∘ _ ×₁ id ⟩  ∎
+
+hex₂
+    : {X Y Z : Box}
+    → (swap-⧈ X Z ⊞₁ id-⧈ ⌻ associator⇐) ⌻ id-⧈ {X} ⊞₁ swap-⧈ Y Z
+    ≈-⧈ (associator⇐ ⌻ swap-⧈ (X ⊞ Y) Z) ⌻ associator⇐
+hex₂ = eqᵢ ⌸ hexagon₂
+  where
+    eqᵢ : (π₂ ×₁ (swap ∘ π₂) ∘ σ₂₃) ∘ ⟨ π₁ , ((assocˡ ∘ π₂) ∘ ⟨ π₁ , ((swap ∘ π₂) ×₁ π₂ ∘ σ₂₃) ∘ assocʳ ×₁ id ⟩) ∘ (id ×₁ swap) ×₁ id ⟩
+        ≈ (assocˡ ∘ π₂) ∘ ⟨ π₁ , ((swap ∘ π₂) ∘ ⟨ π₁ , (assocˡ ∘ π₂) ∘ swap ×₁ id ⟩) ∘ assocʳ ×₁ id ⟩
+    eqᵢ = begin
+        (π₂ ×₁ (swap ∘ π₂) ∘ σ₂₃) ∘ ⟨ π₁ , ((_ ∘ π₂) ∘ ⟨ π₁ , _ ∘ _ ×₁ id ⟩) ∘ _ ×₁ id ⟩  ≈⟨ refl⟩∘⟨ ⟨⟩-congˡ (pullʳ project₂ ⟩∘⟨refl) ⟩
+        (π₂ ×₁ _ ∘ σ₂₃) ∘ ⟨ π₁ , (_ ∘ ((swap ∘ π₂) ×₁ π₂ ∘ σ₂₃) ∘ _ ×₁ id) ∘ _ ×₁ id ⟩    ≈⟨ refl⟩∘⟨ ⟨⟩-congˡ ((refl⟩∘⟨ ×₁∘⟨⟩ ⟩∘⟨refl) ⟩∘⟨refl) ⟩
+        _ ∘ ⟨ π₁ , (_ ∘ ⟨ (swap ∘ π₂) ∘ π₁ ×₁ π₁ , π₂ ∘ π₂ ×₁ π₂ ⟩ ∘ _ ×₁ id) ∘ _ ×₁ id ⟩ ≈⟨ refl⟩∘⟨ ⟨⟩-congˡ ((refl⟩∘⟨ ⟨⟩-cong₂ (extendˡ π₂∘×₁) π₂∘×₁ ⟩∘⟨refl) ⟩∘⟨refl) ⟩
+        _ ∘ ⟨ π₁ , (_ ∘ ⟨ (swap ∘ π₁) ∘ π₂ , π₂ ∘ π₂ ⟩ ∘ assocʳ ×₁ id) ∘ _ ×₁ id ⟩        ≈⟨ refl⟩∘⟨ ⟨⟩-congˡ ((refl⟩∘⟨ pushˡ (sym ⟨⟩∘)) ⟩∘⟨refl) ⟩
+        (π₂ ×₁ _ ∘ σ₂₃) ∘ ⟨ π₁ , (_ ∘ ⟨ swap ∘ π₁ , π₂ ⟩ ∘ π₂ ∘ assocʳ ×₁ id) ∘ _ ×₁ id ⟩ ≈⟨ refl⟩∘⟨ ⟨⟩-congˡ (pushˡ (refl⟩∘⟨ refl⟩∘⟨ π₂∘first)) ⟩
+        (π₂ ×₁ _ ∘ σ₂₃) ∘ ⟨ π₁ , _ ∘ (⟨ swap ∘ π₁ , π₂ ⟩ ∘ π₂) ∘ _ ×₁ id ⟩                ≈⟨ refl⟩∘⟨ ⟨⟩-congˡ (refl⟩∘⟨ pullʳ π₂∘first) ⟩
+        (π₂ ×₁ (swap ∘ π₂) ∘ σ₂₃) ∘ ⟨ π₁ , _ ∘ ⟨ _ ∘ π₁ , π₂ ⟩ ∘ π₂ ⟩                     ≈⟨ ×₁∘⟨⟩ ⟩∘⟨refl ⟩
+        ⟨ π₂ ∘ π₁ ×₁ π₁ , (swap ∘ π₂) ∘ π₂ ×₁ π₂ ⟩ ∘ ⟨ π₁ , _ ∘ ⟨ swap ∘ π₁ , π₂ ⟩ ∘ π₂ ⟩ ≈⟨ ⟨⟩-cong₂ π₂∘×₁ (extendˡ π₂∘×₁) ⟩∘⟨refl ⟩
+        ⟨ π₁ ∘ π₂ , (swap ∘ π₂) ∘ π₂ ⟩ ∘ ⟨ π₁ , assocˡ ∘ ⟨ swap ∘ π₁ , π₂ ⟩ ∘ π₂ ⟩        ≈⟨ pushˡ (sym ⟨⟩∘) ⟩
+        ⟨ π₁ , swap ∘ π₂ ⟩ ∘ π₂ ∘ ⟨ π₁ , assocˡ ∘ ⟨ swap ∘ π₁ , π₂ ⟩ ∘ π₂ ⟩               ≈⟨ refl⟩∘⟨ project₂ ⟩
+        ⟨ π₁ , swap ∘ π₂ ⟩ ∘ assocˡ ∘ ⟨ swap ∘ π₁ , π₂ ⟩ ∘ π₂                             ≈⟨ ⟨⟩-congʳ (sym identityˡ) ⟩∘⟨ pushʳ (⟨⟩-congˡ (sym identityˡ) ⟩∘⟨refl) ⟩
+        id ×₁ swap ∘ (assocˡ ∘ swap ×₁ id) ∘ π₂                                           ≈⟨ extendʳ (hexagon₂-inv braided) ⟩
+        assocˡ ∘ (swap ∘ assocˡ) ∘ π₂                                                     ≈⟨ refl⟩∘⟨ pullʳ (pushʳ (sym π₂∘first)) ⟩
+        assocˡ ∘ swap ∘ (assocˡ ∘ π₂) ∘ assocʳ ×₁ id                                      ≈⟨ refl⟩∘⟨ refl⟩∘⟨ pushʳ (sym π₂∘first) ⟩∘⟨refl ⟩
+        assocˡ ∘ swap ∘ ((assocˡ ∘ π₂) ∘ swap ×₁ id) ∘ assocʳ ×₁ id                       ≈⟨ refl⟩∘⟨ pullˡ (pushʳ (sym project₂)) ⟩
+        assocˡ ∘ ((swap ∘ π₂) ∘ ⟨ π₁ , (assocˡ ∘ π₂) ∘ swap ×₁ id ⟩) ∘ assocʳ ×₁ id       ≈⟨ pushʳ (sym project₂) ⟩
+        (assocˡ ∘ π₂) ∘ ⟨ π₁ , ((_ ∘ π₂) ∘ ⟨ π₁ , (_ ∘ π₂) ∘ swap ×₁ id ⟩) ∘ _ ×₁ id ⟩    ∎
+
+module Directed where
+
+  open D using (-⊞-)
+
+  γ : -⊞- ≃ flip-bifunctor -⊞-
+  γ = niHelper record
+      { η = uncurry swap-⧈
+      ; η⁻¹ = uncurry (flip swap-⧈)
+      ; commute = uncurry swap-commute
+      ; iso = λ (X , Y) → record
+          { isoˡ = swap∘swap-⧈
+          ; isoʳ = swap∘swap-⧈
+          }
+      }
+
+module Balanced where
+
+  open B using (-⊞-)
+
+  γ : -⊞- ≃ flip-bifunctor -⊞-
+  γ = niHelper record
+      { η = λ (X , Y) → swap-⧈ (X □ X) (Y □ Y)
+      ; η⁻¹ = λ (X , Y) → swap-⧈ (Y □ Y) (X □ X)
+      ; commute = uncurry swap-commute
+      ; iso = λ (X , Y) → record
+          { isoˡ = swap∘swap-⧈
+          ; isoʳ = swap∘swap-⧈
+          }
+      }
+
+DWD-Braided : Braided DWD-Monoidal
+DWD-Braided = record
+    { braiding = Directed.γ
+    ; hexagon₁ = hex₁
+    ; hexagon₂ = hex₂
+  }
+
+BWD-Braided : Braided BWD-Monoidal
+BWD-Braided = record
+    { braiding = Balanced.γ
+    ; hexagon₁ = hex₁
+    ; hexagon₂ = hex₂
+  }
diff --git a/Data/WiringDiagram/Monoidal.agda b/Data/WiringDiagram/Monoidal/Core.agda
index 1327b1d..382e188 100644
--- a/Data/WiringDiagram/Monoidal.agda
+++ b/Data/WiringDiagram/Monoidal/Core.agda
@@ -4,77 +4,53 @@ open import Categories.Category using (Category)
 open import Category.Dagger.Semiadditive using (SemiadditiveDagger)
 open import Level using (Level)
 
-module Data.WiringDiagram.Monoidal
+module Data.WiringDiagram.Monoidal.Core
     {o ℓ e : Level}
     {𝒞 : Category o ℓ e}
     (S : SemiadditiveDagger 𝒞)
   where
 
-import Categories.Category.Monoidal.Interchange.Braided as Interchange
-import Categories.Category.Monoidal.Interchange.Symmetric as SymInterchange
 import Categories.Category.Monoidal.Reasoning as ⊗-Reasoning
+import Categories.Morphism as Morphism
 import Categories.Morphism.Reasoning 𝒞 as ⇒-Reasoning
+import Data.WiringDiagram.Balanced as BalancedWD
 import Data.WiringDiagram.Core as WD
-import Data.WiringDiagram.Directed as Directed
+import Data.WiringDiagram.Directed as DirectedWD
 
 open import Categories.Category.Monoidal using (Monoidal)
-open import Categories.Category.Monoidal.Interchange using (HasInterchange)
-open import Categories.Object.Initial using (Initial; IsInitial)
 open import Categories.Category.Monoidal.Symmetric using (module Symmetric)
-open import Categories.NaturalTransformation.NaturalIsomorphism using (NaturalIsomorphism)
-open import Categories.Category.Monoidal.Symmetric.Properties using () renaming (module Shorthands to SymShorthands)
-open import Categories.Category.Monoidal.Utilities using (module Shorthands; pentagon-inv)
+open import Categories.Category.Monoidal.Utilities using (pentagon-inv)
 open import Categories.Functor.Bifunctor using (Bifunctor)
+open import Categories.Object.Initial using (Initial; IsInitial)
 open import Data.Product using (_,_; uncurry′)
 
-open WD S using (Box; WiringDiagram; _□_; _⧈_; _≈-⧈_; _⌸_; id-⧈; _⌻_; ≈-sym)
-open Directed S using (DWD)
+open SemiadditiveDagger S
 
+open BalancedWD S using (BWD)
 open Category 𝒞
-module S = SemiadditiveDagger S
-open S
-open Shorthands monoidal
-open SymShorthands symmetric
-
+open DirectedWD S using (DWD)
 open Monoidal monoidal using (triangle; pentagon)
 open Symmetric symmetric using (braided)
-open Interchange braided using (swapInner; swapInner-natural; hasInterchange)
-
-open import Categories.Morphism DWD using (_≅_)
+open WD S using (Box; WiringDiagram; _□_; _⧈_; _≈-⧈_; _⌸_; id-⧈; _⌻_; ≈-sym)
 
 module DWD = Category DWD
 
-𝟘-□ : Box
-𝟘-□ = 𝟘 □ 𝟘
+-- Swap middle two of four
 
-module i⇒ = HasInterchange hasInterchange
+σ₂₃ : {A B C D : Obj} → (A ⊕ B) ⊕ (C ⊕ D) ⇒ (A ⊕ C) ⊕ (B ⊕ D)
+σ₂₃ = ⟨ π₁ ×₁ π₁ , π₂ ×₁ π₂ ⟩
 
-module i≃ = NaturalIsomorphism i⇒.naturalIso
+-- Monoidal unit and initial object
 
-i⇒ = i⇒.swapInner.from
-i⇐ = i⇒.swapInner.to
+𝟘-□ : Box
+𝟘-□ = 𝟘 □ 𝟘
 
-σ₂₃ : {A B C D : Obj} → (A ⊕ B) ⊕ (C ⊕ D) ⇒ (A ⊕ C) ⊕ (B ⊕ D)
-σ₂₃ = ⟨ π₁ ×₁ π₁ , π₂ ×₁ π₂ ⟩
+-- Wiring diagram from the initial box to any box
 
--- Wiring diagram from the zero box to any box
 ¡-⧈ : {A : Box} → WiringDiagram 𝟘-□ A
 ¡-⧈ {A} = ! WD.⧈ ¡
 
-¡-⧈-unique : {A : Box} (f : WiringDiagram 𝟘-□ A) → ¡-⧈ ≈-⧈ f
-¡-⧈-unique (fᵢ ⧈ fₒ) = !-unique fᵢ ⌸ ¡-unique fₒ
-
-𝟘-□-isInitial : IsInitial DWD 𝟘-□
-𝟘-□-isInitial = record
-    { ¡ = ¡-⧈
-    ; ¡-unique = ¡-⧈-unique
-    }
-
-initial-□ : Initial DWD
-initial-□ = record
-    { ⊥ = 𝟘-□
-    ; ⊥-is-initial = 𝟘-□-isInitial
-    }
+-- Monoidal products of boxes and wiring diagrams
 
 _⊞_ : Box → Box → Box
 (Aᵢ □ Aₒ) ⊞ (Bᵢ □ Bₒ) = Aᵢ ⊕ Bᵢ □ Aₒ ⊕ Bₒ
@@ -84,13 +60,48 @@ _⊞₁_
       (f : WiringDiagram A B)
       (g : WiringDiagram C D)
     → WiringDiagram (A ⊞ C) (B ⊞ D)
-_⊞₁_ {A} {B} {C} {D} (fᵢ ⧈ fₒ) (gᵢ ⧈ gₒ) = fᵢ ×₁ gᵢ ∘ σ₂₃ ⧈ fₒ ×₁ gₒ
+(fᵢ ⧈ fₒ) ⊞₁ (gᵢ ⧈ gₒ) = fᵢ ×₁ gᵢ ∘ σ₂₃ ⧈ fₒ ×₁ gₒ
+
+infixr 10 _⊞_ _⊞₁_
+
+-- Left and right unitor wiring diagrams
+
+unitorˡ⇒ : {X : Box} → WiringDiagram (𝟘-□ ⊞ X) X
+unitorˡ⇒ = i₂ ∘ π₂ ⧈ π₂
+
+unitorˡ⇐ : {X : Box} → WiringDiagram X (𝟘-□ ⊞ X)
+unitorˡ⇐ = π₂ ∘ π₂ ⧈ i₂
+
+unitorʳ⇒ : {X : Box} → WiringDiagram (X ⊞ 𝟘-□) X
+unitorʳ⇒ = i₁ ∘ π₂ ⧈ π₁
+
+unitorʳ⇐ : {X : Box} → WiringDiagram X (X ⊞ 𝟘-□)
+unitorʳ⇐ = π₁ ∘ π₂ ⧈ i₁
+
+-- Associator wiring diagrams
+
+associator⇒
+    : {X Y Z : Box}
+    → WiringDiagram ((X ⊞ Y) ⊞ Z) (X ⊞ (Y ⊞ Z))
+associator⇒ = assocʳ ∘ π₂ ⧈ assocˡ
+
+associator⇐
+    : {X Y Z : Box}
+    → WiringDiagram (X ⊞ (Y ⊞ Z)) ((X ⊞ Y) ⊞ Z)
+associator⇐ = assocˡ ∘ π₂ ⧈ assocʳ
+
+-- Properties
+
+open HomReasoning
+open ⇒-Reasoning
+open Equiv
+
+¡-⧈-unique : {A : Box} (f : WiringDiagram 𝟘-□ A) → ¡-⧈ ≈-⧈ f
+¡-⧈-unique (fᵢ ⧈ fₒ) = !-unique fᵢ ⌸ ¡-unique fₒ
 
 ⊞-identity : {A B : Box} → id-⧈ {A} ⊞₁ id-⧈ {B} ≈-⧈ id-⧈
-⊞-identity {A} {B} = eqᵢ ⌸ id×₁id
+⊞-identity = eqᵢ ⌸ id×₁id
   where
-    open HomReasoning
-    open ⇒-Reasoning
     eqᵢ : π₂ ×₁ π₂ ∘ σ₂₃ ≈ π₂
     eqᵢ = begin
         π₂ ×₁ π₂ ∘ σ₂₃                    ≈⟨ ×₁∘⟨⟩ ⟩
@@ -111,27 +122,21 @@ _⊞₁_ {A} {B} {C} {D} (fᵢ ⧈ fₒ) (gᵢ ⧈ gₒ) = fᵢ ×₁ gᵢ ∘ �
     ⟨ ⟨ π₁ ∘ π₁ ×₁ π₁ , id ∘ π₁ ×₁ π₁ ⟩ , ⟨ π₁ ∘ π₂ ×₁ π₂ , id ∘ π₂ ×₁ π₂ ⟩ ⟩                     ≈⟨ ⟨⟩-cong₂ ⟨⟩∘ ⟨⟩∘ ⟨
     ⟨ ⟨ π₁ , id ⟩ ∘ π₁ ×₁ π₁ , ⟨ π₁ , id ⟩ ∘ π₂ ×₁ π₂ ⟩                                           ≈⟨ ×₁∘⟨⟩ ⟨
     ⟨ π₁ , id ⟩ ×₁ ⟨ π₁ , id ⟩ ∘ ⟨ π₁ ×₁ π₁ , π₂ ×₁ π₂ ⟩                                          ∎
-  where
-    open HomReasoning
 
-σ₂₃-comm
+σ₂₃-×₁
     : {A A′ B B′ C C′ D D′ : Obj}
       {f : A ⇒ A′}
       {g : B ⇒ B′}
       {h : C ⇒ C′}
       {i : D ⇒ D′}
     → (f ×₁ g) ×₁ (h ×₁ i) ∘ σ₂₃ ≈ σ₂₃ ∘ (f ×₁ h) ×₁ (g ×₁ i)
-σ₂₃-comm {f = f} {g} {h} {i} = begin
+σ₂₃-×₁ {f = f} {g} {h} {i} = begin
     (f ×₁ g) ×₁ (h ×₁ i) ∘ ⟨ π₁ ×₁ π₁ , π₂ ×₁ π₂ ⟩                        ≈⟨ ×₁∘⟨⟩ ⟩
     ⟨ f ×₁ g ∘ π₁ ×₁ π₁ , h ×₁ i ∘ π₂ ×₁ π₂ ⟩                             ≈⟨ ⟨⟩-cong₂ ×₁∘×₁ ×₁∘×₁ ⟩
     ⟨ (f ∘ π₁) ×₁ (g ∘ π₁) , (h ∘ π₂) ×₁ (i ∘ π₂) ⟩                       ≈⟨ ⟨⟩-cong₂ (×₁-cong₂ π₁∘×₁ π₁∘×₁) (×₁-cong₂ π₂∘×₁ π₂∘×₁) ⟨
     ⟨ (π₁ ∘ f ×₁ h) ×₁ (π₁ ∘ g ×₁ i) , (π₂ ∘ f ×₁ h) ×₁ (π₂ ∘ g ×₁ i) ⟩   ≈⟨ ⟨⟩-cong₂ ×₁∘×₁ ×₁∘×₁ ⟨
     ⟨ π₁ ×₁ π₁ ∘ (f ×₁ h) ×₁ (g ×₁ i) , π₂ ×₁ π₂ ∘ (f ×₁ h) ×₁ (g ×₁ i) ⟩ ≈⟨ ⟨⟩∘ ⟨
     σ₂₃ ∘ (f ×₁ h) ×₁ (g ×₁ i)                                            ∎
-  where
-    open HomReasoning
-
-infixr 10 _⊞_ _⊞₁_
 
 ⊞-homo
     : {A B C D E F : Box}
@@ -154,13 +159,13 @@ infixr 10 _⊞_ _⊞₁_
         (fᵢ ∘ id ×₁ _) ×₁ (gᵢ ∘ id ×₁ _) ∘ ⟨ π₁ , id ⟩ ×₁ ⟨ π₁ , id ⟩ ∘ σ₂₃             ≈⟨ refl⟩∘⟨ σ₂₃-lemma ⟨
         (fᵢ ∘ id ×₁ _) ×₁ (gᵢ ∘ id ×₁ (iᵢ ∘ gₒ ×₁ id)) ∘ σ₂₃ ∘ ⟨ π₁ , σ₂₃ ⟩             ≈⟨ ×₁-cong₂ (pushʳ (sym second∘second)) (pushʳ (sym second∘second)) ⟩∘⟨refl ⟩
         (_ ∘ id ×₁ (fₒ ×₁ id)) ×₁ (_ ∘ id ×₁ (gₒ ×₁ id)) ∘ σ₂₃ ∘ ⟨ π₁ , σ₂₃ ⟩           ≈⟨ pushˡ (sym ×₁∘×₁) ⟩
-        (fᵢ ∘ id ×₁ hᵢ) ×₁ _ ∘ (id ×₁ (fₒ ×₁ id)) ×₁ (id ×₁ _) ∘ σ₂₃ ∘ ⟨ π₁ , σ₂₃ ⟩     ≈⟨ refl⟩∘⟨ extendʳ σ₂₃-comm ⟩
+        (fᵢ ∘ id ×₁ hᵢ) ×₁ _ ∘ (id ×₁ (fₒ ×₁ id)) ×₁ (id ×₁ _) ∘ σ₂₃ ∘ ⟨ π₁ , σ₂₃ ⟩     ≈⟨ refl⟩∘⟨ extendʳ σ₂₃-×₁ ⟩
         (fᵢ ∘ id ×₁ hᵢ) ×₁ _ ∘ σ₂₃ ∘ (id ×₁ id) ×₁ _ ×₁ (gₒ ×₁ id) ∘ ⟨ π₁ , σ₂₃ ⟩       ≈⟨ refl⟩∘⟨ refl⟩∘⟨ ×₁-congʳ id×₁id ⟩∘⟨refl ⟩
         (fᵢ ∘ id ×₁ hᵢ) ×₁ _ ∘ σ₂₃ ∘ id ×₁ (fₒ ×₁ id) ×₁ (gₒ ×₁ id) ∘ ⟨ π₁ , σ₂₃ ⟩      ≈⟨ refl⟩∘⟨ refl⟩∘⟨ second∘⟨⟩ ⟩
-        (fᵢ ∘ id ×₁ hᵢ) ×₁ _ ∘ σ₂₃ ∘ ⟨ π₁ , (fₒ ×₁ id) ×₁ (gₒ ×₁ id) ∘ σ₂₃ ⟩            ≈⟨ refl⟩∘⟨ refl⟩∘⟨ ⟨⟩-congˡ σ₂₃-comm ⟩
+        (fᵢ ∘ id ×₁ hᵢ) ×₁ _ ∘ σ₂₃ ∘ ⟨ π₁ , (fₒ ×₁ id) ×₁ (gₒ ×₁ id) ∘ σ₂₃ ⟩            ≈⟨ refl⟩∘⟨ refl⟩∘⟨ ⟨⟩-congˡ σ₂₃-×₁ ⟩
         (fᵢ ∘ id ×₁ hᵢ) ×₁ _ ∘ σ₂₃ ∘ ⟨ π₁ , σ₂₃ ∘ (fₒ ×₁ gₒ) ×₁ (id ×₁ id) ⟩            ≈⟨ refl⟩∘⟨ refl⟩∘⟨ ⟨⟩-congˡ (refl⟩∘⟨ ×₁-congˡ id×₁id) ⟩
         (fᵢ ∘ id ×₁ hᵢ) ×₁ _ ∘ σ₂₃ ∘ ⟨ π₁ , σ₂₃ ∘ (fₒ ×₁ gₒ) ×₁ id ⟩                    ≈⟨ pushˡ (sym ×₁∘×₁) ⟩
-        fᵢ ×₁ gᵢ ∘ (id ×₁ hᵢ) ×₁ (id ×₁ iᵢ) ∘ σ₂₃ ∘ ⟨ π₁ , σ₂₃ ∘ (fₒ ×₁ gₒ) ×₁ id ⟩     ≈⟨ pushʳ (extendʳ σ₂₃-comm) ⟩
+        fᵢ ×₁ gᵢ ∘ (id ×₁ hᵢ) ×₁ (id ×₁ iᵢ) ∘ σ₂₃ ∘ ⟨ π₁ , σ₂₃ ∘ (fₒ ×₁ gₒ) ×₁ id ⟩     ≈⟨ pushʳ (extendʳ σ₂₃-×₁) ⟩
         (fᵢ ×₁ gᵢ ∘ σ₂₃) ∘ (id ×₁ id) ×₁ (hᵢ ×₁ iᵢ) ∘ ⟨ π₁ , σ₂₃ ∘ (fₒ ×₁ gₒ) ×₁ id ⟩   ≈⟨ refl⟩∘⟨ ×₁-congʳ id×₁id ⟩∘⟨refl ⟩
         (fᵢ ×₁ gᵢ ∘ σ₂₃) ∘ id ×₁ (hᵢ ×₁ iᵢ) ∘ ⟨ π₁ , σ₂₃ ∘ (fₒ ×₁ gₒ) ×₁ id ⟩           ≈⟨ refl⟩∘⟨ ×₁∘⟨⟩ ⟩
         (fᵢ ×₁ gᵢ ∘ σ₂₃) ∘ ⟨ id ∘ π₁ , hᵢ ×₁ iᵢ ∘ σ₂₃ ∘ (fₒ ×₁ gₒ) ×₁ id ⟩              ≈⟨ refl⟩∘⟨ ⟨⟩-cong₂ identityˡ sym-assoc ⟩
@@ -174,25 +179,6 @@ infixr 10 _⊞_ _⊞₁_
     → h ≈-⧈ i
     → f ⊞₁ h ≈-⧈ g ⊞₁ i
 ⊞-resp-≈-⧈ (fᵢ≈gᵢ ⌸ fₒ≈gₒ) (hᵢ≈iᵢ ⌸ hₒ≈iₒ) = (×₁-cong₂ fᵢ≈gᵢ hᵢ≈iᵢ ⟩∘⟨refl) ⌸ ×₁-cong₂ fₒ≈gₒ hₒ≈iₒ
-  where
-    open HomReasoning
-
--⊞- : Bifunctor DWD DWD DWD
--⊞- = record
-    { F₀ = uncurry′ _⊞_
-    ; F₁ = uncurry′ _⊞₁_
-    ; identity = ⊞-identity
-    ; homomorphism = ⊞-homo
-    ; F-resp-≈ = uncurry′ ⊞-resp-≈-⧈
-    }
-
-open import Data.Product using (_×_)
-
-unitorˡ⇒ : {X : Box} → WiringDiagram (𝟘-□ ⊞ X) X
-unitorˡ⇒ = i₂ ∘ π₂ ⧈ π₂
-
-unitorˡ⇐ : {X : Box} → WiringDiagram X (𝟘-□ ⊞ X)
-unitorˡ⇐ {X} = π₂ ∘ π₂ ⧈ i₂
 
 λ-isoˡ : {X : Box} → unitorˡ⇐ ⌻ unitorˡ⇒ ≈-⧈ DWD.id {𝟘-□ ⊞ X}
 λ-isoˡ = eqᵢ ⌸ i₂∘π₂≈id
@@ -215,8 +201,6 @@ unitorˡ⇐ {X} = π₂ ∘ π₂ ⧈ i₂
 λ-isoʳ : {X : Box} → unitorˡ⇒ ⌻ unitorˡ⇐ ≈-⧈ DWD.id {X}
 λ-isoʳ {X} = eqᵢ ⌸ π₂∘i₂≈id
   where
-    open ⇒-Reasoning
-    open HomReasoning
     eqᵢ : (π₂ ∘ π₂) ∘ ⟨ π₁ , (i₂ ∘ π₂) ∘ i₂ ×₁ id ⟩ ≈ π₂
     eqᵢ = begin
         (π₂ ∘ π₂) ∘ ⟨ π₁ , (i₂ ∘ π₂) ∘ i₂ ×₁ id ⟩ ≈⟨ pullʳ project₂ ⟩
@@ -224,28 +208,9 @@ unitorˡ⇐ {X} = π₂ ∘ π₂ ⧈ i₂
         π₂ ∘ i₂ ∘ π₂                              ≈⟨ cancelˡ π₂∘i₂≈id ⟩
         π₂                                        ∎
 
-unitorˡ : {X : Box} → 𝟘-□ ⊞ X ≅ X
-unitorˡ {X} = record
-    { from = unitorˡ⇒
-    ; to = unitorˡ⇐
-    ; iso = record
-        { isoˡ = λ-isoˡ
-        ; isoʳ = λ-isoʳ
-        }
-    }
-
-unitorʳ⇒ : {X : Box} → WiringDiagram (X ⊞ 𝟘-□) X
-unitorʳ⇒ = i₁ ∘ π₂ ⧈ π₁
-
-unitorʳ⇐ : {X : Box} → WiringDiagram X (X ⊞ 𝟘-□)
-unitorʳ⇐ {X} = π₁ ∘ π₂ ⧈ i₁
-
 ρ-isoˡ : {X : Box} → unitorʳ⇐ ⌻ unitorʳ⇒ ≈-⧈ DWD.id {X ⊞ 𝟘-□}
 ρ-isoˡ = eqᵢ ⌸ i₁∘π₁≈id
   where
-    open ⇒-Reasoning
-    open HomReasoning
-    open Equiv
     i₁∘π₁≈id : {A : Obj} → i₁ {A} {𝟘} ∘ π₁ {A} {𝟘} ≈ id
     i₁∘π₁≈id = begin
         i₁ ∘ π₁             ≈⟨ ⟨⟩-unique (cancelˡ π₁∘i₁≈id) (pullˡ π₂∘i₁≈0) ⟨
@@ -261,8 +226,6 @@ unitorʳ⇐ {X} = π₁ ∘ π₂ ⧈ i₁
 ρ-isoʳ : {X : Box} → unitorʳ⇒ ⌻ unitorʳ⇐ ≈-⧈ DWD.id {X}
 ρ-isoʳ {X} = eqᵢ ⌸ π₁∘i₁≈id
   where
-    open ⇒-Reasoning
-    open HomReasoning
     eqᵢ : (π₁ ∘ π₂) ∘ ⟨ π₁ , (i₁ ∘ π₂) ∘ i₁ ×₁ id ⟩ ≈ π₂
     eqᵢ = begin
         (π₁ ∘ π₂) ∘ ⟨ π₁ , (i₁ ∘ π₂) ∘ i₁ ×₁ id ⟩ ≈⟨ pullʳ project₂ ⟩
@@ -270,25 +233,12 @@ unitorʳ⇐ {X} = π₁ ∘ π₂ ⧈ i₁
         π₁ ∘ i₁ ∘ π₂                              ≈⟨ cancelˡ π₁∘i₁≈id ⟩
         π₂                                        ∎
 
-unitorʳ : {X : Box} → X ⊞ 𝟘-□ ≅ X
-unitorʳ {X} = record
-    { from = unitorʳ⇒
-    ; to = unitorʳ⇐
-    ; iso = record
-        { isoˡ = ρ-isoˡ
-        ; isoʳ = ρ-isoʳ
-        }
-    }
-
 unitorˡ-commute-from
     : {X Y : Box}
       {f : WiringDiagram X Y}
     → unitorˡ⇒ ⌻ id-⧈ ⊞₁ f ≈-⧈ f ⌻ unitorˡ⇒
 unitorˡ-commute-from {X} {Y} {fᵢ ⧈ fₒ} = eqᵢ ⌸ project₂
   where
-    open HomReasoning
-    open ⇒-Reasoning
-    open Equiv
     eqᵢ : (π₂ ×₁ fᵢ ∘ σ₂₃) ∘ ⟨ π₁ , (i₂ ∘ π₂) ∘ (id ×₁ fₒ) ×₁ id ⟩ ≈ (i₂ ∘ π₂) ∘ ⟨ π₁ , fᵢ ∘ π₂ ×₁ id ⟩
     eqᵢ = begin
         (π₂ ×₁ fᵢ ∘ σ₂₃) ∘ ⟨ π₁ , (i₂ ∘ π₂) ∘ (id ×₁ fₒ) ×₁ id ⟩  ≈⟨ refl⟩∘⟨ ⟨⟩-congˡ (pullʳ π₂∘first) ⟩
@@ -311,9 +261,6 @@ unitorˡ-commute-to
     → unitorˡ⇐ ⌻ f ≈-⧈ id-⧈ ⊞₁ f ⌻ unitorˡ⇐
 unitorˡ-commute-to {X} {Y} {fᵢ ⧈ fₒ} = eqᵢ ⌸ eqₒ
   where
-    open HomReasoning
-    open ⇒-Reasoning
-    open Equiv
     eqₒ : i₂ ∘ fₒ ≈ id ×₁ fₒ ∘ i₂
     eqₒ = begin
         i₂ ∘ fₒ       ≈⟨ inject₂ ⟨
@@ -336,9 +283,6 @@ unitorʳ-commute-from
     → unitorʳ⇒ ⌻ f ⊞₁ id-⧈ ≈-⧈ f ⌻ unitorʳ⇒
 unitorʳ-commute-from {X} {Y} {fᵢ ⧈ fₒ} = eqᵢ ⌸ project₁
   where
-    open HomReasoning
-    open ⇒-Reasoning
-    open Equiv
     eqᵢ : (fᵢ ×₁ π₂ ∘ σ₂₃) ∘ ⟨ π₁ , (i₁ ∘ π₂) ∘ (fₒ ×₁ id) ×₁ id ⟩ ≈ (i₁ ∘ π₂) ∘ ⟨ π₁ , fᵢ ∘ π₁ ×₁ id ⟩
     eqᵢ = begin
         (fᵢ ×₁ π₂ ∘ σ₂₃) ∘ ⟨ π₁ , (i₁ ∘ π₂) ∘ (fₒ ×₁ id) ×₁ id ⟩    ≈⟨ refl⟩∘⟨ ⟨⟩-congˡ (pullʳ π₂∘first) ⟩
@@ -360,9 +304,6 @@ unitorʳ-commute-to
     → unitorʳ⇐ ⌻ f ≈-⧈ f ⊞₁ id-⧈ ⌻ unitorʳ⇐
 unitorʳ-commute-to {X} {Y} {fᵢ ⧈ fₒ} = eqᵢ ⌸ eqₒ
   where
-    open HomReasoning
-    open ⇒-Reasoning
-    open Equiv
     eqᵢ : fᵢ ∘ ⟨ π₁ , (π₁ ∘ π₂) ∘ fₒ ×₁ id ⟩ ≈ (π₁ ∘ π₂) ∘ ⟨ π₁ , (fᵢ ×₁ π₂ ∘ σ₂₃) ∘ i₁ ×₁ id ⟩
     eqᵢ = begin
         fᵢ ∘ ⟨ π₁ , (π₁ ∘ π₂) ∘ fₒ ×₁ id ⟩                ≈⟨ refl⟩∘⟨ ⟨⟩-congˡ (pullʳ π₂∘first) ⟩
@@ -380,21 +321,9 @@ unitorʳ-commute-to {X} {Y} {fᵢ ⧈ fₒ} = eqᵢ ⌸ eqₒ
         fₒ +₁ id ∘ i₁ ≈⟨ ×₁-+₁ fₒ id ⟩∘⟨refl ⟨
         fₒ ×₁ id ∘ i₁ ∎
 
-associator⇒
-    : {X Y Z : Box}
-    → WiringDiagram ((X ⊞ Y) ⊞ Z) (X ⊞ (Y ⊞ Z))
-associator⇒ = assocʳ ∘ π₂ ⧈ assocˡ
-
-associator⇐
-    : {X Y Z : Box}
-    → WiringDiagram (X ⊞ (Y ⊞ Z)) ((X ⊞ Y) ⊞ Z)
-associator⇐ = assocˡ ∘ π₂ ⧈ assocʳ
-
 α-isoˡ : {X Y Z : Box} → associator⇐ {X} {Y} {Z} ⌻ associator⇒ ≈-⧈ DWD.id
 α-isoˡ {X} {Y} {Z} = eqᵢ ⌸ assocʳ∘assocˡ
   where
-    open HomReasoning
-    open ⇒-Reasoning
     eqᵢ : (assocʳ ∘ π₂) ∘ ⟨ π₁ , (assocˡ ∘ π₂) ∘ assocˡ ×₁ id ⟩ ≈ π₂
     eqᵢ = begin
         (assocʳ ∘ π₂) ∘ ⟨ π₁ , (assocˡ ∘ π₂) ∘ assocˡ ×₁ id ⟩ ≈⟨ pullʳ project₂ ⟩
@@ -405,8 +334,6 @@ associator⇐ = assocˡ ∘ π₂ ⧈ assocʳ
 α-isoʳ : {X Y Z : Box} → associator⇒ {X} {Y} {Z} ⌻ associator⇐ ≈-⧈ DWD.id
 α-isoʳ {X} {Y} {Z} = eqᵢ ⌸ assocˡ∘assocʳ
   where
-    open HomReasoning
-    open ⇒-Reasoning
     eqᵢ : (assocˡ ∘ π₂) ∘ ⟨ π₁ , (assocʳ ∘ π₂) ∘ assocʳ ×₁ id ⟩ ≈ π₂
     eqᵢ = begin
         (assocˡ ∘ π₂) ∘ ⟨ π₁ , (assocʳ ∘ π₂) ∘ assocʳ ×₁ id ⟩ ≈⟨ pullʳ project₂ ⟩
@@ -414,16 +341,6 @@ associator⇐ = assocˡ ∘ π₂ ⧈ assocʳ
         assocˡ ∘ assocʳ ∘ π₂                                  ≈⟨ cancelˡ assocˡ∘assocʳ ⟩
         π₂                                                    ∎
 
-associator : {X Y Z : Box} → (X ⊞ Y) ⊞ Z ≅ X ⊞ (Y ⊞ Z)
-associator = record
-    { from = associator⇒
-    ; to = associator⇐
-    ; iso = record
-        { isoˡ = α-isoˡ
-        ; isoʳ = α-isoʳ
-        }
-    }
-
 associator-commute-from
     : {X X′ Y Y′ Z Z′ : Box}
       {f : WiringDiagram X X′}
@@ -432,9 +349,6 @@ associator-commute-from
     → f ⊞₁ (g ⊞₁ h) ⌻ associator⇒ ≈-⧈ associator⇒ ⌻ (f ⊞₁ g) ⊞₁ h
 associator-commute-from {X} {X′} {Y} {Y′} {Z} {Z′} {fᵢ ⧈ fₒ} {gᵢ ⧈ gₒ} {hᵢ ⧈ hₒ} = eqᵢ ⌸ eqₒ
   where
-    open HomReasoning
-    open ⇒-Reasoning
-    open Equiv
     lemma : assocʳ ∘ (id ×₁ σ₂₃ ∘ σ₂₃) ∘ assocˡ ×₁ id ≈ σ₂₃ ×₁ id ∘ σ₂₃ ∘ id ×₁ assocʳ
     lemma = begin
         assocʳ ∘ (id ×₁ σ₂₃ ∘ σ₂₃) ∘ assocˡ ×₁ id                                                     ≈⟨ refl⟩∘⟨ second∘⟨⟩ ⟩∘⟨refl ⟩
@@ -484,9 +398,6 @@ associator-commute-to
     → (f ⊞₁ g) ⊞₁ h ⌻ associator⇐ ≈-⧈ associator⇐ ⌻ f ⊞₁ (g ⊞₁ h)
 associator-commute-to {X} {X′} {Y} {Y′} {Z} {Z′} {fᵢ ⧈ fₒ} {gᵢ ⧈ gₒ} {hᵢ ⧈ hₒ} = eqᵢ ⌸ eqₒ
   where
-    open HomReasoning
-    open ⇒-Reasoning
-    open Equiv
     lemma : assocˡ ∘ (σ₂₃ ×₁ id ∘ σ₂₃) ∘ assocʳ ×₁ id ≈ id ×₁ σ₂₃ ∘ σ₂₃ ∘ id ×₁ assocˡ
     lemma = begin
         assocˡ ∘ (σ₂₃ ×₁ id ∘ σ₂₃) ∘ assocʳ ×₁ id                                                     ≈⟨ refl⟩∘⟨ first∘⟨⟩ ⟩∘⟨refl ⟩
@@ -527,8 +438,6 @@ tri : {X Y : Box}
     → id-⧈ {X} ⊞₁ unitorˡ⇒ ⌻ associator⇒ ≈-⧈ unitorʳ⇒ ⊞₁ id-⧈ {Y}
 tri = eqᵢ ⌸ triangle
   where
-    open HomReasoning
-    open ⇒-Reasoning
     eqᵢ : (assocʳ ∘ π₂) ∘ ⟨ π₁ , (π₂ ×₁ (i₂ ∘ π₂) ∘ σ₂₃) ∘ assocˡ ×₁ id ⟩ ≈ (i₁ ∘ π₂) ×₁ π₂ ∘ σ₂₃
     eqᵢ = begin
         (assocʳ ∘ π₂) ∘ ⟨ π₁ , (π₂ ×₁ (i₂ ∘ π₂) ∘ σ₂₃) ∘ assocˡ ×₁ id ⟩   ≈⟨ pullʳ project₂ ⟩
@@ -552,9 +461,6 @@ pent
     ≈-⧈ associator⇒ ⌻ associator⇒
 pent =  eqᵢ ⌸ pentagon
   where
-    open HomReasoning
-    open ⇒-Reasoning
-    open Equiv
     eqᵢ : (((assocʳ ∘ π₂) ×₁ π₂ ∘ σ₂₃) ∘ ⟨ π₁ , (assocʳ ∘ π₂) ∘ (assocˡ ×₁ id) ×₁ id ⟩) ∘ ⟨ π₁ , (π₂ ×₁ (assocʳ ∘ π₂) ∘ σ₂₃) ∘ (assocˡ ∘ assocˡ ×₁ id) ×₁ id ⟩
         ≈ (assocʳ ∘ π₂) ∘ ⟨ π₁ , (assocʳ ∘ π₂) ∘ assocˡ ×₁ id ⟩
     eqᵢ = begin
@@ -573,13 +479,140 @@ pent =  eqᵢ ⌸ pentagon
         assocʳ ∘ (assocʳ ∘ π₂) ∘ assocˡ ×₁ id                                             ≈⟨ pushʳ (sym project₂) ⟩
         (assocʳ ∘ π₂) ∘ ⟨ π₁ , (assocʳ ∘ π₂) ∘ assocˡ ×₁ id ⟩                             ∎
 
+module Directed where
+
+  open Morphism DWD using (_≅_)
+
+  -⊞- : Bifunctor DWD DWD DWD
+  -⊞- = record
+      { F₀ = uncurry′ _⊞_
+      ; F₁ = uncurry′ _⊞₁_
+      ; identity = ⊞-identity
+      ; homomorphism = ⊞-homo
+      ; F-resp-≈ = uncurry′ ⊞-resp-≈-⧈
+      }
+
+  unitorˡ : {X : Box} → 𝟘-□ ⊞ X ≅ X
+  unitorˡ {X} = record
+      { from = unitorˡ⇒
+      ; to = unitorˡ⇐
+      ; iso = record
+          { isoˡ = λ-isoˡ
+          ; isoʳ = λ-isoʳ
+          }
+      }
+
+  unitorʳ : {X : Box} → X ⊞ 𝟘-□ ≅ X
+  unitorʳ {X} = record
+      { from = unitorʳ⇒
+      ; to = unitorʳ⇐
+      ; iso = record
+          { isoˡ = ρ-isoˡ
+          ; isoʳ = ρ-isoʳ
+          }
+      }
+
+  associator : {X Y Z : Box} → (X ⊞ Y) ⊞ Z ≅ X ⊞ (Y ⊞ Z)
+  associator = record
+      { from = associator⇒
+      ; to = associator⇐
+      ; iso = record
+          { isoˡ = α-isoˡ
+          ; isoʳ = α-isoʳ
+          }
+      }
+
+  𝟘-□-isInitial : IsInitial DWD 𝟘-□
+  𝟘-□-isInitial = record
+      { ¡ = ¡-⧈
+      ; ¡-unique = ¡-⧈-unique
+      }
+
+module Balanced where
+
+  open Morphism BWD using (_≅_)
+
+  -⊞- : Bifunctor BWD BWD BWD
+  -⊞- = record
+      { F₀ = uncurry′ _⊕_
+      ; F₁ = uncurry′ _⊞₁_
+      ; identity = ⊞-identity
+      ; homomorphism = ⊞-homo
+      ; F-resp-≈ = uncurry′ ⊞-resp-≈-⧈
+      }
+
+  unitorˡ : {X : Obj} → 𝟘 ⊕ X ≅ X
+  unitorˡ {X} = record
+      { from = unitorˡ⇒
+      ; to = unitorˡ⇐
+      ; iso = record
+          { isoˡ = λ-isoˡ
+          ; isoʳ = λ-isoʳ
+          }
+      }
+
+  unitorʳ : {X : Obj} → X ⊕ 𝟘 ≅ X
+  unitorʳ {X} = record
+      { from = unitorʳ⇒
+      ; to = unitorʳ⇐
+      ; iso = record
+          { isoˡ = ρ-isoˡ
+          ; isoʳ = ρ-isoʳ
+          }
+      }
+
+  associator : {X Y Z : Obj} → (X ⊕ Y) ⊕ Z ≅ X ⊕ (Y ⊕ Z)
+  associator = record
+      { from = associator⇒
+      ; to = associator⇐
+      ; iso = record
+          { isoˡ = α-isoˡ
+          ; isoʳ = α-isoʳ
+          }
+      }
+
+  𝟘-isInitial : IsInitial BWD 𝟘
+  𝟘-isInitial = record
+      { ¡ = ¡-⧈
+      ; ¡-unique = ¡-⧈-unique
+      }
+
+DWD-Initial : Initial DWD
+DWD-Initial = record
+    { ⊥ = 𝟘-□
+    ; ⊥-is-initial = Directed.𝟘-□-isInitial
+    }
+
+BWD-Initial : Initial BWD
+BWD-Initial = record
+    { ⊥ = 𝟘
+    ; ⊥-is-initial = Balanced.𝟘-isInitial
+    }
+
 DWD-Monoidal : Monoidal DWD
 DWD-Monoidal = record
-    { ⊗ = -⊞-
+    { ⊗ = Directed.-⊞-
     ; unit = 𝟘-□
-    ; unitorˡ = unitorˡ
-    ; unitorʳ = unitorʳ
-    ; associator = associator
+    ; unitorˡ = Directed.unitorˡ
+    ; unitorʳ = Directed.unitorʳ
+    ; associator = Directed.associator
+    ; unitorˡ-commute-from = unitorˡ-commute-from
+    ; unitorˡ-commute-to = unitorˡ-commute-to
+    ; unitorʳ-commute-from = unitorʳ-commute-from
+    ; unitorʳ-commute-to = unitorʳ-commute-to
+    ; assoc-commute-from = ≈-sym associator-commute-from
+    ; assoc-commute-to = ≈-sym associator-commute-to
+    ; triangle = tri
+    ; pentagon = pent
+    }
+
+BWD-Monoidal : Monoidal BWD
+BWD-Monoidal = record
+    { ⊗ = Balanced.-⊞-
+    ; unit = 𝟘
+    ; unitorˡ = Balanced.unitorˡ
+    ; unitorʳ = Balanced.unitorʳ
+    ; associator = Balanced.associator
     ; unitorˡ-commute-from = unitorˡ-commute-from
     ; unitorˡ-commute-to = unitorˡ-commute-to
     ; unitorʳ-commute-from = unitorʳ-commute-from