Construct monoidal merge functor

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