Upgrade Push + Pull to symmetric monoidal functorsmain

1 files changed, 401 insertions, 0 deletions

diff --git a/Data/WiringDiagram/Monoidal.agda b/Data/WiringDiagram/Monoidal.agda
new file mode 100644
index 0000000..3d7ea78
--- /dev/null
+++ b/Data/WiringDiagram/Monoidal.agda
@@ -0,0 +1,401 @@
+{-# OPTIONS --without-K --safe #-}
+{-# OPTIONS --lossy-unification #-}
+
+open import Categories.Category using (Category)
+open import Category.Dagger.Semiadditive using (SemiadditiveDagger)
+open import Level using (Level)
+
+module Data.WiringDiagram.Monoidal
+    {o ℓ e : Level}
+    {𝒞 : Category o ℓ e}
+    (S : SemiadditiveDagger 𝒞)
+  where
+
+import Categories.Morphism.Reasoning as ⇒-Reasoning
+
+open import Categories.Category.Monoidal.Bundle using (MonoidalCategory; SymmetricMonoidalCategory)
+open import Categories.Category.Monoidal.Construction.Product using () renaming (Product-MonoidalCategory to _×-⊗_)
+open import Categories.Category.Monoidal.Construction.Product using () renaming (Product-SymmetricMonoidalCategory to _×-σ⊗_)
+open import Categories.Category.Product using (_⁂_)
+open import Categories.Functor using (Functor; _∘F_)
+open import Categories.Functor.Monoidal using (IsStrongMonoidalFunctor; StrongMonoidalFunctor)
+open import Categories.Functor.Monoidal.Symmetric using (module Strong)
+open import Categories.Morphism using (module ≅)
+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.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.Symmetric S using (DWD-Symmetric; BWD-Symmetric) public
+
+module DWD = Category DWD
+module BWD = Category BWD
+module Pulsh = Functor Pulsh
+module Push = Functor Push
+module Pull = Functor Pull
+module S = SemiadditiveDagger S
+
+open Category 𝒞 hiding (op)
+open Equiv using (refl; sym)
+open S
+
+DWD-MC : MonoidalCategory o ℓ e
+DWD-MC = record
+    { U = DWD
+    ; monoidal = DWD-Monoidal
+    }
+
+DWD-SMC : SymmetricMonoidalCategory o ℓ e
+DWD-SMC = record
+    { U = DWD
+    ; monoidal = DWD-Monoidal
+    ; symmetric = DWD-Symmetric
+    }
+
+BWD-MC : MonoidalCategory o ℓ e
+BWD-MC = record
+    { U = BWD
+    ; monoidal = BWD-Monoidal
+    }
+
+BWD-SMC : SymmetricMonoidalCategory o ℓ e
+BWD-SMC = record
+    { U = BWD
+    ; monoidal = BWD-Monoidal
+    ; symmetric = BWD-Symmetric
+    }
+
+module DWD-MC = MonoidalCategory DWD-MC
+module DWD-SMC = SymmetricMonoidalCategory DWD-SMC
+module BWD-MC = MonoidalCategory BWD-MC
+module BWD-SMC = SymmetricMonoidalCategory BWD-SMC
+
+S-MC : MonoidalCategory o ℓ e
+S-MC = S.monoidalCategory
+
+S-SMC : SymmetricMonoidalCategory o ℓ e
+S-SMC = S.symmetricMonoidalCategory
+
+module S-MC = MonoidalCategory S-MC
+module S-SMC = SymmetricMonoidalCategory S-SMC
+
+module Directed where
+
+  Pulsh-⊞₁
+      : {A A′ B B′ C C′ D D′ : Obj}
+        (f : A′ ⇒ A)
+        (g : B ⇒ B′)
+        (h : C′ ⇒ C)
+        (i : D ⇒ D′)
+      → Pulsh.₁ (f , g) ⊞₁ Pulsh.₁ (h , i) ≈-⧈ Pulsh.₁ (f ×₁ h , g ×₁ i)
+  Pulsh-⊞₁ f g h i = eqᵢ ⌸ refl
+    where
+      open HomReasoning
+      open ⇒-Reasoning 𝒞
+      eqᵢ : (f ∘ π₂) ×₁ (h ∘ π₂) ∘ σ₂₃ ≈ f ×₁ h ∘ π₂
+      eqᵢ = begin
+          (f ∘ π₂) ×₁ (h ∘ π₂) ∘ σ₂₃                  ≈⟨ pushˡ (sym ×₁∘×₁) ⟩
+          f ×₁ h ∘ π₂ ×₁ π₂ ∘ σ₂₃                     ≈⟨ refl⟩∘⟨ ×₁∘⟨⟩ ⟩
+          f ×₁ h ∘ ⟨ π₂ ∘ π₁ ×₁ π₁ , π₂ ∘ π₂ ×₁ π₂ ⟩  ≈⟨ refl⟩∘⟨ ⟨⟩-cong₂ π₂∘×₁ π₂∘×₁ ⟩
+          f ×₁ h ∘ ⟨ π₁ ∘ π₂ , π₂ ∘ π₂ ⟩              ≈⟨ refl⟩∘⟨ g-η ⟩
+          f ×₁ h ∘ π₂                                 ∎
+
+  commute
+      : {A A′ B B′ C C′ D D′ : Obj}
+        (f : A′ ⇒ A)
+        (g : B ⇒ B′)
+        (h : C′ ⇒ C)
+        (i : D ⇒ D′)
+      → id-⧈ ⌻ Pulsh.₁ (f , g) ⊞₁ Pulsh.₁ (h , i) ≈-⧈ Pulsh.₁ (f ×₁ h , g ×₁ i) ⌻ id-⧈
+  commute f g h i = begin
+      id-⧈ ⌻ Pulsh.₁ (f , g) ⊞₁ Pulsh.₁ (h , i) ≈⟨ DWD.identityˡ ⟩
+      Pulsh.₁ (f , g) ⊞₁ Pulsh.₁ (h , i)        ≈⟨ Pulsh-⊞₁ f g h i ⟩
+      Pulsh.₁ (f ×₁ h , g ×₁ i)                 ≈⟨ DWD.identityʳ ⟨
+      Pulsh.₁ (f ×₁ h , g ×₁ i) ⌻ id-⧈          ∎
+    where
+      open DWD.HomReasoning
+
+  ⊗-homo : DWD-MC.⊗ ∘F (Pulsh ⁂ Pulsh) ≃ Pulsh ∘F MonoidalCategory.⊗ (S-MC.op ×-⊗ S-MC)
+  ⊗-homo = niHelper record
+      { η = λ (X , Y) → id-⧈ {Pulsh.₀ (zip S._⊕_ S._⊕_ X Y)}
+      ; η⁻¹ = λ (X , Y) → id-⧈ {Pulsh.₀ (zip S._⊕_ S._⊕_ X Y)}
+      ; commute = λ ((f , g) , (h , i)) → commute f g h i
+      ; iso = λ _ → id-iso DWD
+      }
+
+  open DWD.HomReasoning
+  open ⇒-Reasoning DWD
+
+  associativity
+      : {A A′ B B′ C C′ : Obj}
+      → Pulsh.₁ (assocʳ {A} {B} {C} , assocˡ {A′} {B′} {C′}) ⌻ id-⧈ ⌻ id-⧈ ⊞₁ id-⧈
+      ≈-⧈ id-⧈ ⌻ id-⧈ ⊞₁ id-⧈ ⌻ associator⇒
+  associativity = begin
+      Pulsh.₁ (assocʳ , assocˡ) ⌻ id-⧈ ⌻ id-⧈ ⊞₁ id-⧈ ≈⟨ elimʳ (elimʳ ⊞-identity) ⟩
+      Pulsh.₁ (assocʳ , assocˡ)                       ≈⟨ introˡ ⊞-identity ⟩
+      id-⧈ ⊞₁ id-⧈ ⌻ associator⇒                      ≈⟨ DWD.identityˡ ⟨
+      id-⧈ ⌻ id-⧈ ⊞₁ id-⧈ ⌻ associator⇒               ∎
+
+  unitaryˡ
+      : {A B : Obj}
+      → Pulsh.₁ (⟨ ! {A} , id {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ˡ⇒                                        ∎
+
+  unitaryʳ
+      : {A B : Obj}
+      → Pulsh.₁ (⟨ id {A} , ! {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ʳ⇒                                        ∎
+
+  braiding-compat
+      : {A B C D : Obj}
+      → Pulsh.₁ (swap {A} {B} , swap {C} {D}) ⌻ id-⧈
+      ≈-⧈ id-⧈ ⌻ swap-⧈ (B □ C) (A □ D)
+  braiding-compat = DWD.identityʳ ○ DWD.Equiv.sym DWD.identityˡ
+
+module BalancedPush where
+
+  Push-⊞₁
+      : {A A′ B B′ : Obj}
+        (f : A ⇒ A′)
+        (g : B ⇒ B′)
+      → Push.₁ f ⊞₁ Push.₁ g ≈-⧈ Push.₁ (f ×₁ g)
+  Push-⊞₁ {A} {A′} {B} {B′} f g = eqᵢ ⌸ refl
+    where
+      open HomReasoning
+      open ⇒-Reasoning 𝒞
+      f†×₁g† : A′ ⊕ B′ ⇒ A ⊕ B
+      f†×₁g† = (f †) ×₁ (g †)
+      eqᵢ : (f † ∘ π₂) ×₁ (g † ∘ π₂) ∘ σ₂₃ ≈ (f ×₁ g) † ∘ π₂
+      eqᵢ = begin
+          (f † ∘ π₂) ×₁ (g † ∘ π₂) ∘ σ₂₃              ≈⟨ pushˡ (sym ×₁∘×₁) ⟩
+          f†×₁g† ∘ π₂ ×₁ π₂ ∘ σ₂₃                     ≈⟨ refl⟩∘⟨ ×₁∘⟨⟩ ⟩
+          f†×₁g† ∘ ⟨ π₂ ∘ π₁ ×₁ π₁ , π₂ ∘ π₂ ×₁ π₂ ⟩  ≈⟨ refl⟩∘⟨ ⟨⟩-cong₂ π₂∘×₁ π₂∘×₁ ⟩
+          f†×₁g† ∘ ⟨ π₁ ∘ π₂ , π₂ ∘ π₂ ⟩              ≈⟨ refl⟩∘⟨ g-η ⟩
+          f†×₁g† ∘ π₂                                 ≈⟨ †-resp-×₁ ⟩∘⟨refl ⟨
+          (f ×₁ g) † ∘ π₂                             ∎
+
+  commute
+      : {A B C D : Obj}
+        (f : A ⇒ B)
+        (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-⧈        ∎
+    where
+      open DWD.HomReasoning
+
+  ⊗-homo : BWD-MC.⊗ ∘F (Push ⁂ Push) ≃ Push ∘F MonoidalCategory.⊗ S-MC
+  ⊗-homo = niHelper record
+      { η = λ (X , Y) → id-⧈ {Push.₀ (X ⊕ Y) □ Push.₀ (X ⊕ Y)}
+      ; η⁻¹ = λ (X , Y) → id-⧈ {Push.₀ (X ⊕ Y) □ Push.₀ (X ⊕ Y)}
+      ; commute = λ (f , g) → commute f g
+      ; iso = λ _ → id-iso BWD
+      }
+
+  open BWD.HomReasoning
+  open ⇒-Reasoning BWD
+
+  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 ⟩
+      assocʳ ∘ π₂ ⧈ assocˡ                ≈⟨ introˡ ⊞-identity ⟩
+      id-⧈ ⊞₁ id-⧈ ⌻ associator⇒          ≈⟨ BWD.identityˡ ⟨
+      id-⧈ ⌻ id-⧈ ⊞₁ id-⧈ ⌻ associator⇒   ∎
+
+  unitaryˡ
+      : {A : Obj}
+      → Push.₁ (π₂ {𝟘} {A}) ⌻ id-⧈ ⌻ id-⧈ ⊞₁ id-⧈
+      ≈-⧈ unitorˡ⇒
+  unitaryˡ = begin
+      Push.₁ π₂ ⌻ id-⧈ ⌻ id-⧈ ⊞₁ id-⧈ ≈⟨ elimʳ (elimʳ ⊞-identity) ⟩
+      Push.₁ π₂                       ≈⟨ ∘-resp-≈ˡ π₂† ⌸ refl ⟩
+      unitorˡ⇒                        ∎
+
+  unitaryʳ
+      : {A : Obj}
+      → Push.₁ (π₁ {A} {𝟘}) ⌻ id-⧈ ⌻ id-⧈ ⊞₁ id-⧈
+      ≈-⧈ unitorʳ⇒
+  unitaryʳ = begin
+      Push.₁ π₁ ⌻ id-⧈ ⌻ id-⧈ ⊞₁ id-⧈ ≈⟨ elimʳ (elimʳ ⊞-identity) ⟩
+      Push.₁ π₁                       ≈⟨ ∘-resp-≈ˡ π₁† ⌸ refl ⟩
+      unitorʳ⇒                        ∎
+
+  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ˡ
+
+module BalancedPull where
+
+  Pull-⊞₁
+      : {A A′ B B′ : Obj}
+        (f : A ⇒ A′)
+        (g : B ⇒ B′)
+      → Pull.₁ f ⊞₁ Pull.₁ g ≈-⧈ Pull.₁ (f ×₁ g)
+  Pull-⊞₁ {A} {A′} {B} {B′} f g = eqᵢ ⌸ sym †-resp-×₁
+    where
+      open HomReasoning
+      open ⇒-Reasoning 𝒞
+      eqᵢ : (f ∘ π₂) ×₁ (g ∘ π₂) ∘ σ₂₃ ≈ (f ×₁ g) ∘ π₂
+      eqᵢ = begin
+          (f ∘ π₂) ×₁ (g ∘ π₂) ∘ σ₂₃                  ≈⟨ pushˡ (sym ×₁∘×₁) ⟩
+          f ×₁ g ∘ π₂ ×₁ π₂ ∘ σ₂₃                     ≈⟨ refl⟩∘⟨ ×₁∘⟨⟩ ⟩
+          f ×₁ g ∘ ⟨ π₂ ∘ π₁ ×₁ π₁ , π₂ ∘ π₂ ×₁ π₂ ⟩  ≈⟨ refl⟩∘⟨ ⟨⟩-cong₂ π₂∘×₁ π₂∘×₁ ⟩
+          f ×₁ g ∘ ⟨ π₁ ∘ π₂ , π₂ ∘ π₂ ⟩              ≈⟨ refl⟩∘⟨ g-η ⟩
+          f ×₁ g ∘ π₂                                 ∎
+
+  commute
+      : {A B C D : Obj}
+        (f : A ⇒ B)
+        (g : C ⇒ D)
+      → id-⧈ ⌻ Pull.₁ f ⊞₁ Pull.₁ g ≈-⧈ Pull.₁ (f ×₁ g) ⌻ id-⧈
+  commute f g = begin
+      id-⧈ ⌻ Pull.₁ f ⊞₁ Pull.₁ g   ≈⟨ DWD.identityˡ ⟩
+      Pull.₁ f ⊞₁ Pull.₁ g          ≈⟨ Pull-⊞₁ f g ⟩
+      Pull.₁ (f ×₁ g)               ≈⟨ DWD.identityʳ ⟨
+      Pull.₁ (f ×₁ g) ⌻ id-⧈        ∎
+    where
+      open DWD.HomReasoning
+
+  ⊗-homo : BWD-MC.⊗ ∘F (Pull ⁂ Pull) ≃ Pull ∘F MonoidalCategory.⊗ S-MC.op
+  ⊗-homo = niHelper record
+      { η = λ (X , Y) → id-⧈ {Pull.₀ (X ⊕ Y) □ Pull.₀ (X ⊕ Y)}
+      ; η⁻¹ = λ (X , Y) → id-⧈ {Pull.₀ (X ⊕ Y) □ Pull.₀ (X ⊕ Y)}
+      ; commute = λ (f , g) → commute f g
+      ; iso = λ _ → id-iso BWD
+      }
+
+  open BWD.HomReasoning
+  open ⇒-Reasoning BWD
+
+  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 ⌸ α⇐† ⟩
+      assocʳ ∘ π₂ ⧈ assocˡ                ≈⟨ introˡ ⊞-identity ⟩
+      id-⧈ ⊞₁ id-⧈ ⌻ associator⇒          ≈⟨ BWD.identityˡ ⟨
+      id-⧈ ⌻ id-⧈ ⊞₁ id-⧈ ⌻ associator⇒   ∎
+
+  unitaryˡ
+      : {A : Obj}
+      → Pull.₁ ⟨ ! {A} , id {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ˡ⇒                                ∎
+
+  unitaryʳ
+      : {A : Obj}
+      → Pull.₁ ⟨ id {A} , ! {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ʳ⇒                                ∎
+
+  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ˡ
+
+Pulsh-IsMF : IsStrongMonoidalFunctor (S-MC.op ×-⊗ S-MC) DWD-MC Pulsh
+Pulsh-IsMF = record
+    { ε = ≅.refl DWD
+    ; ⊗-homo = Directed.⊗-homo
+    ; associativity = Directed.associativity
+    ; unitaryˡ = Directed.unitaryˡ
+    ; unitaryʳ = Directed.unitaryʳ
+    }
+
+Pulsh-MF : StrongMonoidalFunctor (S-MC.op ×-⊗ S-MC) DWD-MC
+Pulsh-MF = record
+    { F = Pulsh
+    ; isStrongMonoidal = Pulsh-IsMF
+    }
+
+Pulsh-SMF : Strong.SymmetricMonoidalFunctor (S-SMC.op ×-σ⊗ S-SMC) DWD-SMC
+Pulsh-SMF = record
+    { F = Pulsh
+    ; isBraidedMonoidal = record
+        { isStrongMonoidal = Pulsh-IsMF
+        ; braiding-compat = Directed.braiding-compat
+        }
+    }
+
+Push-IsMF : IsStrongMonoidalFunctor S-MC BWD-MC Push
+Push-IsMF = record
+    { ε = ≅.refl BWD
+    ; ⊗-homo = BalancedPush.⊗-homo
+    ; associativity = BalancedPush.associativity
+    ; unitaryˡ = BalancedPush.unitaryˡ
+    ; unitaryʳ = BalancedPush.unitaryʳ
+    }
+
+Push-MF : StrongMonoidalFunctor S-MC BWD-MC
+Push-MF = record
+    { F = Push
+    ; isStrongMonoidal = Push-IsMF
+    }
+
+Push-SMF : Strong.SymmetricMonoidalFunctor S-SMC BWD-SMC
+Push-SMF = record
+    { F = Push
+    ; isBraidedMonoidal = record
+        { isStrongMonoidal = Push-IsMF
+        ; braiding-compat = BalancedPush.braiding-compat
+        }
+    }
+
+Pull-IsMF : IsStrongMonoidalFunctor S-MC.op BWD-MC Pull
+Pull-IsMF = record
+    { ε = ≅.refl BWD
+    ; ⊗-homo = BalancedPull.⊗-homo
+    ; associativity = BalancedPull.associativity
+    ; unitaryˡ = BalancedPull.unitaryˡ
+    ; unitaryʳ = BalancedPull.unitaryʳ
+    }
+
+Pull-MF : StrongMonoidalFunctor S-MC.op BWD-MC
+Pull-MF = record
+    { F = Pull
+    ; isStrongMonoidal = Pull-IsMF
+    }
+
+Pull-SMF : Strong.SymmetricMonoidalFunctor S-SMC.op BWD-SMC
+Pull-SMF = record
+    { F = Pull
+    ; isBraidedMonoidal = record
+        { isStrongMonoidal = Pull-IsMF
+        ; braiding-compat = BalancedPull.braiding-compat
+        }
+    }