diff options
Diffstat (limited to 'Data')
| -rw-r--r-- | Data/WiringDiagram/Monoidal.agda | 38 | ||||
| -rw-r--r-- | Data/WiringDiagram/Monoidal/Braided.agda | 19 | ||||
| -rw-r--r-- | Data/WiringDiagram/Monoidal/Core.agda | 24 |
3 files changed, 22 insertions, 59 deletions
diff --git a/Data/WiringDiagram/Monoidal.agda b/Data/WiringDiagram/Monoidal.agda index 3d7ea78..96ff101 100644 --- a/Data/WiringDiagram/Monoidal.agda +++ b/Data/WiringDiagram/Monoidal.agda @@ -28,7 +28,7 @@ open import Data.WiringDiagram.Balanced S using (BWD; Push; Pull) open import Data.WiringDiagram.Core S using (_□_; _⧈_; id-⧈; _≈-⧈_; _⌸_; _⌻_) open import Data.WiringDiagram.Directed S using (DWD; Pulsh) open import Data.WiringDiagram.Monoidal.Braided S using (swap-⧈; DWD-Braided) public -open import Data.WiringDiagram.Monoidal.Core S using (DWD-Monoidal; BWD-Monoidal; _⊞_; _⊞₁_; σ₂₃; associator⇒; unitorˡ⇒; unitorʳ⇒; ⊞-identity) public +open import Data.WiringDiagram.Monoidal.Core S using (DWD-Monoidal; BWD-Monoidal; _⊞_; _⊞₁_; associator⇒; unitorˡ⇒; unitorʳ⇒; ⊞-identity) public open import Data.WiringDiagram.Monoidal.Symmetric S using (DWD-Symmetric; BWD-Symmetric) public module DWD = Category DWD @@ -141,23 +141,19 @@ module Directed where unitaryˡ : {A B : Obj} - → Pulsh.₁ (⟨ ! {A} , id {A} ⟩ , π₂ {𝟘} {B}) ⌻ id-⧈ ⌻ id-⧈ ⊞₁ id-⧈ + → Pulsh.₁ (i₂ {𝟘} {A} , π₂ {𝟘} {B}) ⌻ id-⧈ ⌻ id-⧈ ⊞₁ id-⧈ ≈-⧈ unitorˡ⇒ unitaryˡ = begin - Pulsh.₁ (⟨ ! , id ⟩ , π₂) ⌻ id-⧈ ⌻ id-⧈ ⊞₁ id-⧈ ≈⟨ elimʳ (elimʳ ⊞-identity) ⟩ - Pulsh.₁ (⟨ ! , id ⟩ , π₂) ≈⟨ Pulsh.F-resp-≈ (⟨⟩-congʳ (!-unique zero⇒) , refl) ⟩ - Pulsh.₁ (⟨ zero⇒ , id ⟩ , π₂) ≈⟨ Pulsh.F-resp-≈ (⟨⟩-unique π₁∘i₂≈0 π₂∘i₂≈id , refl) ⟩ - unitorˡ⇒ ∎ + Pulsh.₁ (i₂ , π₂) ⌻ id-⧈ ⌻ id-⧈ ⊞₁ id-⧈ ≈⟨ elimʳ (elimʳ ⊞-identity) ⟩ + unitorˡ⇒ ∎ unitaryʳ : {A B : Obj} - → Pulsh.₁ (⟨ id {A} , ! {A} ⟩ , π₁ {B} {𝟘}) ⌻ id-⧈ ⌻ id-⧈ ⊞₁ id-⧈ + → Pulsh.₁ (i₁ {A} {𝟘} , π₁ {B} {𝟘}) ⌻ id-⧈ ⌻ id-⧈ ⊞₁ id-⧈ ≈-⧈ unitorʳ⇒ unitaryʳ = begin - Pulsh.₁ (⟨ id , ! ⟩ , π₁) ⌻ id-⧈ ⌻ id-⧈ ⊞₁ id-⧈ ≈⟨ elimʳ (elimʳ ⊞-identity) ⟩ - Pulsh.₁ (⟨ id , ! ⟩ , π₁) ≈⟨ Pulsh.F-resp-≈ (⟨⟩-congˡ (!-unique zero⇒) , refl) ⟩ - Pulsh.₁ (⟨ id , zero⇒ ⟩ , π₁) ≈⟨ Pulsh.F-resp-≈ (⟨⟩-unique π₁∘i₁≈id π₂∘i₁≈0 , refl) ⟩ - unitorʳ⇒ ∎ + Pulsh.₁ (i₁ , π₁) ⌻ id-⧈ ⌻ id-⧈ ⊞₁ id-⧈ ≈⟨ elimʳ (elimʳ ⊞-identity) ⟩ + unitorʳ⇒ ∎ braiding-compat : {A B C D : Obj} @@ -302,25 +298,21 @@ module BalancedPull where unitaryˡ : {A : Obj} - → Pull.₁ ⟨ ! {A} , id {A} ⟩ ⌻ id-⧈ ⌻ id-⧈ ⊞₁ id-⧈ + → Pull.₁ (i₂ {𝟘} {A}) ⌻ id-⧈ ⌻ id-⧈ ⊞₁ id-⧈ ≈-⧈ unitorˡ⇒ unitaryˡ = begin - Pull.₁ ⟨ ! , id ⟩ ⌻ id-⧈ ⌻ id-⧈ ⊞₁ id-⧈ ≈⟨ elimʳ (elimʳ ⊞-identity) ⟩ - Pull.₁ ⟨ ! , id ⟩ ≈⟨ Pull.F-resp-≈ (⟨⟩-congʳ (!-unique zero⇒)) ⟩ - Pull.₁ ⟨ zero⇒ , id ⟩ ≈⟨ Pull.F-resp-≈ (⟨⟩-unique π₁∘i₂≈0 π₂∘i₂≈id) ⟩ - Pull.₁ i₂ ≈⟨ refl ⌸ i₂† ⟩ - unitorˡ⇒ ∎ + Pull.₁ i₂ ⌻ id-⧈ ⌻ id-⧈ ⊞₁ id-⧈ ≈⟨ elimʳ (elimʳ ⊞-identity) ⟩ + Pull.₁ i₂ ≈⟨ refl ⌸ i₂† ⟩ + unitorˡ⇒ ∎ unitaryʳ : {A : Obj} - → Pull.₁ ⟨ id {A} , ! {A} ⟩ ⌻ id-⧈ ⌻ id-⧈ ⊞₁ id-⧈ + → Pull.₁ (i₁ {A} {𝟘}) ⌻ id-⧈ ⌻ id-⧈ ⊞₁ id-⧈ ≈-⧈ unitorʳ⇒ unitaryʳ = begin - Pull.₁ ⟨ id , ! ⟩ ⌻ id-⧈ ⌻ id-⧈ ⊞₁ id-⧈ ≈⟨ elimʳ (elimʳ ⊞-identity) ⟩ - Pull.₁ ⟨ id , ! ⟩ ≈⟨ Pull.F-resp-≈ (⟨⟩-congˡ (!-unique zero⇒)) ⟩ - Pull.₁ ⟨ id , zero⇒ ⟩ ≈⟨ Pull.F-resp-≈ (⟨⟩-unique π₁∘i₁≈id π₂∘i₁≈0) ⟩ - Pull.₁ i₁ ≈⟨ refl ⌸ i₁† ⟩ - unitorʳ⇒ ∎ + Pull.₁ i₁ ⌻ id-⧈ ⌻ id-⧈ ⊞₁ id-⧈ ≈⟨ elimʳ (elimʳ ⊞-identity) ⟩ + Pull.₁ i₁ ≈⟨ refl ⌸ i₁† ⟩ + unitorʳ⇒ ∎ braiding-compat : {A B : Obj} diff --git a/Data/WiringDiagram/Monoidal/Braided.agda b/Data/WiringDiagram/Monoidal/Braided.agda index 7b28d85..d45d8d2 100644 --- a/Data/WiringDiagram/Monoidal/Braided.agda +++ b/Data/WiringDiagram/Monoidal/Braided.agda @@ -11,6 +11,7 @@ module Data.WiringDiagram.Monoidal.Braided where import Categories.Morphism.Reasoning 𝒞 as ⇒-Reasoning +import Category.Semiadditive.Monoidal as SemiadditiveMonoidal import Data.WiringDiagram.Core as WD open import Categories.Category.Monoidal using (Monoidal) @@ -21,12 +22,15 @@ 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) + 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 SemiadditiveMonoidal semiadditive using (symmetric) + open Symmetric symmetric using (braided; hexagon₁; hexagon₂) open WD S using (Box; WiringDiagram; _□_; _⧈_; _≈-⧈_; _⌸_; id-⧈; _⌻_; ≈-sym) @@ -34,19 +38,6 @@ 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 diff --git a/Data/WiringDiagram/Monoidal/Core.agda b/Data/WiringDiagram/Monoidal/Core.agda index 5abd60f..daed109 100644 --- a/Data/WiringDiagram/Monoidal/Core.agda +++ b/Data/WiringDiagram/Monoidal/Core.agda @@ -13,33 +13,28 @@ module Data.WiringDiagram.Monoidal.Core import Categories.Category.Monoidal.Reasoning as ⊗-Reasoning import Categories.Morphism as Morphism import Categories.Morphism.Reasoning 𝒞 as ⇒-Reasoning +import Category.Semiadditive.Monoidal as SemiadditiveMonoidal 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 SemiadditiveMonoidal semiadditive using (monoidal) 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 @@ -123,21 +118,6 @@ open Equiv ⟨ ⟨ π₁ , 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} |