diff options
Diffstat (limited to 'Data/WiringDiagram/Monoidal')
| -rw-r--r-- | Data/WiringDiagram/Monoidal/Braided.agda | 182 | ||||
| -rw-r--r-- | Data/WiringDiagram/Monoidal/Core.agda | 624 |
2 files changed, 806 insertions, 0 deletions
diff --git a/Data/WiringDiagram/Monoidal/Braided.agda b/Data/WiringDiagram/Monoidal/Braided.agda new file mode 100644 index 0000000..7b28d85 --- /dev/null +++ b/Data/WiringDiagram/Monoidal/Braided.agda @@ -0,0 +1,182 @@ +{-# OPTIONS --without-K --safe #-} + +open import Categories.Category using (Category) +open import Category.Dagger.Semiadditive using (SemiadditiveDagger) +open import Level using (Level) + +module Data.WiringDiagram.Monoidal.Braided + {o ℓ e : Level} + {𝒞 : Category o ℓ e} + (S : SemiadditiveDagger 𝒞) + where + +import Categories.Morphism.Reasoning 𝒞 as ⇒-Reasoning +import Data.WiringDiagram.Core as WD + +open import Categories.Category.Monoidal using (Monoidal) +open import Categories.Category.Monoidal.Braided using (Braided) +open import Categories.Category.Monoidal.Braided.Properties using (hexagon₁-inv; hexagon₂-inv) +open import Categories.Category.Monoidal.Symmetric using (module Symmetric) +open import Categories.Functor.Bifunctor using (flip-bifunctor) +open import Categories.NaturalTransformation.NaturalIsomorphism using (_≃_; niHelper) +open import Data.Product using (uncurry; _,_) +open import Data.WiringDiagram.Monoidal.Core S + using (_⊞_; _⊞₁_; σ₂₃; associator⇒; associator⇐; DWD-Monoidal; BWD-Monoidal) + renaming (module Directed to D; module Balanced to B) +open import Function using (flip) + +open Category 𝒞 +open SemiadditiveDagger S +open Symmetric symmetric using (braided; hexagon₁; hexagon₂) +open WD S using (Box; WiringDiagram; _□_; _⧈_; _≈-⧈_; _⌸_; id-⧈; _⌻_; ≈-sym) + +open HomReasoning +open ⇒-Reasoning +open Equiv + +σ₂₃-⟨⟩ + : {X A B C D : Obj} + {f : X ⇒ A} + {g : X ⇒ B} + {h : X ⇒ C} + {i : X ⇒ D} + → σ₂₃ ∘ ⟨ ⟨ f , g ⟩ , ⟨ h , i ⟩ ⟩ ≈ ⟨ ⟨ f , h ⟩ , ⟨ g , i ⟩ ⟩ +σ₂₃-⟨⟩ {f = f} {g} {h} {i} = begin + σ₂₃ ∘ ⟨ ⟨ f , g ⟩ , ⟨ h , i ⟩ ⟩ ≈⟨ ⟨⟩∘ ⟩ + ⟨ π₁ ×₁ π₁ ∘ ⟨ ⟨ f , g ⟩ , ⟨ h , i ⟩ ⟩ , π₂ ×₁ π₂ ∘ ⟨ ⟨ f , g ⟩ , ⟨ h , i ⟩ ⟩ ⟩ ≈⟨ ⟨⟩-cong₂ ×₁∘⟨⟩ ×₁∘⟨⟩ ⟩ + ⟨ ⟨ π₁ ∘ ⟨ f , g ⟩ , π₁ ∘ ⟨ h , i ⟩ ⟩ , ⟨ π₂ ∘ ⟨ f , g ⟩ , π₂ ∘ ⟨ h , i ⟩ ⟩ ⟩ ≈⟨ ⟨⟩-cong₂ (⟨⟩-cong₂ project₁ project₁) (⟨⟩-cong₂ project₂ project₂) ⟩ + ⟨ ⟨ f , h ⟩ , ⟨ g , i ⟩ ⟩ ∎ + +swap-⧈ : (X Y : Box) → WiringDiagram (X ⊞ Y) (Y ⊞ X) +swap-⧈ X Y = swap ∘ π₂ ⧈ swap + +swap-commute + : {X X′ Y Y′ : Box} + (f : WiringDiagram X X′) + (g : WiringDiagram Y Y′) + → swap-⧈ X′ Y′ ⌻ f ⊞₁ g ≈-⧈ g ⊞₁ f ⌻ swap-⧈ X Y +swap-commute (fᵢ ⧈ fₒ) (gᵢ ⧈ gₒ) = eqᵢ ⌸ swap∘×₁ + where + eqᵢ : (fᵢ ×₁ gᵢ ∘ σ₂₃) ∘ ⟨ π₁ , (swap ∘ π₂) ∘ (fₒ ×₁ gₒ) ×₁ id ⟩ ≈ (swap ∘ π₂) ∘ ⟨ π₁ , (gᵢ ×₁ fᵢ ∘ σ₂₃) ∘ swap ×₁ id ⟩ + eqᵢ = begin + (fᵢ ×₁ gᵢ ∘ σ₂₃) ∘ ⟨ π₁ , (swap ∘ π₂) ∘ (fₒ ×₁ gₒ) ×₁ id ⟩ ≈⟨ refl⟩∘⟨ ⟨⟩-congˡ (pullʳ π₂∘first) ⟩ + (fᵢ ×₁ gᵢ ∘ σ₂₃) ∘ ⟨ π₁ , swap ∘ π₂ ⟩ ≈⟨ pullʳ ⟨⟩∘ ⟩ + fᵢ ×₁ gᵢ ∘ ⟨ π₁ ×₁ π₁ ∘ _ , π₂ ×₁ π₂ ∘ ⟨ π₁ , swap ∘ π₂ ⟩ ⟩ ≈⟨ refl⟩∘⟨ ⟨⟩-cong₂ ×₁∘⟨⟩ ×₁∘⟨⟩ ⟩ + fᵢ ×₁ gᵢ ∘ ⟨ ⟨ _ , _ ⟩ , ⟨ π₂ ∘ π₁ , π₂ ∘ swap ∘ π₂ ⟩ ⟩ ≈⟨ refl⟩∘⟨ ⟨⟩-cong₂ (⟨⟩-congˡ (pullˡ project₁)) (⟨⟩-congˡ (pullˡ project₂)) ⟩ + fᵢ ×₁ gᵢ ∘ ⟨ π₁ ×₁ π₂ , π₂ ×₁ π₁ ⟩ ≈⟨ refl⟩∘⟨ swap∘⟨⟩ ⟨ + fᵢ ×₁ gᵢ ∘ swap ∘ ⟨ π₂ ×₁ π₁ , π₁ ×₁ π₂ ⟩ ≈⟨ refl⟩∘⟨ pushʳ (sym σ₂₃-⟨⟩) ⟩ + fᵢ ×₁ gᵢ ∘ (swap ∘ σ₂₃) ∘ ⟨ _ , ⟨ π₁ ∘ π₂ , π₂ ∘ π₂ ⟩ ⟩ ≈⟨ refl⟩∘⟨ refl⟩∘⟨ ⟨⟩-cong₂ ⟨⟩∘ ⟨⟩∘ ⟨ + fᵢ ×₁ gᵢ ∘ (swap ∘ σ₂₃) ∘ ⟨ _ ∘ π₁ , ⟨ π₁ , π₂ ⟩ ∘ π₂ ⟩ ≈⟨ refl⟩∘⟨ refl⟩∘⟨ ⟨⟩-congˡ (η ⟩∘⟨refl) ⟩ + fᵢ ×₁ gᵢ ∘ (swap ∘ σ₂₃) ∘ swap ×₁ id ≈⟨ extendʳ (extendʳ swap∘×₁) ⟨ + swap ∘ (gᵢ ×₁ fᵢ ∘ σ₂₃) ∘ swap ×₁ id ≈⟨ pushʳ (sym project₂) ⟩ + (swap ∘ π₂) ∘ ⟨ π₁ , (gᵢ ×₁ fᵢ ∘ σ₂₃) ∘ swap ×₁ id ⟩ ∎ + +swap∘swap-⧈ + : {X Y : Box} + → swap-⧈ Y X ⌻ swap-⧈ X Y ≈-⧈ id-⧈ +swap∘swap-⧈ = eqᵢ ⌸ swap∘swap + where + eqᵢ : (swap ∘ π₂) ∘ ⟨ π₁ , (swap ∘ π₂) ∘ swap ×₁ id ⟩ ≈ π₂ + eqᵢ = begin + (swap ∘ π₂) ∘ ⟨ π₁ , (swap ∘ π₂) ∘ swap ×₁ id ⟩ ≈⟨ pullʳ project₂ ⟩ + swap ∘ (swap ∘ π₂) ∘ swap ×₁ id ≈⟨ refl⟩∘⟨ pullʳ π₂∘first ⟩ + swap ∘ swap ∘ π₂ ≈⟨ cancelˡ swap∘swap ⟩ + π₂ ∎ + +hex₁ + : {X Y Z : Box} + → id-⧈ ⊞₁ swap-⧈ X Z ⌻ associator⇒ ⌻ swap-⧈ X Y ⊞₁ id-⧈ {Z} + ≈-⧈ associator⇒ ⌻ swap-⧈ X (Y ⊞ Z) ⌻ associator⇒ +hex₁ = eqᵢ ⌸ hexagon₁ + where + eqᵢ : (((swap ∘ π₂) ×₁ π₂ ∘ σ₂₃) ∘ ⟨ π₁ , (assocʳ ∘ π₂) ∘ (swap ×₁ id) ×₁ id ⟩) ∘ ⟨ π₁ , (π₂ ×₁ (swap ∘ π₂) ∘ σ₂₃) ∘ (assocˡ ∘ swap ×₁ id) ×₁ id ⟩ + ≈ ((assocʳ ∘ π₂) ∘ ⟨ π₁ , (swap ∘ π₂) ∘ assocˡ ×₁ id ⟩) ∘ ⟨ π₁ , (assocʳ ∘ π₂) ∘ (swap ∘ assocˡ) ×₁ id ⟩ + eqᵢ = begin + (((swap ∘ π₂) ×₁ π₂ ∘ σ₂₃) ∘ ⟨ π₁ , (assocʳ ∘ π₂) ∘ (swap ×₁ id) ×₁ id ⟩) ∘ _ ≈⟨ (refl⟩∘⟨ ⟨⟩-congˡ (pullʳ π₂∘first)) ⟩∘⟨refl ⟩ + (((swap ∘ π₂) ×₁ π₂ ∘ ⟨ π₁ ×₁ π₁ , π₂ ×₁ π₂ ⟩) ∘ ⟨ π₁ , assocʳ ∘ π₂ ⟩) ∘ _ ≈⟨ ×₁∘⟨⟩ ⟩∘⟨refl ⟩∘⟨refl ⟩ + ((⟨ (swap ∘ π₂) ∘ π₁ ×₁ π₁ , π₂ ∘ π₂ ×₁ π₂ ⟩) ∘ ⟨ π₁ , assocʳ ∘ π₂ ⟩) ∘ _ ≈⟨ ⟨⟩-cong₂ (extendˡ π₂∘×₁) π₂∘×₁ ⟩∘⟨refl ⟩∘⟨refl ⟩ + ((⟨ (swap ∘ π₁) ∘ π₂ , π₂ ∘ π₂ ⟩) ∘ ⟨ π₁ , assocʳ ∘ π₂ ⟩) ∘ _ ≈⟨ ⟨⟩∘ ⟩∘⟨refl ⟩∘⟨refl ⟨ + ((⟨ swap ∘ π₁ , π₂ ⟩ ∘ π₂) ∘ ⟨ π₁ , assocʳ ∘ π₂ ⟩) ∘ _ ≈⟨ pullʳ project₂ ⟩∘⟨refl ⟩ + (⟨ swap ∘ π₁ , π₂ ⟩ ∘ assocʳ ∘ π₂) ∘ _ ≈⟨ pullʳ (pullʳ project₂) ⟩ + ⟨ swap ∘ π₁ , π₂ ⟩ ∘ assocʳ ∘ (π₂ ×₁ (swap ∘ π₂) ∘ σ₂₃) ∘ _ ×₁ id ≈⟨ refl⟩∘⟨ refl⟩∘⟨ ×₁∘⟨⟩ ⟩∘⟨refl ⟩ + ⟨ _ ∘ π₁ , π₂ ⟩ ∘ _ ∘ ⟨ π₂ ∘ π₁ ×₁ π₁ , (swap ∘ π₂) ∘ π₂ ×₁ π₂ ⟩ ∘ _ ×₁ id ≈⟨ refl⟩∘⟨ refl⟩∘⟨ ⟨⟩-cong₂ π₂∘×₁ (extendˡ π₂∘×₁) ⟩∘⟨refl ⟩ + ⟨ swap ∘ π₁ , π₂ ⟩ ∘ assocʳ ∘ ⟨ π₁ ∘ π₂ , (swap ∘ π₂) ∘ π₂ ⟩ ∘ _ ×₁ id ≈⟨ refl⟩∘⟨ refl⟩∘⟨ pushˡ (sym ⟨⟩∘) ⟩ + ⟨ swap ∘ π₁ , π₂ ⟩ ∘ assocʳ ∘ ⟨ π₁ , swap ∘ π₂ ⟩ ∘ π₂ ∘ _ ×₁ id ≈⟨ pushʳ (refl⟩∘⟨ refl⟩∘⟨ π₂∘first) ⟩ + (⟨ swap ∘ π₁ , π₂ ⟩ ∘ assocʳ) ∘ ⟨ π₁ , swap ∘ π₂ ⟩ ∘ π₂ ≈⟨ (⟨⟩-congˡ identityˡ ⟩∘⟨refl) ⟩∘⟨ ⟨⟩-congʳ identityˡ ⟩∘⟨refl ⟨ + (swap ×₁ id ∘ assocʳ) ∘ id ×₁ swap ∘ π₂ ≈⟨ extendʳ (hexagon₁-inv braided) ⟩ + (assocʳ ∘ swap) ∘ assocʳ ∘ π₂ ≈⟨ refl⟩∘⟨ pushʳ (sym π₂∘first) ⟩ + (assocʳ ∘ swap) ∘ (assocʳ ∘ π₂) ∘ _ ×₁ id ≈⟨ pushʳ (sym project₂) ⟩ + ((assocʳ ∘ swap) ∘ π₂) ∘ ⟨ π₁ , (assocʳ ∘ π₂) ∘ _ ×₁ id ⟩ ≈⟨ pullʳ (pushʳ (sym π₂∘first)) ⟩∘⟨refl ⟩ + (assocʳ ∘ (swap ∘ π₂) ∘ assocˡ ×₁ id) ∘ ⟨ π₁ , (assocʳ ∘ π₂) ∘ _ ×₁ id ⟩ ≈⟨ pushʳ (sym project₂) ⟩∘⟨refl ⟩ + ((assocʳ ∘ π₂) ∘ ⟨ π₁ , (swap ∘ π₂) ∘ assocˡ ×₁ id ⟩) ∘ ⟨ π₁ , _ ∘ _ ×₁ id ⟩ ∎ + +hex₂ + : {X Y Z : Box} + → (swap-⧈ X Z ⊞₁ id-⧈ ⌻ associator⇐) ⌻ id-⧈ {X} ⊞₁ swap-⧈ Y Z + ≈-⧈ (associator⇐ ⌻ swap-⧈ (X ⊞ Y) Z) ⌻ associator⇐ +hex₂ = eqᵢ ⌸ hexagon₂ + where + eqᵢ : (π₂ ×₁ (swap ∘ π₂) ∘ σ₂₃) ∘ ⟨ π₁ , ((assocˡ ∘ π₂) ∘ ⟨ π₁ , ((swap ∘ π₂) ×₁ π₂ ∘ σ₂₃) ∘ assocʳ ×₁ id ⟩) ∘ (id ×₁ swap) ×₁ id ⟩ + ≈ (assocˡ ∘ π₂) ∘ ⟨ π₁ , ((swap ∘ π₂) ∘ ⟨ π₁ , (assocˡ ∘ π₂) ∘ swap ×₁ id ⟩) ∘ assocʳ ×₁ id ⟩ + eqᵢ = begin + (π₂ ×₁ (swap ∘ π₂) ∘ σ₂₃) ∘ ⟨ π₁ , ((_ ∘ π₂) ∘ ⟨ π₁ , _ ∘ _ ×₁ id ⟩) ∘ _ ×₁ id ⟩ ≈⟨ refl⟩∘⟨ ⟨⟩-congˡ (pullʳ project₂ ⟩∘⟨refl) ⟩ + (π₂ ×₁ _ ∘ σ₂₃) ∘ ⟨ π₁ , (_ ∘ ((swap ∘ π₂) ×₁ π₂ ∘ σ₂₃) ∘ _ ×₁ id) ∘ _ ×₁ id ⟩ ≈⟨ refl⟩∘⟨ ⟨⟩-congˡ ((refl⟩∘⟨ ×₁∘⟨⟩ ⟩∘⟨refl) ⟩∘⟨refl) ⟩ + _ ∘ ⟨ π₁ , (_ ∘ ⟨ (swap ∘ π₂) ∘ π₁ ×₁ π₁ , π₂ ∘ π₂ ×₁ π₂ ⟩ ∘ _ ×₁ id) ∘ _ ×₁ id ⟩ ≈⟨ refl⟩∘⟨ ⟨⟩-congˡ ((refl⟩∘⟨ ⟨⟩-cong₂ (extendˡ π₂∘×₁) π₂∘×₁ ⟩∘⟨refl) ⟩∘⟨refl) ⟩ + _ ∘ ⟨ π₁ , (_ ∘ ⟨ (swap ∘ π₁) ∘ π₂ , π₂ ∘ π₂ ⟩ ∘ assocʳ ×₁ id) ∘ _ ×₁ id ⟩ ≈⟨ refl⟩∘⟨ ⟨⟩-congˡ ((refl⟩∘⟨ pushˡ (sym ⟨⟩∘)) ⟩∘⟨refl) ⟩ + (π₂ ×₁ _ ∘ σ₂₃) ∘ ⟨ π₁ , (_ ∘ ⟨ swap ∘ π₁ , π₂ ⟩ ∘ π₂ ∘ assocʳ ×₁ id) ∘ _ ×₁ id ⟩ ≈⟨ refl⟩∘⟨ ⟨⟩-congˡ (pushˡ (refl⟩∘⟨ refl⟩∘⟨ π₂∘first)) ⟩ + (π₂ ×₁ _ ∘ σ₂₃) ∘ ⟨ π₁ , _ ∘ (⟨ swap ∘ π₁ , π₂ ⟩ ∘ π₂) ∘ _ ×₁ id ⟩ ≈⟨ refl⟩∘⟨ ⟨⟩-congˡ (refl⟩∘⟨ pullʳ π₂∘first) ⟩ + (π₂ ×₁ (swap ∘ π₂) ∘ σ₂₃) ∘ ⟨ π₁ , _ ∘ ⟨ _ ∘ π₁ , π₂ ⟩ ∘ π₂ ⟩ ≈⟨ ×₁∘⟨⟩ ⟩∘⟨refl ⟩ + ⟨ π₂ ∘ π₁ ×₁ π₁ , (swap ∘ π₂) ∘ π₂ ×₁ π₂ ⟩ ∘ ⟨ π₁ , _ ∘ ⟨ swap ∘ π₁ , π₂ ⟩ ∘ π₂ ⟩ ≈⟨ ⟨⟩-cong₂ π₂∘×₁ (extendˡ π₂∘×₁) ⟩∘⟨refl ⟩ + ⟨ π₁ ∘ π₂ , (swap ∘ π₂) ∘ π₂ ⟩ ∘ ⟨ π₁ , assocˡ ∘ ⟨ swap ∘ π₁ , π₂ ⟩ ∘ π₂ ⟩ ≈⟨ pushˡ (sym ⟨⟩∘) ⟩ + ⟨ π₁ , swap ∘ π₂ ⟩ ∘ π₂ ∘ ⟨ π₁ , assocˡ ∘ ⟨ swap ∘ π₁ , π₂ ⟩ ∘ π₂ ⟩ ≈⟨ refl⟩∘⟨ project₂ ⟩ + ⟨ π₁ , swap ∘ π₂ ⟩ ∘ assocˡ ∘ ⟨ swap ∘ π₁ , π₂ ⟩ ∘ π₂ ≈⟨ ⟨⟩-congʳ (sym identityˡ) ⟩∘⟨ pushʳ (⟨⟩-congˡ (sym identityˡ) ⟩∘⟨refl) ⟩ + id ×₁ swap ∘ (assocˡ ∘ swap ×₁ id) ∘ π₂ ≈⟨ extendʳ (hexagon₂-inv braided) ⟩ + assocˡ ∘ (swap ∘ assocˡ) ∘ π₂ ≈⟨ refl⟩∘⟨ pullʳ (pushʳ (sym π₂∘first)) ⟩ + assocˡ ∘ swap ∘ (assocˡ ∘ π₂) ∘ assocʳ ×₁ id ≈⟨ refl⟩∘⟨ refl⟩∘⟨ pushʳ (sym π₂∘first) ⟩∘⟨refl ⟩ + assocˡ ∘ swap ∘ ((assocˡ ∘ π₂) ∘ swap ×₁ id) ∘ assocʳ ×₁ id ≈⟨ refl⟩∘⟨ pullˡ (pushʳ (sym project₂)) ⟩ + assocˡ ∘ ((swap ∘ π₂) ∘ ⟨ π₁ , (assocˡ ∘ π₂) ∘ swap ×₁ id ⟩) ∘ assocʳ ×₁ id ≈⟨ pushʳ (sym project₂) ⟩ + (assocˡ ∘ π₂) ∘ ⟨ π₁ , ((_ ∘ π₂) ∘ ⟨ π₁ , (_ ∘ π₂) ∘ swap ×₁ id ⟩) ∘ _ ×₁ id ⟩ ∎ + +module Directed where + + open D using (-⊞-) + + γ : -⊞- ≃ flip-bifunctor -⊞- + γ = niHelper record + { η = uncurry swap-⧈ + ; η⁻¹ = uncurry (flip swap-⧈) + ; commute = uncurry swap-commute + ; iso = λ (X , Y) → record + { isoˡ = swap∘swap-⧈ + ; isoʳ = swap∘swap-⧈ + } + } + +module Balanced where + + open B using (-⊞-) + + γ : -⊞- ≃ flip-bifunctor -⊞- + γ = niHelper record + { η = λ (X , Y) → swap-⧈ (X □ X) (Y □ Y) + ; η⁻¹ = λ (X , Y) → swap-⧈ (Y □ Y) (X □ X) + ; commute = uncurry swap-commute + ; iso = λ (X , Y) → record + { isoˡ = swap∘swap-⧈ + ; isoʳ = swap∘swap-⧈ + } + } + +DWD-Braided : Braided DWD-Monoidal +DWD-Braided = record + { braiding = Directed.γ + ; hexagon₁ = hex₁ + ; hexagon₂ = hex₂ + } + +BWD-Braided : Braided BWD-Monoidal +BWD-Braided = record + { braiding = Balanced.γ + ; hexagon₁ = hex₁ + ; hexagon₂ = hex₂ + } diff --git a/Data/WiringDiagram/Monoidal/Core.agda b/Data/WiringDiagram/Monoidal/Core.agda new file mode 100644 index 0000000..382e188 --- /dev/null +++ b/Data/WiringDiagram/Monoidal/Core.agda @@ -0,0 +1,624 @@ +{-# 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.Core + {o ℓ e : Level} + {𝒞 : Category o ℓ e} + (S : SemiadditiveDagger 𝒞) + where + +import Categories.Category.Monoidal.Reasoning as ⊗-Reasoning +import Categories.Morphism as Morphism +import Categories.Morphism.Reasoning 𝒞 as ⇒-Reasoning +import Data.WiringDiagram.Balanced as BalancedWD +import Data.WiringDiagram.Core as WD +import Data.WiringDiagram.Directed as DirectedWD + +open import Categories.Category.Monoidal using (Monoidal) +open import Categories.Category.Monoidal.Symmetric using (module Symmetric) +open import Categories.Category.Monoidal.Utilities using (pentagon-inv) +open import Categories.Functor.Bifunctor using (Bifunctor) +open import Categories.Object.Initial using (Initial; IsInitial) +open import Data.Product using (_,_; uncurry′) + +open SemiadditiveDagger S + +open BalancedWD S using (BWD) +open Category 𝒞 +open DirectedWD S using (DWD) +open Monoidal monoidal using (triangle; pentagon) +open Symmetric symmetric using (braided) +open WD S using (Box; WiringDiagram; _□_; _⧈_; _≈-⧈_; _⌸_; id-⧈; _⌻_; ≈-sym) + +module DWD = Category DWD + +-- Swap middle two of four + +σ₂₃ : {A B C D : Obj} → (A ⊕ B) ⊕ (C ⊕ D) ⇒ (A ⊕ C) ⊕ (B ⊕ D) +σ₂₃ = ⟨ π₁ ×₁ π₁ , π₂ ×₁ π₂ ⟩ + +-- Monoidal unit and initial object + +𝟘-□ : Box +𝟘-□ = 𝟘 □ 𝟘 + +-- Wiring diagram from the initial box to any box + +¡-⧈ : {A : Box} → WiringDiagram 𝟘-□ A +¡-⧈ {A} = ! WD.⧈ ¡ + +-- Monoidal products of boxes and wiring diagrams + +_⊞_ : 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) +(fᵢ ⧈ fₒ) ⊞₁ (gᵢ ⧈ gₒ) = fᵢ ×₁ gᵢ ∘ σ₂₃ ⧈ fₒ ×₁ gₒ + +infixr 10 _⊞_ _⊞₁_ + +-- Left and right unitor wiring diagrams + +unitorˡ⇒ : {X : Box} → WiringDiagram (𝟘-□ ⊞ X) X +unitorˡ⇒ = i₂ ∘ π₂ ⧈ π₂ + +unitorˡ⇐ : {X : Box} → WiringDiagram X (𝟘-□ ⊞ X) +unitorˡ⇐ = π₂ ∘ π₂ ⧈ i₂ + +unitorʳ⇒ : {X : Box} → WiringDiagram (X ⊞ 𝟘-□) X +unitorʳ⇒ = i₁ ∘ π₂ ⧈ π₁ + +unitorʳ⇐ : {X : Box} → WiringDiagram X (X ⊞ 𝟘-□) +unitorʳ⇐ = π₁ ∘ π₂ ⧈ i₁ + +-- Associator wiring diagrams + +associator⇒ + : {X Y Z : Box} + → WiringDiagram ((X ⊞ Y) ⊞ Z) (X ⊞ (Y ⊞ Z)) +associator⇒ = assocʳ ∘ π₂ ⧈ assocˡ + +associator⇐ + : {X Y Z : Box} + → WiringDiagram (X ⊞ (Y ⊞ Z)) ((X ⊞ Y) ⊞ Z) +associator⇐ = assocˡ ∘ π₂ ⧈ assocʳ + +-- Properties + +open HomReasoning +open ⇒-Reasoning +open Equiv + +¡-⧈-unique : {A : Box} (f : WiringDiagram 𝟘-□ A) → ¡-⧈ ≈-⧈ f +¡-⧈-unique (fᵢ ⧈ fₒ) = !-unique fᵢ ⌸ ¡-unique fₒ + +⊞-identity : {A B : Box} → id-⧈ {A} ⊞₁ id-⧈ {B} ≈-⧈ id-⧈ +⊞-identity = eqᵢ ⌸ id×₁id + where + 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 ⟩ ∘ ⟨ π₁ ×₁ π₁ , π₂ ×₁ π₂ ⟩ ∎ + +σ₂₃-×₁ + : {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) +σ₂₃-×₁ {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) ∎ + +⊞-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ʳ σ₂₃-×₁ ⟩ + (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ˡ σ₂₃-×₁ ⟩ + (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ʳ σ₂₃-×₁) ⟩ + (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ₒ + +λ-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 + eqᵢ : (π₂ ∘ π₂) ∘ ⟨ π₁ , (i₂ ∘ π₂) ∘ i₂ ×₁ id ⟩ ≈ π₂ + eqᵢ = begin + (π₂ ∘ π₂) ∘ ⟨ π₁ , (i₂ ∘ π₂) ∘ i₂ ×₁ id ⟩ ≈⟨ pullʳ project₂ ⟩ + π₂ ∘ (i₂ ∘ π₂) ∘ i₂ ×₁ id ≈⟨ refl⟩∘⟨ pullʳ π₂∘first ⟩ + π₂ ∘ i₂ ∘ π₂ ≈⟨ cancelˡ π₂∘i₂≈id ⟩ + π₂ ∎ + +ρ-isoˡ : {X : Box} → unitorʳ⇐ ⌻ unitorʳ⇒ ≈-⧈ DWD.id {X ⊞ 𝟘-□} +ρ-isoˡ = eqᵢ ⌸ i₁∘π₁≈id + where + 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 + eqᵢ : (π₁ ∘ π₂) ∘ ⟨ π₁ , (i₁ ∘ π₂) ∘ i₁ ×₁ id ⟩ ≈ π₂ + eqᵢ = begin + (π₁ ∘ π₂) ∘ ⟨ π₁ , (i₁ ∘ π₂) ∘ i₁ ×₁ id ⟩ ≈⟨ pullʳ project₂ ⟩ + π₁ ∘ (i₁ ∘ π₂) ∘ i₁ ×₁ id ≈⟨ refl⟩∘⟨ pullʳ π₂∘first ⟩ + π₁ ∘ i₁ ∘ π₂ ≈⟨ cancelˡ π₁∘i₁≈id ⟩ + π₂ ∎ + +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 + 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 + 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 + 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 + 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₁ ∎ + +α-isoˡ : {X Y Z : Box} → associator⇐ {X} {Y} {Z} ⌻ associator⇒ ≈-⧈ DWD.id +α-isoˡ {X} {Y} {Z} = eqᵢ ⌸ assocʳ∘assocˡ + where + 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 + 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-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 + 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 + 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 + 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 + 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 ⟩ ∎ + +module Directed where + + open Morphism DWD using (_≅_) + + -⊞- : Bifunctor DWD DWD DWD + -⊞- = record + { F₀ = uncurry′ _⊞_ + ; F₁ = uncurry′ _⊞₁_ + ; identity = ⊞-identity + ; homomorphism = ⊞-homo + ; F-resp-≈ = uncurry′ ⊞-resp-≈-⧈ + } + + unitorˡ : {X : Box} → 𝟘-□ ⊞ X ≅ X + unitorˡ {X} = record + { from = unitorˡ⇒ + ; to = unitorˡ⇐ + ; iso = record + { isoˡ = λ-isoˡ + ; isoʳ = λ-isoʳ + } + } + + unitorʳ : {X : Box} → X ⊞ 𝟘-□ ≅ X + unitorʳ {X} = record + { from = unitorʳ⇒ + ; to = unitorʳ⇐ + ; iso = record + { isoˡ = ρ-isoˡ + ; isoʳ = ρ-isoʳ + } + } + + associator : {X Y Z : Box} → (X ⊞ Y) ⊞ Z ≅ X ⊞ (Y ⊞ Z) + associator = record + { from = associator⇒ + ; to = associator⇐ + ; iso = record + { isoˡ = α-isoˡ + ; isoʳ = α-isoʳ + } + } + + 𝟘-□-isInitial : IsInitial DWD 𝟘-□ + 𝟘-□-isInitial = record + { ¡ = ¡-⧈ + ; ¡-unique = ¡-⧈-unique + } + +module Balanced where + + open Morphism BWD using (_≅_) + + -⊞- : Bifunctor BWD BWD BWD + -⊞- = record + { F₀ = uncurry′ _⊕_ + ; F₁ = uncurry′ _⊞₁_ + ; identity = ⊞-identity + ; homomorphism = ⊞-homo + ; F-resp-≈ = uncurry′ ⊞-resp-≈-⧈ + } + + unitorˡ : {X : Obj} → 𝟘 ⊕ X ≅ X + unitorˡ {X} = record + { from = unitorˡ⇒ + ; to = unitorˡ⇐ + ; iso = record + { isoˡ = λ-isoˡ + ; isoʳ = λ-isoʳ + } + } + + unitorʳ : {X : Obj} → X ⊕ 𝟘 ≅ X + unitorʳ {X} = record + { from = unitorʳ⇒ + ; to = unitorʳ⇐ + ; iso = record + { isoˡ = ρ-isoˡ + ; isoʳ = ρ-isoʳ + } + } + + associator : {X Y Z : Obj} → (X ⊕ Y) ⊕ Z ≅ X ⊕ (Y ⊕ Z) + associator = record + { from = associator⇒ + ; to = associator⇐ + ; iso = record + { isoˡ = α-isoˡ + ; isoʳ = α-isoʳ + } + } + + 𝟘-isInitial : IsInitial BWD 𝟘 + 𝟘-isInitial = record + { ¡ = ¡-⧈ + ; ¡-unique = ¡-⧈-unique + } + +DWD-Initial : Initial DWD +DWD-Initial = record + { ⊥ = 𝟘-□ + ; ⊥-is-initial = Directed.𝟘-□-isInitial + } + +BWD-Initial : Initial BWD +BWD-Initial = record + { ⊥ = 𝟘 + ; ⊥-is-initial = Balanced.𝟘-isInitial + } + +DWD-Monoidal : Monoidal DWD +DWD-Monoidal = record + { ⊗ = Directed.-⊞- + ; unit = 𝟘-□ + ; unitorˡ = Directed.unitorˡ + ; unitorʳ = Directed.unitorʳ + ; associator = Directed.associator + ; unitorˡ-commute-from = unitorˡ-commute-from + ; unitorˡ-commute-to = unitorˡ-commute-to + ; unitorʳ-commute-from = unitorʳ-commute-from + ; unitorʳ-commute-to = unitorʳ-commute-to + ; assoc-commute-from = ≈-sym associator-commute-from + ; assoc-commute-to = ≈-sym associator-commute-to + ; triangle = tri + ; pentagon = pent + } + +BWD-Monoidal : Monoidal BWD +BWD-Monoidal = record + { ⊗ = Balanced.-⊞- + ; unit = 𝟘 + ; unitorˡ = Balanced.unitorˡ + ; unitorʳ = Balanced.unitorʳ + ; associator = Balanced.associator + ; unitorˡ-commute-from = unitorˡ-commute-from + ; unitorˡ-commute-to = unitorˡ-commute-to + ; unitorʳ-commute-from = unitorʳ-commute-from + ; unitorʳ-commute-to = unitorʳ-commute-to + ; assoc-commute-from = ≈-sym associator-commute-from + ; assoc-commute-to = ≈-sym associator-commute-to + ; triangle = tri + ; pentagon = pent + } |