diff options
Diffstat (limited to 'Data')
| -rw-r--r-- | Data/WiringDiagram/Monoidal.agda | 591 |
1 files changed, 591 insertions, 0 deletions
diff --git a/Data/WiringDiagram/Monoidal.agda b/Data/WiringDiagram/Monoidal.agda new file mode 100644 index 0000000..1327b1d --- /dev/null +++ b/Data/WiringDiagram/Monoidal.agda @@ -0,0 +1,591 @@ +{-# 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 + } |