diff options
Diffstat (limited to 'Data/WiringDiagram')
| -rw-r--r-- | Data/WiringDiagram/Equalities.agda | 5 | ||||
| -rw-r--r-- | Data/WiringDiagram/Monoidal.agda | 43 |
2 files changed, 38 insertions, 10 deletions
diff --git a/Data/WiringDiagram/Equalities.agda b/Data/WiringDiagram/Equalities.agda index 61deee4..1c3928e 100644 --- a/Data/WiringDiagram/Equalities.agda +++ b/Data/WiringDiagram/Equalities.agda @@ -12,7 +12,7 @@ import Categories.Morphism.Reasoning 𝒞 as ⇒-Reasoning open import Categories.Category.Monoidal using (module Monoidal) open import Categories.Category.Monoidal.Utilities using (module Shorthands) -open import Data.WiringDiagram.Core S.semiadditiveDagger using (_⌸_; _⌻_; _≈-⧈_; ≈-trans; loop; push; pull; merge; split) +open import Data.WiringDiagram.Core S.semiadditiveDagger using (_⌸_; _⌻_; _≈-⧈_; id-⧈; ≈-trans; loop; push; pull; merge; split) open Category 𝒞 @@ -112,3 +112,6 @@ loop∘push∘loop f id≤f†∘f = ≈-trans (loop∘push∘loop≈merge f id loop∘pull∘loop : {A B : Obj} → (f : A ⇒ B) → (f ∘ (f †)) ≤ id → loop ⌻ pull f ⌻ loop ≈-⧈ pull f ⌻ loop loop∘pull∘loop f f∘f†≤id = ≈-trans (loop∘pull∘loop≈split f f∘f†≤id) (split≈pull∘loop f) + +loop-𝟘 : loop {𝟘} ≈-⧈ id-⧈ +loop-𝟘 = []-unique !-unique₂ π₂∘i₂≈id ⌸ refl diff --git a/Data/WiringDiagram/Monoidal.agda b/Data/WiringDiagram/Monoidal.agda index 25702e7..d3a6526 100644 --- a/Data/WiringDiagram/Monoidal.agda +++ b/Data/WiringDiagram/Monoidal.agda @@ -189,10 +189,10 @@ module BalancedPush where (g : C ⇒ D) → id-⧈ ⌻ Push.₁ f ⊞₁ Push.₁ g ≈-⧈ Push.₁ (f ×₁ g) ⌻ id-⧈ commute f g = begin - id-⧈ ⌻ Push.₁ f ⊞₁ Push.₁ g ≈⟨ DWD.identityˡ ⟩ - Push.₁ f ⊞₁ Push.₁ g ≈⟨ Push-⊞₁ f g ⟩ - Push.₁ (f ×₁ g) ≈⟨ DWD.identityʳ ⟨ - Push.₁ (f ×₁ g) ⌻ id-⧈ ∎ + id-⧈ ⌻ Push.₁ f ⊞₁ Push.₁ g ≈⟨ DWD.identityˡ ⟩ + Push.₁ f ⊞₁ Push.₁ g ≈⟨ Push-⊞₁ f g ⟩ + Push.₁ (f ×₁ g) ≈⟨ DWD.identityʳ ⟨ + Push.₁ (f ×₁ g) ⌻ id-⧈ ∎ where open DWD.HomReasoning @@ -251,11 +251,16 @@ module BalancedPush where Push.₁ π₁ ≈⟨ Push-π₁ ⟩ unitorʳ⇒ ∎ + Push-swap + : {A B : Obj} + → Push.₁ swap ≈-⧈ swap-⧈ (A □ A) (B □ B) + Push-swap = ∘-resp-≈ˡ swap† ⌸ refl + braiding-compat : {A B : Obj} → Push.₁ (swap {A} {B}) ⌻ id-⧈ ≈-⧈ id-⧈ ⌻ swap-⧈ (A □ A) (B □ B) - braiding-compat = BWD.identityʳ ○ ∘-resp-≈ˡ swap† ⌸ refl ○ BWD.Equiv.sym BWD.identityˡ + braiding-compat = BWD.identityʳ ○ Push-swap ○ BWD.Equiv.sym BWD.identityˡ module BalancedPull where @@ -300,40 +305,60 @@ module BalancedPull where open BWD.HomReasoning open ⇒-Reasoning BWD + Pull-assoc + : {A B C : Obj} + → Pull.₁ (assocʳ {A} {B} {C}) ≈-⧈ associator⇒ + Pull-assoc = refl ⌸ α⇐† + associativity : {A B C : Obj} → Pull.₁ (assocʳ {A} {B} {C}) ⌻ id-⧈ ⌻ id-⧈ ⊞₁ id-⧈ ≈-⧈ id-⧈ ⌻ id-⧈ ⊞₁ id-⧈ ⌻ associator⇒ associativity = begin Pull.₁ assocʳ ⌻ id-⧈ ⌻ id-⧈ ⊞₁ id-⧈ ≈⟨ elimʳ (elimʳ ⊞-identity) ⟩ - Pull.₁ assocʳ ≈⟨ refl ⌸ α⇐† ⟩ + Pull.₁ assocʳ ≈⟨ Pull-assoc ⟩ assocʳ ∘ π₂ ⧈ assocˡ ≈⟨ introˡ ⊞-identity ⟩ id-⧈ ⊞₁ id-⧈ ⌻ associator⇒ ≈⟨ BWD.identityˡ ⟨ id-⧈ ⌻ id-⧈ ⊞₁ id-⧈ ⌻ associator⇒ ∎ + Pull-i₂ + : {A : Obj} + → Pull.₁ (i₂ {𝟘} {A}) ≈-⧈ unitorˡ⇒ + Pull-i₂ = refl ⌸ i₂† + unitaryˡ : {A : Obj} → Pull.₁ (i₂ {𝟘} {A}) ⌻ id-⧈ ⌻ id-⧈ ⊞₁ id-⧈ ≈-⧈ unitorˡ⇒ unitaryˡ = begin Pull.₁ i₂ ⌻ id-⧈ ⌻ id-⧈ ⊞₁ id-⧈ ≈⟨ elimʳ (elimʳ ⊞-identity) ⟩ - Pull.₁ i₂ ≈⟨ refl ⌸ i₂† ⟩ + Pull.₁ i₂ ≈⟨ Pull-i₂ ⟩ unitorˡ⇒ ∎ + Pull-i₁ + : {A : Obj} + → Pull.₁ (i₁ {A} {𝟘}) ≈-⧈ unitorʳ⇒ + Pull-i₁ = refl ⌸ i₁† + unitaryʳ : {A : Obj} → Pull.₁ (i₁ {A} {𝟘}) ⌻ id-⧈ ⌻ id-⧈ ⊞₁ id-⧈ ≈-⧈ unitorʳ⇒ unitaryʳ = begin Pull.₁ i₁ ⌻ id-⧈ ⌻ id-⧈ ⊞₁ id-⧈ ≈⟨ elimʳ (elimʳ ⊞-identity) ⟩ - Pull.₁ i₁ ≈⟨ refl ⌸ i₁† ⟩ + Pull.₁ i₁ ≈⟨ Pull-i₁ ⟩ unitorʳ⇒ ∎ + Pull-swap + : {A B : Obj} + → Pull.₁ swap ≈-⧈ swap-⧈ (A □ A) (B □ B) + Pull-swap = refl ⌸ swap† + braiding-compat : {A B : Obj} → Pull.₁ (swap {A} {B}) ⌻ id-⧈ ≈-⧈ id-⧈ ⌻ swap-⧈ (B □ B) (A □ A) - braiding-compat = BWD.identityʳ ○ refl ⌸ swap† ○ BWD.Equiv.sym BWD.identityˡ + braiding-compat = BWD.identityʳ ○ Pull-swap ○ BWD.Equiv.sym BWD.identityˡ Pulsh-IsMF : IsStrongMonoidalFunctor (S-MC.op ×-⊗ S-MC) DWD-MC Pulsh Pulsh-IsMF = record |