diff options
Diffstat (limited to 'Data/WiringDiagram/Monoidal.agda')
| -rw-r--r-- | Data/WiringDiagram/Monoidal.agda | 26 |
1 files changed, 22 insertions, 4 deletions
diff --git a/Data/WiringDiagram/Monoidal.agda b/Data/WiringDiagram/Monoidal.agda index 96ff101..25702e7 100644 --- a/Data/WiringDiagram/Monoidal.agda +++ b/Data/WiringDiagram/Monoidal.agda @@ -25,7 +25,7 @@ open import Categories.Morphism.Properties using (id-iso) open import Categories.NaturalTransformation.NaturalIsomorphism using (_≃_; niHelper) open import Data.Product using (_,_; zip) open import Data.WiringDiagram.Balanced S using (BWD; Push; Pull) -open import Data.WiringDiagram.Core S using (_□_; _⧈_; id-⧈; _≈-⧈_; _⌸_; _⌻_) +open import Data.WiringDiagram.Core S using (_□_; _⧈_; id-⧈; _≈-⧈_; _⌸_; _⌻_; loop) 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 @@ -207,33 +207,48 @@ module BalancedPush where open BWD.HomReasoning open ⇒-Reasoning BWD + Push-assoc + : {A B C : Obj} + → Push.₁ (assocˡ {A} {B} {C}) ≈-⧈ associator⇒ + Push-assoc = ∘-resp-≈ˡ α⇒† ⌸ refl + associativity : {A B C : Obj} → Push.₁ (assocˡ {A} {B} {C}) ⌻ id-⧈ ⌻ id-⧈ ⊞₁ id-⧈ ≈-⧈ id-⧈ ⌻ id-⧈ ⊞₁ id-⧈ ⌻ associator⇒ associativity = begin Push.₁ assocˡ ⌻ id-⧈ ⌻ id-⧈ ⊞₁ id-⧈ ≈⟨ elimʳ (elimʳ ⊞-identity) ⟩ - Push.₁ assocˡ ≈⟨ ∘-resp-≈ˡ α⇒† ⌸ refl ⟩ + Push.₁ assocˡ ≈⟨ Push-assoc ⟩ assocʳ ∘ π₂ ⧈ assocˡ ≈⟨ introˡ ⊞-identity ⟩ id-⧈ ⊞₁ id-⧈ ⌻ associator⇒ ≈⟨ BWD.identityˡ ⟨ id-⧈ ⌻ id-⧈ ⊞₁ id-⧈ ⌻ associator⇒ ∎ + Push-π₂ + : {A : Obj} + → Push.₁ (π₂ {𝟘} {A}) ≈-⧈ unitorˡ⇒ + Push-π₂ = ∘-resp-≈ˡ π₂† ⌸ refl + unitaryˡ : {A : Obj} → Push.₁ (π₂ {𝟘} {A}) ⌻ id-⧈ ⌻ id-⧈ ⊞₁ id-⧈ ≈-⧈ unitorˡ⇒ unitaryˡ = begin Push.₁ π₂ ⌻ id-⧈ ⌻ id-⧈ ⊞₁ id-⧈ ≈⟨ elimʳ (elimʳ ⊞-identity) ⟩ - Push.₁ π₂ ≈⟨ ∘-resp-≈ˡ π₂† ⌸ refl ⟩ + Push.₁ π₂ ≈⟨ Push-π₂ ⟩ unitorˡ⇒ ∎ + Push-π₁ + : {A : Obj} + → Push.₁ (π₁ {A} {𝟘}) ≈-⧈ unitorʳ⇒ + Push-π₁ = ∘-resp-≈ˡ π₁† ⌸ refl + unitaryʳ : {A : Obj} → Push.₁ (π₁ {A} {𝟘}) ⌻ id-⧈ ⌻ id-⧈ ⊞₁ id-⧈ ≈-⧈ unitorʳ⇒ unitaryʳ = begin Push.₁ π₁ ⌻ id-⧈ ⌻ id-⧈ ⊞₁ id-⧈ ≈⟨ elimʳ (elimʳ ⊞-identity) ⟩ - Push.₁ π₁ ≈⟨ ∘-resp-≈ˡ π₁† ⌸ refl ⟩ + Push.₁ π₁ ≈⟨ Push-π₁ ⟩ unitorʳ⇒ ∎ braiding-compat @@ -391,3 +406,6 @@ Pull-SMF = record ; braiding-compat = BalancedPull.braiding-compat } } + +loop⊞loop : {A B : Obj} → loop {A} ⊞₁ loop {B} ≈-⧈ loop +loop⊞loop = sym S.∇-⊕ ⌸ id×₁id |