diff options
Diffstat (limited to 'Data/WiringDiagram/Monoidal/Braided.agda')
| -rw-r--r-- | Data/WiringDiagram/Monoidal/Braided.agda | 182 |
1 files changed, 182 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₂ + } |