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