1 files changed, 34 insertions, 9 deletions
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