{-# 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
        }
    }