From 014e65626daa7bbd0375e5b9ad9bf0ad8addabdc Mon Sep 17 00:00:00 2001 From: Jacques Comeaux Date: Sat, 1 Aug 2026 19:21:52 -0500 Subject: Upgrade Push + Pull to symmetric monoidal functors --- Data/WiringDiagram/Monoidal.agda | 401 +++++++++++++++++++++++++++++++++++++++ 1 file changed, 401 insertions(+) create mode 100644 Data/WiringDiagram/Monoidal.agda (limited to 'Data/WiringDiagram') 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 + } + } -- cgit v1.2.3