{-# 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
    }