Add braiding to wiring diagram monoidal structure

1 files changed, 0 insertions, 591 deletions

diff --git a/Data/WiringDiagram/Monoidal.agda b/Data/WiringDiagram/Monoidal.agda
deleted file mode 100644
index 1327b1d..0000000
--- a/Data/WiringDiagram/Monoidal.agda
+++ /dev/null
@@ -1,591 +0,0 @@
-{-# 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
-    {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.Reasoning 𝒞 as ⇒-Reasoning
-import Data.WiringDiagram.Core as WD
-import Data.WiringDiagram.Directed as Directed
-
-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.Functor.Bifunctor using (Bifunctor)
-open import Data.Product using (_,_; uncurry′)
-
-open WD S using (Box; WiringDiagram; _□_; _⧈_; _≈-⧈_; _⌸_; id-⧈; _⌻_; ≈-sym)
-open Directed S using (DWD)
-
-open Category 𝒞
-module S = SemiadditiveDagger S
-open S
-open Shorthands monoidal
-open SymShorthands symmetric
-
-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 (_≅_)
-
-module DWD = Category DWD
-
-𝟘-□ : Box
-𝟘-□ = 𝟘 □ 𝟘
-
-module i⇒ = HasInterchange hasInterchange
-
-module i≃ = NaturalIsomorphism i⇒.naturalIso
-
-i⇒ = i⇒.swapInner.from
-i⇐ = i⇒.swapInner.to
-
-σ₂₃ : {A B C D : Obj} → (A ⊕ B) ⊕ (C ⊕ D) ⇒ (A ⊕ C) ⊕ (B ⊕ D)
-σ₂₃ = ⟨ π₁ ×₁ π₁ , π₂ ×₁ π₂ ⟩
-
--- 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
-    }
-
-_⊞_ : Box → Box → Box
-(Aᵢ □ Aₒ) ⊞ (Bᵢ □ Bₒ) = Aᵢ ⊕ Bᵢ □ Aₒ ⊕ Bₒ
-
-_⊞₁_
-    : {A B C D : Box}
-      (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ₒ
-
-⊞-identity : {A B : Box} → id-⧈ {A} ⊞₁ id-⧈ {B} ≈-⧈ id-⧈
-⊞-identity {A} {B} = eqᵢ ⌸ id×₁id
-  where
-    open HomReasoning
-    open ⇒-Reasoning
-    eqᵢ : π₂ ×₁ π₂ ∘ σ₂₃ ≈ π₂
-    eqᵢ = begin
-        π₂ ×₁ π₂ ∘ σ₂₃                    ≈⟨ ×₁∘⟨⟩ ⟩
-        ⟨ π₂ ∘ π₁ ×₁ π₁ , π₂ ∘ π₂ ×₁ π₂ ⟩ ≈⟨ ⟨⟩-cong₂ π₂∘×₁ π₂∘×₁ ⟩
-        ⟨ π₁ ∘ π₂ , π₂ ∘ π₂ ⟩             ≈⟨ g-η ⟩
-        π₂ ∎
-
-σ₂₃-lemma
-    : {A B C D : Obj}
-    → σ₂₃ {A} {B} {A ⊕ C} {B ⊕ D} ∘ ⟨ π₁ {A ⊕ B} {C ⊕ D} , σ₂₃ {A} {B} {C} {D} ⟩
-    ≈ ⟨ π₁ , id ⟩ ×₁ ⟨ π₁ , id ⟩ ∘ σ₂₃
-σ₂₃-lemma = begin
-    ⟨ π₁ ×₁ π₁ , π₂ ×₁ π₂ ⟩ ∘ ⟨ π₁ , ⟨ π₁ ×₁ π₁ , π₂ ×₁ π₂ ⟩ ⟩                                    ≈⟨ ⟨⟩∘ ⟩
-    ⟨ π₁ ×₁ π₁ ∘ ⟨ π₁ , ⟨ π₁ ×₁ π₁ , π₂ ×₁ π₂ ⟩ ⟩ , π₂ ×₁ π₂ ∘ ⟨ π₁ , ⟨ π₁ ×₁ π₁ , π₂ ×₁ π₂ ⟩ ⟩ ⟩ ≈⟨ ⟨⟩-cong₂ ×₁∘⟨⟩ ×₁∘⟨⟩ ⟩
-    ⟨ ⟨ π₁ ∘ π₁ , π₁ ∘ ⟨ π₁ ×₁ π₁ , π₂ ×₁ π₂ ⟩ ⟩ , ⟨ π₂ ∘ π₁ , π₂ ∘ ⟨ π₁ ×₁ π₁ , π₂ ×₁ π₂ ⟩ ⟩ ⟩   ≈⟨ ⟨⟩-cong₂ (⟨⟩-congˡ project₁) (⟨⟩-congˡ project₂) ⟩
-    ⟨ ⟨ π₁ ∘ π₁ , π₁ ×₁ π₁ ⟩ , ⟨ π₂ ∘ π₁ , π₂ ×₁ π₂ ⟩ ⟩                                           ≈⟨ ⟨⟩-cong₂ (⟨⟩-congʳ π₁∘×₁) (⟨⟩-congʳ π₁∘×₁) ⟨
-    ⟨ ⟨ π₁ ∘ π₁ ×₁ π₁ , π₁ ×₁ π₁ ⟩ , ⟨ π₁ ∘ π₂ ×₁ π₂ , π₂ ×₁ π₂ ⟩ ⟩                               ≈⟨ ⟨⟩-cong₂ (⟨⟩-congˡ identityˡ) (⟨⟩-congˡ identityˡ) ⟨
-    ⟨ ⟨ π₁ ∘ π₁ ×₁ π₁ , 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 ×₁ 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}
-      {f : WiringDiagram A C}
-      {g : WiringDiagram B D}
-      {h : WiringDiagram C E}
-      {i : WiringDiagram D F}
-    → (h ⌻ f) ⊞₁ (i ⌻ g) ≈-⧈ h ⊞₁ i ⌻ f ⊞₁ g
-⊞-homo {A} {B} {C} {D} {E} {F} {fᵢ ⧈ fₒ} {gᵢ ⧈ gₒ} {hᵢ ⧈ hₒ} {iᵢ ⧈ iₒ} = eqᵢ ⌸ Equiv.sym ×₁∘×₁
-  where
-    open HomReasoning
-    open ⇒-Reasoning
-    open Equiv
-    eqᵢ : (fᵢ ∘ ⟨ π₁ , hᵢ ∘ fₒ ×₁ id ⟩) ×₁ (gᵢ ∘ ⟨ π₁ , iᵢ ∘ gₒ ×₁ id ⟩) ∘ σ₂₃
-        ≈ (fᵢ ×₁ gᵢ ∘ σ₂₃) ∘ ⟨ π₁ , (hᵢ ×₁ iᵢ ∘ σ₂₃) ∘ (fₒ ×₁ gₒ) ×₁ id ⟩
-    eqᵢ = begin
-        (fᵢ ∘ ⟨ π₁ , hᵢ ∘ fₒ ×₁ id ⟩) ×₁ (gᵢ ∘ ⟨ π₁ , iᵢ ∘ gₒ ×₁ id ⟩) ∘ σ₂₃            ≈⟨ ×₁-cong₂ (refl⟩∘⟨ ⟨⟩-congˡ identityʳ) (refl⟩∘⟨ ⟨⟩-congˡ identityʳ) ⟩∘⟨refl ⟨
-        (fᵢ ∘ ⟨ π₁ , _ ∘ id ⟩) ×₁ (gᵢ ∘ ⟨ π₁ , (iᵢ ∘ gₒ ×₁ id) ∘ id ⟩) ∘ σ₂₃            ≈⟨ ×₁-cong₂ (pullʳ second∘⟨⟩) (pullʳ second∘⟨⟩) ⟩∘⟨refl ⟨
-        ((fᵢ ∘ id ×₁ _) ∘ ⟨ π₁ , id ⟩) ×₁ ((gᵢ ∘ id ×₁ (iᵢ ∘ gₒ ×₁ id)) ∘ ⟨ π₁ , id ⟩) ∘ σ₂₃  ≈⟨ pushˡ (sym ×₁∘×₁) ⟩
-        (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 ×₁ 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ₒ ×₁ 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 ×₁ 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 ⟩
-        (fᵢ ×₁ gᵢ ∘ σ₂₃) ∘ ⟨ π₁ , (hᵢ ×₁ iᵢ ∘ σ₂₃) ∘ (fₒ ×₁ gₒ) ×₁ id ⟩                 ∎
-
-⊞-resp-≈-⧈
-    : {A B C D : Box}
-      {f g : WiringDiagram A B}
-      {h i : WiringDiagram C D}
-    → f ≈-⧈ g
-    → 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
-  where
-    open ⇒-Reasoning
-    open HomReasoning
-    open Equiv
-    i₂∘π₂≈id : {A : Obj} → i₂ {𝟘} {A} ∘ π₂ {𝟘} {A} ≈ id
-    i₂∘π₂≈id = begin
-        i₂ ∘ π₂             ≈⟨ ⟨⟩-unique (pullˡ π₁∘i₂≈0) (cancelˡ π₂∘i₂≈id) ⟨
-        ⟨ zero⇒ ∘ π₂ , π₂ ⟩ ≈⟨ ⟨⟩-unique !-unique₂ identityʳ ⟩
-        id                  ∎
-    eqᵢ : (i₂ ∘ π₂) ∘ ⟨ π₁ , (π₂ ∘ π₂) ∘ π₂ ×₁ id ⟩ ≈ π₂
-    eqᵢ = begin
-        (i₂ ∘ π₂) ∘ ⟨ π₁ , (π₂ ∘ π₂) ∘ π₂ ×₁ id ⟩ ≈⟨ pullʳ project₂ ⟩
-        i₂ ∘ (π₂ ∘ π₂) ∘ π₂ ×₁ id                 ≈⟨ refl⟩∘⟨ pullʳ π₂∘first ⟩
-        i₂ ∘ π₂ ∘ π₂                              ≈⟨ cancelˡ i₂∘π₂≈id ⟩
-        π₂                                        ∎
-
-λ-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₂ ⟩
-        π₂ ∘ (i₂ ∘ π₂) ∘ i₂ ×₁ id                 ≈⟨ refl⟩∘⟨ pullʳ π₂∘first ⟩
-        π₂ ∘ 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) ⟨
-        ⟨ π₁ , zero⇒ ∘ π₁ ⟩ ≈⟨ ⟨⟩-unique identityʳ !-unique₂ ⟩
-        id                  ∎
-    eqᵢ : (i₁ ∘ π₂) ∘ ⟨ π₁ , (π₁ ∘ π₂) ∘ π₁ ×₁ id ⟩ ≈ π₂
-    eqᵢ = begin
-        (i₁ ∘ π₂) ∘ ⟨ π₁ , (π₁ ∘ π₂) ∘ π₁ ×₁ id ⟩ ≈⟨ pullʳ project₂ ⟩
-        i₁ ∘ (π₁ ∘ π₂) ∘ π₁ ×₁ id                 ≈⟨ refl⟩∘⟨ pullʳ π₂∘first ⟩
-        i₁ ∘ π₁ ∘ π₂                              ≈⟨ cancelˡ i₁∘π₁≈id ⟩
-        π₂                                        ∎
-
-ρ-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₂ ⟩
-        π₁ ∘ (i₁ ∘ π₂) ∘ i₁ ×₁ id                 ≈⟨ refl⟩∘⟨ pullʳ π₂∘first ⟩
-        π₁ ∘ 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) ⟩
-        (π₂ ×₁ fᵢ ∘ σ₂₃) ∘ ⟨ π₁ , i₂ ∘ π₂ ⟩                       ≈⟨ ×₁∘⟨⟩ ⟩∘⟨refl ⟩
-        ⟨ π₂ ∘ π₁ ×₁ π₁ , fᵢ ∘ π₂ ×₁ π₂ ⟩ ∘ ⟨ π₁ , i₂ ∘ π₂ ⟩      ≈⟨ ⟨⟩-congʳ π₂∘×₁ ⟩∘⟨refl ⟩
-        ⟨ π₁ ∘ π₂ , fᵢ ∘ π₂ ×₁ π₂ ⟩ ∘ ⟨ π₁ , i₂ ∘ π₂ ⟩            ≈⟨ ⟨⟩∘ ⟩
-        ⟨ (π₁ ∘ π₂) ∘ ⟨ π₁ , i₂ ∘ π₂ ⟩ , (fᵢ ∘ π₂ ×₁ π₂) ∘ ⟨ π₁ , i₂ ∘ π₂ ⟩ ⟩ ≈⟨ ⟨⟩-cong₂ (pullʳ project₂) (pullʳ ×₁∘⟨⟩) ⟩
-        ⟨ π₁ ∘ i₂ ∘ π₂ , fᵢ ∘ ⟨ π₂ ∘ π₁ , π₂ ∘ i₂ ∘ π₂ ⟩ ⟩        ≈⟨ ⟨⟩-congˡ (refl⟩∘⟨ ⟨⟩-congˡ (pullˡ π₂∘i₂≈id)) ⟩
-        ⟨ π₁ ∘ i₂ ∘ π₂ , fᵢ ∘ π₂ ×₁ id ⟩                          ≈⟨ ⟨⟩-congʳ (pullˡ π₁∘i₂≈0) ⟩
-        ⟨ zero⇒ ∘ π₂ , fᵢ ∘ π₂ ×₁ id ⟩                            ≈⟨ ⟨⟩-congʳ (zero-∘ʳ π₂) ⟩
-        ⟨ zero⇒ , fᵢ ∘ π₂ ×₁ id ⟩                                 ≈⟨ ⟨⟩-cong₂ (zero-∘ʳ (fᵢ ∘ π₂ ×₁ id)) identityˡ ⟨
-        ⟨ zero⇒ ∘ fᵢ ∘ π₂ ×₁ id , id ∘ fᵢ ∘ π₂ ×₁ id ⟩            ≈⟨ ⟨⟩∘ ⟨
-        ⟨ zero⇒ , id ⟩ ∘ fᵢ ∘ π₂ ×₁ id                            ≈⟨ ⟨⟩-unique π₁∘i₂≈0 π₂∘i₂≈id ⟩∘⟨refl ⟩
-        i₂ ∘ fᵢ ∘ π₂ ×₁ id                                        ≈⟨ pushʳ (sym project₂) ⟩
-        (i₂ ∘ π₂) ∘ ⟨ π₁ , fᵢ ∘ π₂ ×₁ id ⟩                        ∎
-
-unitorˡ-commute-to
-    : {X Y : Box}
-      {f : WiringDiagram X Y}
-    → 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₂ ⟨
-        id +₁ fₒ ∘ i₂ ≈⟨ ×₁-+₁ id fₒ ⟩∘⟨refl ⟨
-        id ×₁ fₒ ∘ i₂ ∎
-    eqᵢ : fᵢ ∘ ⟨ π₁ , (π₂ ∘ π₂) ∘ fₒ ×₁ id ⟩ ≈ (π₂ ∘ π₂) ∘ ⟨ π₁ , (π₂ ×₁ fᵢ ∘ σ₂₃) ∘ i₂ ×₁ id ⟩
-    eqᵢ = begin
-        fᵢ ∘ ⟨ π₁ , (π₂ ∘ π₂) ∘ fₒ ×₁ id ⟩                ≈⟨ refl⟩∘⟨ ⟨⟩-congˡ (pullʳ π₂∘first) ⟩
-        fᵢ ∘ ⟨ π₁ , π₂ ∘ π₂ ⟩                             ≈⟨ refl⟩∘⟨ ⟨⟩-congʳ identityˡ ⟨
-        fᵢ ∘ id ×₁ π₂                                     ≈⟨ refl⟩∘⟨ ×₁-congʳ π₂∘i₂≈id ⟨
-        fᵢ ∘ (π₂ ∘ i₂) ×₁ π₂                              ≈⟨ refl⟩∘⟨ ×₁∘first ⟨
-        fᵢ ∘ (π₂ ×₁ π₂) ∘ i₂ ×₁ id                        ≈⟨ refl⟩∘⟨ project₂ ⟩∘⟨refl ⟨
-        fᵢ ∘ (π₂ ∘ σ₂₃) ∘ i₂ ×₁ id                        ≈⟨ extendʳ (extendʳ π₂∘×₁) ⟨
-        π₂ ∘ (π₂ ×₁ fᵢ ∘ σ₂₃) ∘ i₂ ×₁ id                  ≈⟨ pushʳ (sym project₂) ⟩
-        (π₂ ∘ π₂) ∘ ⟨ π₁ , (π₂ ×₁ fᵢ ∘ σ₂₃) ∘ i₂ ×₁ id ⟩  ∎
-
-unitorʳ-commute-from
-    : {X Y : Box}
-      {f : WiringDiagram X Y}
-    → 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) ⟩
-        (fᵢ ×₁ π₂ ∘ σ₂₃) ∘ ⟨ π₁ , i₁ ∘ π₂ ⟩                         ≈⟨ ×₁∘⟨⟩ ⟩∘⟨ ⟨⟩-congʳ (sym identityˡ) ⟩
-        ⟨ fᵢ ∘ π₁ ×₁ π₁ , π₂ ∘ π₂ ×₁ π₂ ⟩ ∘ id ×₁ i₁                ≈⟨ ⟨⟩∘ ⟩
-        ⟨ (fᵢ ∘ π₁ ×₁ π₁) ∘ id ×₁ i₁ , (π₂ ∘ π₂ ×₁ π₂) ∘ id ×₁ i₁ ⟩ ≈⟨ ⟨⟩-cong₂ (pullʳ ×₁∘second) (pullʳ ×₁∘second) ⟩
-        ⟨ fᵢ ∘ π₁ ×₁ (π₁ ∘ i₁) , π₂ ∘ π₂ ×₁ (π₂ ∘ i₁) ⟩             ≈⟨ ⟨⟩-congˡ π₂∘×₁ ⟩
-        ⟨ fᵢ ∘ π₁ ×₁ (π₁ ∘ i₁) , (π₂ ∘ i₁) ∘ π₂ ⟩                   ≈⟨ ⟨⟩-cong₂ (refl⟩∘⟨ ×₁-congˡ π₁∘i₁≈id) (π₂∘i₁≈0 ⟩∘⟨refl) ⟩
-        ⟨ fᵢ ∘ π₁ ×₁ id , zero⇒ ∘ π₂ ⟩                              ≈⟨ ⟨⟩-congˡ (zero-∘ʳ π₂) ⟩
-        ⟨ fᵢ ∘ π₁ ×₁ id , zero⇒ ⟩                                   ≈⟨ ⟨⟩-cong₂ identityˡ (zero-∘ʳ (fᵢ ∘ π₁ ×₁ id)) ⟨
-        ⟨ id ∘ fᵢ ∘ π₁ ×₁ id , zero⇒ ∘ fᵢ ∘ π₁ ×₁ id ⟩              ≈⟨ ⟨⟩∘ ⟨
-        ⟨ id , zero⇒ ⟩ ∘ fᵢ ∘ π₁ ×₁ id                              ≈⟨ ⟨⟩-unique π₁∘i₁≈id π₂∘i₁≈0 ⟩∘⟨refl ⟩
-        i₁ ∘ fᵢ ∘ π₁ ×₁ id                                          ≈⟨ pushʳ (sym project₂) ⟩
-        (i₁ ∘ π₂) ∘ ⟨ π₁ , fᵢ ∘ π₁ ×₁ id ⟩                          ∎
-
-unitorʳ-commute-to
-    : {X Y : Box}
-      {f : WiringDiagram X Y}
-    → 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) ⟩
-        fᵢ ∘ ⟨ π₁ , π₁ ∘ π₂ ⟩                             ≈⟨ refl⟩∘⟨ ⟨⟩-congʳ identityˡ ⟨
-        fᵢ ∘ id ×₁ π₁                                     ≈⟨ refl⟩∘⟨ ×₁-congʳ π₁∘i₁≈id ⟨
-        fᵢ ∘ (π₁ ∘ i₁) ×₁ π₁                              ≈⟨ refl⟩∘⟨ ×₁∘first ⟨
-        fᵢ ∘ π₁ ×₁ π₁ ∘ i₁ ×₁ id                          ≈⟨ refl⟩∘⟨ pushˡ (sym project₁) ⟩
-        fᵢ ∘ π₁ ∘ σ₂₃ ∘ i₁ ×₁ id                          ≈⟨ extendʳ π₁∘×₁ ⟨
-        π₁ ∘ fᵢ ×₁ π₂ ∘ σ₂₃ ∘ i₁ ×₁ id                    ≈⟨ refl⟩∘⟨ sym-assoc ⟩
-        π₁ ∘ (fᵢ ×₁ π₂ ∘ σ₂₃) ∘ i₁ ×₁ id                  ≈⟨ pushʳ (sym project₂) ⟩
-        (π₁ ∘ π₂) ∘ ⟨ π₁ , (fᵢ ×₁ π₂ ∘ σ₂₃) ∘ i₁ ×₁ id ⟩  ∎
-    eqₒ : i₁ ∘ fₒ ≈ fₒ ×₁ id ∘ i₁
-    eqₒ = begin
-        i₁ ∘ fₒ       ≈⟨ +₁∘i₁ ⟨
-        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₂ ⟩
-        assocʳ ∘ (assocˡ ∘ π₂) ∘ assocˡ ×₁ id                 ≈⟨ refl⟩∘⟨ pullʳ π₂∘first ⟩
-        assocʳ ∘ assocˡ ∘ π₂                                  ≈⟨ cancelˡ 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₂ ⟩
-        assocˡ ∘ (assocʳ ∘ π₂) ∘ assocʳ ×₁ id                 ≈⟨ refl⟩∘⟨ pullʳ π₂∘first ⟩
-        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′}
-      {g : WiringDiagram Y Y′}
-      {h : WiringDiagram Z Z′}
-    → 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 ⟩
-        assocʳ ∘ ⟨ π₁ ×₁ π₁ , σ₂₃ ∘ π₂ ×₁ π₂ ⟩ ∘ assocˡ ×₁ id                                         ≈⟨ refl⟩∘⟨ ⟨⟩-congˡ ⟨⟩∘ ⟩∘⟨refl ⟩
-        assocʳ ∘ ⟨ π₁ ×₁ π₁ , ⟨ π₁ ×₁ π₁ ∘ π₂ ×₁ π₂ , π₂ ×₁ π₂ ∘ π₂ ×₁ π₂ ⟩ ⟩ ∘ assocˡ ×₁ id          ≈⟨ pullˡ assocʳ∘⟨⟩ ⟩
-        ⟨ ⟨ π₁ ×₁ π₁ , π₁ ×₁ π₁ ∘ π₂ ×₁ π₂ ⟩ , π₂ ×₁ π₂ ∘ π₂ ×₁ π₂ ⟩ ∘ assocˡ ×₁ id                   ≈⟨ ⟨⟩∘ ⟩
-        ⟨ ⟨ π₁ ×₁ π₁ , π₁ ×₁ π₁ ∘ π₂ ×₁ π₂ ⟩ ∘ assocˡ ×₁ id , (π₂ ×₁ π₂ ∘ π₂ ×₁ π₂) ∘ assocˡ ×₁ id ⟩  ≈⟨ ⟨⟩-congˡ (pullʳ ×₁∘first) ⟩
-        ⟨ ⟨ π₁ ×₁ π₁ , π₁ ×₁ π₁ ∘ π₂ ×₁ π₂ ⟩ ∘ assocˡ ×₁ id , π₂ ×₁ π₂ ∘ (π₂ ∘ assocˡ) ×₁ π₂ ⟩        ≈⟨ ⟨⟩-congˡ ×₁∘×₁ ⟩
-        ⟨ ⟨ π₁ ×₁ π₁ , π₁ ×₁ π₁ ∘ π₂ ×₁ π₂ ⟩ ∘ assocˡ ×₁ id , (π₂ ∘ π₂ ∘ assocˡ) ×₁ (π₂ ∘ π₂) ⟩       ≈⟨ ⟨⟩-congˡ (×₁-congʳ (refl⟩∘⟨ project₂)) ⟩
-        ⟨ ⟨ π₁ ×₁ π₁ , π₁ ×₁ π₁ ∘ π₂ ×₁ π₂ ⟩ ∘ assocˡ ×₁ id , (π₂ ∘ ⟨ π₂ ∘ π₁ , π₂ ⟩) ×₁ (π₂ ∘ π₂) ⟩  ≈⟨ ⟨⟩-congˡ (×₁-congʳ project₂) ⟩
-        ⟨ ⟨ π₁ ×₁ π₁ , π₁ ×₁ π₁ ∘ π₂ ×₁ π₂ ⟩ ∘ assocˡ ×₁ id , π₂ ×₁ (π₂ ∘ π₂) ⟩                       ≈⟨ ⟨⟩-congʳ ⟨⟩∘ ⟩
-        ⟨ ⟨ π₁ ×₁ π₁ ∘ assocˡ ×₁ id , (π₁ ×₁ π₁ ∘ π₂ ×₁ π₂) ∘ assocˡ ×₁ id ⟩ , π₂ ×₁ (π₂ ∘ π₂) ⟩      ≈⟨ ⟨⟩-congʳ (⟨⟩-congˡ (pullʳ ×₁∘first)) ⟩
-        ⟨ ⟨ π₁ ×₁ π₁ ∘ assocˡ ×₁ id , π₁ ×₁ π₁ ∘ (π₂ ∘ assocˡ) ×₁ π₂ ⟩ , π₂ ×₁ (π₂ ∘ π₂) ⟩            ≈⟨ ⟨⟩-congʳ (⟨⟩-congˡ ×₁∘×₁) ⟩
-        ⟨ ⟨ π₁ ×₁ π₁ ∘ assocˡ ×₁ id , (π₁ ∘ π₂ ∘ assocˡ) ×₁ (π₁ ∘ π₂) ⟩ , π₂ ×₁ (π₂ ∘ π₂) ⟩           ≈⟨ ⟨⟩-congʳ (⟨⟩-congˡ (×₁-congʳ (refl⟩∘⟨ project₂))) ⟩
-        ⟨ ⟨ π₁ ×₁ π₁ ∘ assocˡ ×₁ id , (π₁ ∘ ⟨ π₂ ∘ π₁ , π₂ ⟩) ×₁ (π₁ ∘ π₂) ⟩ , π₂ ×₁ (π₂ ∘ π₂) ⟩      ≈⟨ ⟨⟩-congʳ (⟨⟩-congˡ (×₁-congʳ project₁)) ⟩
-        ⟨ ⟨ π₁ ×₁ π₁ ∘ assocˡ ×₁ id , (π₂ ∘ π₁) ×₁ (π₁ ∘ π₂) ⟩ , π₂ ×₁ (π₂ ∘ π₂) ⟩                    ≈⟨ ⟨⟩-congʳ (⟨⟩-congʳ ×₁∘first) ⟩
-        ⟨ ⟨ (π₁ ∘ assocˡ) ×₁ π₁ , (π₂ ∘ π₁) ×₁ (π₁ ∘ π₂) ⟩ , π₂ ×₁ (π₂ ∘ π₂) ⟩                        ≈⟨ ⟨⟩-congʳ (⟨⟩-congʳ (×₁-congʳ project₁)) ⟩
-        ⟨ ⟨ (π₁ ∘ π₁) ×₁ π₁ , (π₂ ∘ π₁) ×₁ (π₁ ∘ π₂) ⟩ , π₂ ×₁ (π₂ ∘ π₂) ⟩                            ≈⟨ ⟨⟩-congʳ (⟨⟩-cong₂ (×₁-congˡ project₁) (×₁-congˡ project₂)) ⟨
-        ⟨ ⟨ (π₁ ∘ π₁) ×₁ (π₁ ∘ ⟨ π₁ , π₁ ∘ π₂ ⟩) , (π₂ ∘ π₁) ×₁ (π₂ ∘ ⟨ π₁ , π₁ ∘ π₂ ⟩) ⟩ , π₂ ×₁ (π₂ ∘ π₂) ⟩ ≈⟨ ⟨⟩-congʳ (⟨⟩-cong₂ (×₁-congˡ (refl⟩∘⟨ project₁)) (×₁-congˡ (refl⟩∘⟨ project₁))) ⟨
-        ⟨ ⟨ (π₁ ∘ π₁) ×₁ (π₁ ∘ π₁ ∘ assocʳ) , (π₂ ∘ π₁) ×₁ (π₂ ∘ π₁ ∘ assocʳ) ⟩ , π₂ ×₁ (π₂ ∘ π₂) ⟩   ≈⟨ ⟨⟩-congʳ (⟨⟩-cong₂ ×₁∘×₁ ×₁∘×₁) ⟨
-        ⟨ ⟨ π₁ ×₁ π₁ ∘ π₁ ×₁ (π₁ ∘ assocʳ) , π₂ ×₁ π₂ ∘ π₁ ×₁ (π₁ ∘ assocʳ) ⟩ , π₂ ×₁ (π₂ ∘ π₂) ⟩     ≈⟨ ⟨⟩-congʳ (⟨⟩-cong₂ (pushʳ (sym ×₁∘second)) (pushʳ (sym ×₁∘second))) ⟩
-        ⟨ ⟨ (π₁ ×₁ π₁ ∘ π₁ ×₁ π₁) ∘ id ×₁ assocʳ , (π₂ ×₁ π₂ ∘ π₁ ×₁ π₁) ∘ id ×₁ assocʳ ⟩ , π₂ ×₁ (π₂ ∘ π₂) ⟩ ≈⟨ ⟨⟩-congʳ ⟨⟩∘ ⟨
-        ⟨ ⟨ π₁ ×₁ π₁ ∘ π₁ ×₁ π₁ , π₂ ×₁ π₂ ∘ π₁ ×₁ π₁ ⟩ ∘ id ×₁ assocʳ , π₂ ×₁ (π₂ ∘ π₂) ⟩            ≈⟨ ⟨⟩-congˡ (×₁-congˡ project₂) ⟨
-        ⟨ ⟨ π₁ ×₁ π₁ ∘ π₁ ×₁ π₁ , π₂ ×₁ π₂ ∘ π₁ ×₁ π₁ ⟩ ∘ id ×₁ assocʳ , π₂ ×₁ (π₂ ∘ assocʳ) ⟩        ≈⟨ ⟨⟩-congˡ ×₁∘second ⟨
-        ⟨ ⟨ π₁ ×₁ π₁ ∘ π₁ ×₁ π₁ , π₂ ×₁ π₂ ∘ π₁ ×₁ π₁ ⟩ ∘ id ×₁ assocʳ , π₂ ×₁ π₂ ∘ id ×₁ assocʳ ⟩    ≈⟨ ⟨⟩∘ ⟨
-        ⟨ ⟨ π₁ ×₁ π₁ ∘ π₁ ×₁ π₁ , π₂ ×₁ π₂ ∘ π₁ ×₁ π₁ ⟩ , π₂ ×₁ π₂ ⟩ ∘ id ×₁ assocʳ                   ≈⟨ ⟨⟩-congʳ ⟨⟩∘ ⟩∘⟨refl ⟨
-        ⟨ σ₂₃ ∘ π₁ ×₁ π₁ , π₂ ×₁ π₂ ⟩ ∘ id ×₁ assocʳ                                                  ≈⟨ pushˡ (sym first∘⟨⟩) ⟩
-        σ₂₃ ×₁ id ∘ σ₂₃ ∘ id ×₁ assocʳ                                                                ∎
-    eqᵢ : (assocʳ ∘ π₂) ∘ ⟨ π₁ , (fᵢ ×₁ (gᵢ ×₁ hᵢ ∘ σ₂₃) ∘ σ₂₃) ∘ assocˡ ×₁ id ⟩ ≈ ((fᵢ ×₁ gᵢ ∘ σ₂₃) ×₁ hᵢ ∘ σ₂₃) ∘ ⟨ π₁ , (assocʳ ∘ π₂) ∘ ((fₒ ×₁ gₒ) ×₁ hₒ) ×₁ id ⟩
-    eqᵢ = begin
-        (assocʳ ∘ π₂) ∘ ⟨ π₁ , (fᵢ ×₁ (gᵢ ×₁ hᵢ ∘ σ₂₃) ∘ σ₂₃) ∘ assocˡ ×₁ id ⟩  ≈⟨ pullʳ project₂ ⟩
-        assocʳ ∘ (fᵢ ×₁ (gᵢ ×₁ hᵢ ∘ σ₂₃) ∘ σ₂₃) ∘ assocˡ ×₁ id                  ≈⟨ refl⟩∘⟨ pushˡ (pushˡ (sym ×₁∘second)) ⟩
-        assocʳ ∘ fᵢ ×₁ (gᵢ ×₁ hᵢ) ∘ (id ×₁ σ₂₃ ∘ σ₂₃) ∘ assocˡ ×₁ id            ≈⟨ extendʳ assocʳ∘×₁ ⟩
-        (fᵢ ×₁ gᵢ) ×₁ hᵢ ∘ assocʳ ∘ (id ×₁ σ₂₃ ∘ σ₂₃) ∘ assocˡ ×₁ id            ≈⟨ refl⟩∘⟨ lemma ⟩
-        (fᵢ ×₁ gᵢ) ×₁ hᵢ ∘ σ₂₃ ×₁ id ∘ σ₂₃ ∘ id ×₁ assocʳ                       ≈⟨ pullˡ ×₁∘first ⟩
-        (fᵢ ×₁ gᵢ ∘ σ₂₃) ×₁ hᵢ ∘ σ₂₃ ∘ id ×₁ assocʳ                             ≈⟨ refl⟩∘⟨ refl⟩∘⟨ ⟨⟩-congʳ identityˡ ⟩
-        (fᵢ ×₁ gᵢ ∘ σ₂₃) ×₁ hᵢ ∘ σ₂₃ ∘ ⟨ π₁ , assocʳ ∘ π₂ ⟩                     ≈⟨ pushʳ (refl⟩∘⟨ ⟨⟩-congˡ (pushʳ (sym π₂∘first))) ⟩
-        ((fᵢ ×₁ gᵢ ∘ σ₂₃) ×₁ hᵢ ∘ σ₂₃) ∘ ⟨ π₁ , (assocʳ ∘ π₂) ∘ ((fₒ ×₁ gₒ) ×₁ hₒ) ×₁ id ⟩ ∎
-    eqₒ : fₒ ×₁ (gₒ ×₁ hₒ) ∘ assocˡ ≈ assocˡ ∘ (fₒ ×₁ gₒ) ×₁ hₒ
-    eqₒ = Equiv.sym assocˡ∘×₁
-
-associator-commute-to
-    : {X X′ Y Y′ Z Z′ : Box}
-      {f : WiringDiagram X X′}
-      {g : WiringDiagram Y Y′}
-      {h : WiringDiagram Z Z′}
-    → (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 ⟩
-        assocˡ ∘ ⟨ σ₂₃ ∘ π₁ ×₁ π₁ , π₂ ×₁ π₂ ⟩ ∘ assocʳ ×₁ id                                         ≈⟨ refl⟩∘⟨ ⟨⟩-congʳ ⟨⟩∘ ⟩∘⟨refl ⟩
-        assocˡ ∘ ⟨ ⟨ π₁ ×₁ π₁ ∘ π₁ ×₁ π₁ , π₂ ×₁ π₂ ∘ π₁ ×₁ π₁ ⟩ , π₂ ×₁ π₂ ⟩ ∘ assocʳ ×₁ id          ≈⟨ pullˡ assocˡ∘⟨⟩ ⟩
-        ⟨ π₁ ×₁ π₁ ∘ π₁ ×₁ π₁ , ⟨ π₂ ×₁ π₂ ∘ π₁ ×₁ π₁ , π₂ ×₁ π₂ ⟩ ⟩ ∘ assocʳ ×₁ id                   ≈⟨ ⟨⟩∘ ⟩
-        ⟨ (π₁ ×₁ π₁ ∘ π₁ ×₁ π₁) ∘ assocʳ ×₁ id , ⟨ π₂ ×₁ π₂ ∘ π₁ ×₁ π₁ , π₂ ×₁ π₂ ⟩ ∘ assocʳ ×₁ id ⟩  ≈⟨ ⟨⟩-congʳ (pullʳ ×₁∘first) ⟩
-        ⟨ π₁ ×₁ π₁ ∘ (π₁ ∘ assocʳ) ×₁ π₁ , ⟨ π₂ ×₁ π₂ ∘ π₁ ×₁ π₁ , π₂ ×₁ π₂ ⟩ ∘ assocʳ ×₁ id ⟩        ≈⟨ ⟨⟩-congʳ ×₁∘×₁ ⟩
-        ⟨ (π₁ ∘ π₁ ∘ assocʳ) ×₁ (π₁ ∘ π₁) , ⟨ π₂ ×₁ π₂ ∘ π₁ ×₁ π₁ , π₂ ×₁ π₂ ⟩ ∘ assocʳ ×₁ id ⟩       ≈⟨ ⟨⟩-congʳ (×₁-congʳ (refl⟩∘⟨ project₁)) ⟩
-        ⟨ (π₁ ∘ ⟨ π₁ , π₁ ∘ π₂ ⟩) ×₁ (π₁ ∘ π₁) , ⟨ π₂ ×₁ π₂ ∘ π₁ ×₁ π₁ , π₂ ×₁ π₂ ⟩ ∘ assocʳ ×₁ id ⟩  ≈⟨ ⟨⟩-congʳ (×₁-congʳ project₁) ⟩
-        ⟨ π₁ ×₁ (π₁ ∘ π₁) , ⟨ π₂ ×₁ π₂ ∘ π₁ ×₁ π₁ , π₂ ×₁ π₂ ⟩ ∘ assocʳ ×₁ id ⟩                       ≈⟨ ⟨⟩-congˡ ⟨⟩∘ ⟩
-        ⟨ π₁ ×₁ (π₁ ∘ π₁) , ⟨ (π₂ ×₁ π₂ ∘ π₁ ×₁ π₁) ∘ assocʳ ×₁ id , π₂ ×₁ π₂ ∘ assocʳ ×₁ id ⟩ ⟩      ≈⟨ ⟨⟩-congˡ (⟨⟩-congʳ (pullʳ ×₁∘first)) ⟩
-        ⟨ π₁ ×₁ (π₁ ∘ π₁) , ⟨ π₂ ×₁ π₂ ∘ (π₁ ∘ assocʳ) ×₁ π₁ , π₂ ×₁ π₂ ∘ assocʳ ×₁ id ⟩ ⟩            ≈⟨ ⟨⟩-congˡ (⟨⟩-cong₂ ×₁∘×₁ ×₁∘first) ⟩
-        ⟨ π₁ ×₁ (π₁ ∘ π₁) , ⟨ (π₂ ∘ π₁ ∘ assocʳ) ×₁ (π₂ ∘ π₁) , (π₂ ∘ assocʳ) ×₁ π₂ ⟩ ⟩               ≈⟨ ⟨⟩-congˡ (⟨⟩-cong₂ (×₁-congʳ (refl⟩∘⟨ project₁)) (×₁-congʳ project₂)) ⟩
-        ⟨ π₁ ×₁ (π₁ ∘ π₁) , ⟨ (π₂ ∘ ⟨ π₁ , π₁ ∘ π₂ ⟩) ×₁ (π₂ ∘ π₁) , (π₂ ∘ π₂) ×₁ π₂ ⟩ ⟩              ≈⟨ ⟨⟩-congˡ (⟨⟩-congʳ (×₁-congʳ project₂)) ⟩
-        ⟨ π₁ ×₁ (π₁ ∘ π₁) , ⟨ (π₁ ∘ π₂) ×₁ (π₂ ∘ π₁) , (π₂ ∘ π₂) ×₁ π₂ ⟩ ⟩                            ≈⟨ ⟨⟩-congˡ (⟨⟩-cong₂ (×₁-congˡ project₁) (×₁-congˡ project₂)) ⟨
-        ⟨ π₁ ×₁ (π₁ ∘ π₁) , ⟨ (π₁ ∘ π₂) ×₁ (π₁ ∘ ⟨ _ , π₂ ⟩) , (π₂ ∘ π₂) ×₁ (π₂ ∘ ⟨ _ , π₂ ⟩) ⟩ ⟩     ≈⟨ ⟨⟩-congˡ (⟨⟩-cong₂ ×₁∘×₁ ×₁∘×₁) ⟨
-        ⟨ π₁ ×₁ (π₁ ∘ π₁) , ⟨ π₁ ×₁ π₁ ∘ π₂ ×₁ ⟨ π₂ ∘ π₁ , π₂ ⟩ , π₂ ×₁ π₂ ∘ π₂ ×₁ ⟨ _ , π₂ ⟩ ⟩ ⟩     ≈⟨ ⟨⟩-congˡ ⟨⟩∘ ⟨
-        ⟨ π₁ ×₁ (π₁ ∘ π₁) , σ₂₃ ∘ π₂ ×₁ ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩                                            ≈⟨ ⟨⟩-cong₂ (×₁-congˡ project₁) (refl⟩∘⟨ (×₁-congˡ project₂)) ⟨
-        ⟨ π₁ ×₁ (π₁ ∘ assocˡ) , σ₂₃ ∘ π₂ ×₁ (π₂ ∘ assocˡ) ⟩                                           ≈⟨ ⟨⟩-cong₂ (sym ×₁∘second) (pushʳ (sym ×₁∘second)) ⟩
-        ⟨ π₁ ×₁ π₁ ∘ id ×₁ assocˡ , (σ₂₃ ∘ π₂ ×₁ π₂) ∘ id ×₁ assocˡ ⟩                                 ≈⟨ ⟨⟩∘ ⟨
-        ⟨ π₁ ×₁  π₁ , σ₂₃ ∘ π₂ ×₁ π₂ ⟩ ∘ id ×₁ assocˡ                                                 ≈⟨ pushˡ (sym second∘⟨⟩) ⟩
-        id ×₁ σ₂₃ ∘ σ₂₃ ∘ id ×₁ assocˡ                                                                ∎
-    eqᵢ : (assocˡ ∘ π₂) ∘ ⟨ π₁ , ((fᵢ ×₁ gᵢ ∘ σ₂₃) ×₁ hᵢ ∘ σ₂₃) ∘ assocʳ ×₁ id ⟩ ≈ (fᵢ ×₁ (gᵢ ×₁ hᵢ ∘ σ₂₃) ∘ σ₂₃) ∘ ⟨ π₁ , (assocˡ ∘ π₂) ∘ (fₒ ×₁ (gₒ ×₁ hₒ)) ×₁ id ⟩
-    eqᵢ = begin
-        (assocˡ ∘ π₂) ∘ ⟨ π₁ , ((fᵢ ×₁ gᵢ ∘ σ₂₃) ×₁ hᵢ ∘ σ₂₃) ∘ assocʳ ×₁ id ⟩  ≈⟨ pullʳ project₂ ⟩
-        assocˡ ∘ ((fᵢ ×₁ gᵢ ∘ σ₂₃) ×₁ hᵢ ∘ σ₂₃) ∘ assocʳ ×₁ id                  ≈⟨ refl⟩∘⟨ pushˡ (pushˡ (sym ×₁∘first)) ⟩
-        assocˡ ∘ (fᵢ ×₁ gᵢ) ×₁ hᵢ ∘ (σ₂₃ ×₁ id ∘ σ₂₃) ∘ assocʳ ×₁ id            ≈⟨ extendʳ assocˡ∘×₁ ⟩
-        fᵢ ×₁ (gᵢ ×₁ hᵢ) ∘ assocˡ ∘ (σ₂₃ ×₁ id ∘ σ₂₃) ∘ assocʳ ×₁ id            ≈⟨ refl⟩∘⟨ lemma ⟩
-        fᵢ ×₁ (gᵢ ×₁ hᵢ) ∘ id ×₁ σ₂₃ ∘ σ₂₃ ∘ id ×₁ assocˡ                       ≈⟨ pullˡ ×₁∘second ⟩
-        fᵢ ×₁ (gᵢ ×₁ hᵢ ∘ σ₂₃) ∘ σ₂₃ ∘ id ×₁ assocˡ                             ≈⟨ refl⟩∘⟨ refl⟩∘⟨ ⟨⟩-congʳ identityˡ ⟩
-        fᵢ ×₁ (gᵢ ×₁ hᵢ ∘ σ₂₃) ∘ σ₂₃ ∘ ⟨ π₁ , assocˡ ∘ π₂ ⟩                     ≈⟨ pushʳ (refl⟩∘⟨ ⟨⟩-congˡ (pushʳ (sym π₂∘first))) ⟩
-        (fᵢ ×₁ (gᵢ ×₁ hᵢ ∘ σ₂₃) ∘ σ₂₃) ∘ ⟨ π₁ , (assocˡ ∘ π₂) ∘ (fₒ ×₁ (gₒ ×₁ hₒ)) ×₁ id ⟩ ∎
-    eqₒ : (fₒ ×₁ gₒ) ×₁ hₒ ∘ assocʳ ≈ assocʳ ∘ fₒ ×₁ (gₒ ×₁ hₒ)
-    eqₒ = Equiv.sym assocʳ∘×₁
-
-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₂ ⟩
-        assocʳ ∘ (π₂ ×₁ (i₂ ∘ π₂) ∘ σ₂₃) ∘ assocˡ ×₁ id                   ≈⟨ refl⟩∘⟨ ×₁∘⟨⟩ ⟩∘⟨refl ⟩
-        assocʳ ∘ ⟨ π₂ ∘ π₁ ×₁ π₁ , (i₂ ∘ π₂) ∘ π₂ ×₁ π₂ ⟩ ∘ assocˡ ×₁ id  ≈⟨ refl⟩∘⟨ ⟨⟩-cong₂ π₂∘×₁ (pullʳ π₂∘×₁) ⟩∘⟨refl ⟩
-        assocʳ ∘ ⟨ π₁ ∘ π₂ , i₂ ∘ π₂ ∘ π₂ ⟩ ∘ assocˡ ×₁ id                ≈⟨ refl⟩∘⟨ ⟨⟩∘ ⟩
-        assocʳ ∘ ⟨ (π₁ ∘ π₂) ∘ assocˡ ×₁ id , (i₂ ∘ π₂ ∘ π₂) ∘ _ ×₁ id ⟩  ≈⟨ refl⟩∘⟨ ⟨⟩-cong₂ (pullʳ π₂∘first) (pullʳ (pullʳ π₂∘first)) ⟩
-        assocʳ ∘ ⟨ π₁ ∘ π₂ , i₂ ∘ π₂ ∘ π₂ ⟩                               ≈⟨ ⟨⟩∘ ⟩
-        ⟨ ⟨ π₁ , π₁ ∘ π₂ ⟩ ∘ _ , (π₂ ∘ π₂) ∘ ⟨ π₁ ∘ π₂ , i₂ ∘ π₂ ∘ π₂ ⟩ ⟩ ≈⟨ ⟨⟩-congʳ (⟨⟩-congʳ identityˡ ⟩∘⟨refl) ⟨
-        ⟨ ⟨ id ∘ π₁ , π₁ ∘ π₂ ⟩ ∘ _ , _ ∘ ⟨ π₁ ∘ π₂ , i₂ ∘ π₂ ∘ π₂ ⟩ ⟩    ≈⟨ ⟨⟩-cong₂ second∘⟨⟩ (pullʳ project₂) ⟩
-        ⟨ ⟨ π₁ ∘ π₂ , π₁ ∘ i₂ ∘ π₂ ∘ π₂ ⟩ , π₂ ∘ i₂ ∘ π₂ ∘ π₂ ⟩           ≈⟨ ⟨⟩-cong₂ (⟨⟩-congˡ (pullˡ π₁∘i₂≈0)) (cancelˡ π₂∘i₂≈id) ⟩
-        ⟨ ⟨ π₁ ∘ π₂ , zero⇒ ∘ π₂ ∘ π₂ ⟩ , π₂ ∘ π₂ ⟩                       ≈⟨ ⟨⟩-congʳ (⟨⟩-congˡ (zero-∘ʳ (π₂ ∘ π₂))) ⟩
-        ⟨ ⟨ π₁ ∘ π₂ , zero⇒ ⟩ , π₂ ∘ π₂ ⟩                                 ≈⟨ ⟨⟩-congʳ (⟨⟩-unique (cancelˡ π₁∘i₁≈id) (pullˡ π₂∘i₁≈0 ○ zero-∘ʳ (π₁ ∘ π₂))) ⟩
-        ⟨ i₁ ∘ π₁ ∘ π₂ , π₂ ∘ π₂ ⟩                                        ≈⟨ ⟨⟩-cong₂ (pullʳ π₂∘×₁) π₂∘×₁ ⟨
-        ⟨ (i₁ ∘ π₂) ∘ π₁ ×₁ π₁ , π₂ ∘ π₂ ×₁ π₂ ⟩                          ≈⟨ ×₁∘⟨⟩ ⟨
-        (i₁ ∘ π₂) ×₁ π₂ ∘ σ₂₃                                             ∎
-
-pent
-    : {W X Y Z : Box}
-    → id-⧈ {W} ⊞₁ associator⇒ ⌻ associator⇒ ⌻ associator⇒ {W} {X} {Y} ⊞₁ id-⧈ {Z}
-    ≈-⧈ 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
-        (((assocʳ ∘ π₂) ×₁ π₂ ∘ σ₂₃) ∘ ⟨ π₁ , (assocʳ ∘ π₂) ∘ (assocˡ ×₁ id) ×₁ id ⟩) ∘ _ ≈⟨ (refl⟩∘⟨ ⟨⟩-congˡ (pullʳ π₂∘first)) ⟩∘⟨refl ⟩
-        (((assocʳ ∘ π₂) ×₁ π₂ ∘ σ₂₃) ∘ ⟨ π₁ , assocʳ ∘ π₂ ⟩) ∘ _                          ≈⟨ ×₁∘⟨⟩ ⟩∘⟨refl ⟩∘⟨refl ⟩
-        (⟨ (assocʳ ∘ π₂) ∘ π₁ ×₁ π₁ , π₂ ∘ π₂ ×₁ π₂ ⟩ ∘ ⟨ π₁ , assocʳ ∘ π₂ ⟩) ∘ _         ≈⟨ ⟨⟩-cong₂ (extendˡ π₂∘×₁) π₂∘×₁ ⟩∘⟨refl ⟩∘⟨refl ⟩
-        (⟨ (assocʳ ∘ π₁) ∘ π₂ , π₂ ∘ π₂ ⟩ ∘ ⟨ π₁ , assocʳ ∘ π₂ ⟩) ∘ _                     ≈⟨ pushˡ (sym ⟨⟩∘) ⟩∘⟨refl ⟩
-        (⟨ assocʳ ∘ π₁ , π₂ ⟩ ∘ π₂ ∘ ⟨ π₁ , assocʳ ∘ π₂ ⟩) ∘ _                            ≈⟨ extendˡ (pushˡ project₂) ⟩
-        (⟨ assocʳ ∘ π₁ , π₂ ⟩ ∘ assocʳ) ∘ π₂ ∘ ⟨ π₁ , _ ∘ (assocˡ ∘ assocˡ ×₁ id) ×₁ id ⟩ ≈⟨ refl⟩∘⟨ project₂ ⟩
-        (⟨ assocʳ ∘ π₁ , π₂ ⟩ ∘ assocʳ) ∘ (π₂ ×₁ (assocʳ ∘ π₂) ∘ σ₂₃) ∘ _ ×₁ id           ≈⟨ refl⟩∘⟨ ×₁∘⟨⟩ ⟩∘⟨refl ⟩
-        (⟨ assocʳ ∘ π₁ , π₂ ⟩ ∘ _) ∘ ⟨ π₂ ∘ π₁ ×₁ π₁ , _ ∘ π₂ ×₁ π₂ ⟩ ∘ _ ×₁ id           ≈⟨ refl⟩∘⟨ ⟨⟩-cong₂ π₂∘×₁ (extendˡ π₂∘×₁) ⟩∘⟨ refl ⟩
-        (⟨ assocʳ ∘ π₁ , π₂ ⟩ ∘ _) ∘ ⟨ π₁ ∘ π₂ , (assocʳ ∘ π₂) ∘ π₂ ⟩ ∘ _ ×₁ id           ≈⟨ refl⟩∘⟨ pushˡ (sym ⟨⟩∘) ⟩
-        (⟨ assocʳ ∘ π₁ , π₂ ⟩ ∘ assocʳ) ∘ ⟨ π₁ , assocʳ ∘ π₂ ⟩ ∘ π₂ ∘ _ ×₁ id             ≈⟨ (⟨⟩-congˡ identityˡ ⟩∘⟨refl) ⟩∘⟨ ⟨⟩-congʳ identityˡ ⟩∘⟨ sym π₂∘first ⟨
-        (assocʳ ×₁ id ∘ assocʳ) ∘ id ×₁ assocʳ ∘ π₂                                       ≈⟨ extendʳ (pentagon-inv monoidal) ⟩
-        assocʳ ∘ assocʳ ∘ π₂                                                              ≈⟨ refl⟩∘⟨ pushʳ (sym π₂∘first) ⟩
-        assocʳ ∘ (assocʳ ∘ π₂) ∘ assocˡ ×₁ id                                             ≈⟨ pushʳ (sym project₂) ⟩
-        (assocʳ ∘ π₂) ∘ ⟨ π₁ , (assocʳ ∘ π₂) ∘ assocˡ ×₁ id ⟩                             ∎
-
-DWD-Monoidal : Monoidal DWD
-DWD-Monoidal = record
-    { ⊗ = -⊞-
-    ; unit = 𝟘-□
-    ; unitorˡ = unitorˡ
-    ; unitorʳ = unitorʳ
-    ; associator = 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
-    }