From 3bc122cbf6ca05155e1f7479d8edf21d024b4b42 Mon Sep 17 00:00:00 2001 From: Sandro Stucki Date: Sat, 6 Jan 2024 22:49:11 +0100 Subject: [PATCH] [ wip ] everything still works for braided categories (as opposed to symmetric). --- src/Categories/Monad/Strong/Properties.agda | 105 ++++++++++---------- 1 file changed, 50 insertions(+), 55 deletions(-) diff --git a/src/Categories/Monad/Strong/Properties.agda b/src/Categories/Monad/Strong/Properties.agda index fe935161b..901093410 100644 --- a/src/Categories/Monad/Strong/Properties.agda +++ b/src/Categories/Monad/Strong/Properties.agda @@ -1,6 +1,6 @@ {-# OPTIONS --without-K --safe #-} --- In symmetric monoidal categories left and right strength imply each other +-- In braided monoidal categories left and right strength imply each other module Categories.Monad.Strong.Properties where @@ -15,7 +15,7 @@ open import Categories.Category.Monoidal using (Monoidal) import Categories.Category.Monoidal.Braided.Properties as BraidedProps import Categories.Category.Monoidal.Reasoning as MonoidalReasoning import Categories.Category.Monoidal.Utilities as MonoidalUtils -open import Categories.Category.Monoidal.Symmetric using (Symmetric) +open import Categories.Category.Monoidal.Braided using (Braided) open import Categories.NaturalTransformation using (NaturalTransformation; ntHelper) open import Categories.Monad using (Monad) open import Categories.Monad.Strong using (Strength; RightStrength; StrongMonad; RightStrongMonad) @@ -27,10 +27,10 @@ private o ℓ e : Level -- FIXME: make these top-level module parameters and remove this anonymous module? -module _ {C : Category o ℓ e} {V : Monoidal C} (S : Symmetric V) where +module _ {C : Category o ℓ e} {V : Monoidal C} (BV : Braided V) where open Category C - open Symmetric S - open BraidedProps braided using (braiding-coherence; inv-braiding-coherence) + open Braided BV + open BraidedProps BV using (braiding-coherence; inv-braiding-coherence) open MonoidalUtils V using (_⊗ᵢ_) open MonoidalUtils.Shorthands V -- for λ⇒, ρ⇒, α⇒, ... open Core.Shorthands C -- for idᵢ, _∘ᵢ_, ... @@ -42,14 +42,8 @@ module _ {C : Category o ℓ e} {V : Monoidal C} (S : Symmetric V) where variable X Y Z W : Obj - -- FIXME: this should probably go into - -- Categories.Monoidal.Symmetric.Properties and be called - -- braided-selfInverse or something similar. - braiding-eq : ∀ {X Y} → braiding.⇐.η (X , Y) ≈ braiding.⇒.η (Y , X) - braiding-eq = introʳ commutative ○ cancelˡ (braiding.iso.isoˡ _) - module LeftStrength {M : Monad C} (leftStrength : Strength V M) where - open BraidedProps.Shorthands braided renaming (σ to B; σ⇒ to B⇒; σ⇐ to B⇐) + open BraidedProps.Shorthands BV renaming (σ to B; σ⇒ to B⇒; σ⇐ to B⇐) open Monad M using (F; μ; η) module leftStrength = Strength leftStrength @@ -61,20 +55,20 @@ module _ {C : Category o ℓ e} {V : Monoidal C} (S : Symmetric V) where open Shorthands - -- The left strength induces a right strength + -- The left strength induces a right strength via braiding. private τ : ∀ {X Y} → F.₀ X ⊗₀ Y ⇒ F.₀ (X ⊗₀ Y) - τ {X} {Y} = F.₁ B⇒ ∘ σ ∘ B⇒ + τ {X} {Y} = F.₁ B⇐ ∘ σ ∘ B⇒ τ-commute : (f : X ⇒ Z) (g : Y ⇒ W) → τ ∘ (F.₁ f ⊗₁ g) ≈ F.₁ (f ⊗₁ g) ∘ τ τ-commute f g = begin - (F.₁ B⇒ ∘ σ ∘ B⇒) ∘ (F.₁ f ⊗₁ g) ≈⟨ pullʳ (pullʳ (braiding.⇒.commute (F.₁ f , g))) ⟩ - F.₁ B⇒ ∘ σ ∘ ((g ⊗₁ F.₁ f) ∘ B⇒) ≈⟨ refl⟩∘⟨ pullˡ (σ.commute (g , f)) ⟩ - F.₁ B⇒ ∘ (F.₁ (g ⊗₁ f) ∘ σ) ∘ B⇒ ≈˘⟨ pushˡ (pushˡ (F.homomorphism)) ⟩ - (F.₁ (B⇒ ∘ (g ⊗₁ f)) ∘ σ) ∘ B⇒ ≈⟨ pushˡ (F.F-resp-≈ (braiding.⇒.commute (g , f)) ⟩∘⟨refl) ⟩ - F.₁ ((f ⊗₁ g) ∘ B⇒) ∘ σ ∘ B⇒ ≈⟨ pushˡ F.homomorphism ⟩ - F.₁ (f ⊗₁ g) ∘ F.₁ B⇒ ∘ σ ∘ B⇒ ∎ + (F.₁ B⇐ ∘ σ ∘ B⇒) ∘ (F.₁ f ⊗₁ g) ≈⟨ pullʳ (pullʳ (braiding.⇒.commute (F.₁ f , g))) ⟩ + F.₁ B⇐ ∘ σ ∘ ((g ⊗₁ F.₁ f) ∘ B⇒) ≈⟨ refl⟩∘⟨ pullˡ (σ.commute (g , f)) ⟩ + F.₁ B⇐ ∘ (F.₁ (g ⊗₁ f) ∘ σ) ∘ B⇒ ≈˘⟨ pushˡ (pushˡ (F.homomorphism)) ⟩ + (F.₁ (B⇐ ∘ (g ⊗₁ f)) ∘ σ) ∘ B⇒ ≈⟨ pushˡ (F.F-resp-≈ (braiding.⇐.commute (f , g)) ⟩∘⟨refl) ⟩ + F.₁ ((f ⊗₁ g) ∘ B⇐) ∘ σ ∘ B⇒ ≈⟨ pushˡ F.homomorphism ⟩ + F.₁ (f ⊗₁ g) ∘ F.₁ B⇐ ∘ σ ∘ B⇒ ∎ right-strengthen : NaturalTransformation (⊗ ∘F (F ⁂ idF)) (F ∘F ⊗) right-strengthen = ntHelper (record @@ -86,15 +80,15 @@ module _ {C : Category o ℓ e} {V : Monoidal C} (S : Symmetric V) where -- The strengths commute with braiding - left-right-braiding-comm : ∀ {X Y} → F.₁ B⇒ ∘ σ {X} {Y} ≈ τ ∘ B⇒ + left-right-braiding-comm : ∀ {X Y} → F.₁ B⇐ ∘ σ {X} {Y} ≈ τ ∘ B⇐ left-right-braiding-comm = begin - F.₁ B⇒ ∘ σ ≈˘⟨ pullʳ (cancelʳ commutative) ⟩ - (F.₁ B⇒ ∘ σ ∘ B⇒) ∘ B⇒ ∎ + F.₁ B⇐ ∘ σ ≈˘⟨ pullʳ (cancelʳ (braiding.iso.isoʳ _)) ⟩ + (F.₁ B⇐ ∘ σ ∘ B⇒) ∘ B⇐ ∎ right-left-braiding-comm : ∀ {X Y} → F.₁ B⇒ ∘ τ {X} {Y} ≈ σ ∘ B⇒ right-left-braiding-comm = begin - F.₁ B⇒ ∘ (F.₁ B⇒ ∘ σ ∘ B⇒) ≈˘⟨ pushˡ F.homomorphism ⟩ - F.₁ (B⇒ ∘ B⇒) ∘ σ ∘ B⇒ ≈⟨ F.F-resp-≈ commutative ⟩∘⟨refl ⟩ + F.₁ B⇒ ∘ (F.₁ B⇐ ∘ σ ∘ B⇒) ≈˘⟨ pushˡ F.homomorphism ⟩ + F.₁ (B⇒ ∘ B⇐) ∘ σ ∘ B⇒ ≈⟨ F.F-resp-≈ (braiding.iso.isoʳ _) ⟩∘⟨refl ⟩ F.₁ id ∘ σ ∘ B⇒ ≈⟨ elimˡ F.identity ⟩ σ ∘ B⇒ ∎ @@ -139,29 +133,29 @@ module _ {C : Category o ℓ e} {V : Monoidal C} (S : Symmetric V) where F.₁ (B⇐ ∘ id ⊗₁ B⇐ ∘ α⇒ ∘ B⇒ ∘ id ⊗₁ B⇒) ∘ τ ≈⟨ pushˡ F.homomorphism ⟩ F.₁ B⇐ ∘ F.₁ (id ⊗₁ B⇐ ∘ α⇒ ∘ B⇒ ∘ id ⊗₁ B⇒) ∘ τ - ≈⟨ F.F-resp-≈ braiding-eq ⟩∘⟨ pushˡ F.homomorphism ⟩ - F.₁ B⇒ ∘ F.₁ (id ⊗₁ B⇐) ∘ F.₁ (α⇒ ∘ B⇒ ∘ id ⊗₁ B⇒) ∘ τ - ≈⟨ refl⟩∘⟨ F.F-resp-≈ (refl⟩⊗⟨ braiding-eq) ⟩∘⟨ pushˡ F.homomorphism ⟩ - F.₁ B⇒ ∘ F.₁ (id ⊗₁ B⇒) ∘ F.₁ α⇒ ∘ F.₁ (B⇒ ∘ id ⊗₁ B⇒) ∘ τ + ≈⟨ refl⟩∘⟨ pushˡ F.homomorphism ⟩ + F.₁ B⇐ ∘ F.₁ (id ⊗₁ B⇐) ∘ F.₁ (α⇒ ∘ B⇒ ∘ id ⊗₁ B⇒) ∘ τ + ≈⟨ refl⟩∘⟨ refl⟩∘⟨ pushˡ F.homomorphism ⟩ + F.₁ B⇐ ∘ F.₁ (id ⊗₁ B⇐) ∘ F.₁ α⇒ ∘ F.₁ (B⇒ ∘ id ⊗₁ B⇒) ∘ τ ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ pushˡ F.homomorphism ⟩ - F.₁ B⇒ ∘ F.₁ (id ⊗₁ B⇒) ∘ F.₁ α⇒ ∘ F.₁ B⇒ ∘ F.₁ (id ⊗₁ B⇒) ∘ τ + F.₁ B⇐ ∘ F.₁ (id ⊗₁ B⇐) ∘ F.₁ α⇒ ∘ F.₁ B⇒ ∘ F.₁ (id ⊗₁ B⇒) ∘ τ ≈˘⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ τ.commute (id , B⇒) ⟩ - F.₁ B⇒ ∘ F.₁ (id ⊗₁ B⇒) ∘ F.₁ α⇒ ∘ F.₁ B⇒ ∘ τ ∘ F.₁ id ⊗₁ B⇒ + F.₁ B⇐ ∘ F.₁ (id ⊗₁ B⇐) ∘ F.₁ α⇒ ∘ F.₁ B⇒ ∘ τ ∘ F.₁ id ⊗₁ B⇒ ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ extendʳ right-left-braiding-comm ⟩ - F.₁ B⇒ ∘ F.₁ (id ⊗₁ B⇒) ∘ F.₁ α⇒ ∘ σ ∘ B⇒ ∘ F.₁ id ⊗₁ B⇒ + F.₁ B⇐ ∘ F.₁ (id ⊗₁ B⇐) ∘ F.₁ α⇒ ∘ σ ∘ B⇒ ∘ F.₁ id ⊗₁ B⇒ ≈⟨ refl⟩∘⟨ refl⟩∘⟨ extendʳ leftStrength.strength-assoc ⟩ - F.₁ B⇒ ∘ F.₁ (id ⊗₁ B⇒) ∘ σ ∘ (id ⊗₁ σ ∘ α⇒) ∘ B⇒ ∘ F.₁ id ⊗₁ B⇒ + F.₁ B⇐ ∘ F.₁ (id ⊗₁ B⇐) ∘ σ ∘ (id ⊗₁ σ ∘ α⇒) ∘ B⇒ ∘ F.₁ id ⊗₁ B⇒ ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ pullʳ (refl⟩∘⟨ refl⟩∘⟨ F.identity ⟩⊗⟨refl) ⟩ - F.₁ B⇒ ∘ F.₁ (id ⊗₁ B⇒) ∘ σ ∘ id ⊗₁ σ ∘ α⇒ ∘ B⇒ ∘ id ⊗₁ B⇒ - ≈˘⟨ refl⟩∘⟨ extendʳ (σ.commute (id , B⇒)) ⟩ - F.₁ B⇒ ∘ σ ∘ id ⊗₁ F.₁ B⇒ ∘ id ⊗₁ σ ∘ α⇒ ∘ B⇒ ∘ id ⊗₁ B⇒ + F.₁ B⇐ ∘ F.₁ (id ⊗₁ B⇐) ∘ σ ∘ id ⊗₁ σ ∘ α⇒ ∘ B⇒ ∘ id ⊗₁ B⇒ + ≈˘⟨ refl⟩∘⟨ extendʳ (σ.commute (id , B⇐)) ⟩ + F.₁ B⇐ ∘ σ ∘ id ⊗₁ F.₁ B⇐ ∘ id ⊗₁ σ ∘ α⇒ ∘ B⇒ ∘ id ⊗₁ B⇒ ≈⟨ extendʳ left-right-braiding-comm ⟩ - τ ∘ B⇒ ∘ id ⊗₁ F.₁ B⇒ ∘ id ⊗₁ σ ∘ α⇒ ∘ B⇒ ∘ id ⊗₁ B⇒ + τ ∘ B⇐ ∘ id ⊗₁ F.₁ B⇐ ∘ id ⊗₁ σ ∘ α⇒ ∘ B⇒ ∘ id ⊗₁ B⇒ ≈⟨ refl⟩∘⟨ refl⟩∘⟨ extendʳ (parallel Equiv.refl left-right-braiding-comm) ⟩ - τ ∘ B⇒ ∘ id ⊗₁ τ ∘ id ⊗₁ B⇒ ∘ α⇒ ∘ B⇒ ∘ id ⊗₁ B⇒ - ≈⟨ refl⟩∘⟨ extendʳ (braiding.⇒.commute (id , τ)) ⟩ - τ ∘ τ ⊗₁ id ∘ B⇒ ∘ id ⊗₁ B⇒ ∘ α⇒ ∘ B⇒ ∘ id ⊗₁ B⇒ - ≈⟨ refl⟩∘⟨ refl⟩∘⟨ ⟺ braiding-eq ⟩∘⟨ (refl⟩⊗⟨ ⟺ braiding-eq) ⟩∘⟨refl ⟩ + τ ∘ B⇐ ∘ id ⊗₁ τ ∘ id ⊗₁ B⇐ ∘ α⇒ ∘ B⇒ ∘ id ⊗₁ B⇒ + ≈⟨ refl⟩∘⟨ extendʳ (braiding.⇐.commute (τ , id)) ⟩ + τ ∘ τ ⊗₁ id ∘ B⇐ ∘ id ⊗₁ B⇐ ∘ α⇒ ∘ B⇒ ∘ id ⊗₁ B⇒ + ≈⟨ refl⟩∘⟨ refl⟩∘⟨ Equiv.refl ⟩∘⟨ (refl⟩⊗⟨ Equiv.refl) ⟩∘⟨refl ⟩ τ ∘ τ ⊗₁ id ∘ B⇐ ∘ id ⊗₁ B⇐ ∘ α⇒ ∘ B⇒ ∘ id ⊗₁ B⇒ ≈⟨ refl⟩∘⟨ refl⟩∘⟨ assoc-reverse ⟩ τ ∘ τ ⊗₁ id ∘ α⇐ @@ -181,31 +175,32 @@ module _ {C : Category o ℓ e} {V : Monoidal C} (S : Symmetric V) where module strength = Strength strength module t = strength.strengthen B = braiding.⇒.η + open BraidedProps.Shorthands BV using () renaming (σ⇐ to B⇐) τ : ∀ ((X , Y) : Obj × Obj) → F.₀ X ⊗₀ Y ⇒ F.₀ (X ⊗₀ Y) - τ (X , Y) = F.₁ (B (Y , X)) ∘ t.η (Y , X) ∘ B (F.₀ X , Y) + τ (X , Y) = F.₁ B⇐ ∘ t.η (Y , X) ∘ B (F.₀ X , Y) identityˡ' : ∀ {X : Obj} → F.₁ unitorʳ.from ∘ τ (X , unit) ≈ unitorʳ.from identityˡ' {X} = begin - F.₁ unitorʳ.from ∘ F.₁ (B (unit , X)) ∘ t.η (unit , X) ∘ B (F.₀ X , unit) ≈⟨ pullˡ (⟺ F.homomorphism) ⟩ - F.₁ (unitorʳ.from ∘ B (unit , X)) ∘ t.η (unit , X) ∘ B (F.₀ X , unit) ≈⟨ ((F.F-resp-≈ ((refl⟩∘⟨ ⟺ braiding-eq) ○ inv-braiding-coherence)) ⟩∘⟨refl) ⟩ + F.₁ unitorʳ.from ∘ F.₁ B⇐ ∘ t.η (unit , X) ∘ B (F.₀ X , unit) ≈⟨ pullˡ (⟺ F.homomorphism) ⟩ + F.₁ (unitorʳ.from ∘ B⇐) ∘ t.η (unit , X) ∘ B (F.₀ X , unit) ≈⟨ ((F.F-resp-≈ (inv-braiding-coherence)) ⟩∘⟨refl) ⟩ F.₁ unitorˡ.from ∘ t.η (unit , X) ∘ B (F.₀ X , unit) ≈⟨ pullˡ strength.identityˡ ⟩ unitorˡ.from ∘ B (F.₀ X , unit) ≈⟨ braiding-coherence ⟩ unitorʳ.from ∎ η-comm' : ∀ {X Y : Obj} → τ (X , Y) ∘ η.η X ⊗₁ id ≈ η.η (X ⊗₀ Y) η-comm' {X} {Y} = begin - (F.₁ (B (Y , X)) ∘ t.η (Y , X) ∘ B (F.₀ X , Y)) ∘ (η.η X ⊗₁ id) ≈⟨ pullʳ (pullʳ (braiding.⇒.commute (η.η X , id))) ⟩ - F.₁ (B (Y , X)) ∘ t.η (Y , X) ∘ ((id ⊗₁ η.η X) ∘ B (X , Y)) ≈⟨ (refl⟩∘⟨ (pullˡ strength.η-comm)) ⟩ - F.₁ (B (Y , X)) ∘ η.η (Y ⊗₀ X) ∘ B (X , Y) ≈⟨ pullˡ (⟺ (η.commute (B (Y , X)))) ⟩ - (η.η (X ⊗₀ Y) ∘ B (Y , X)) ∘ B (X , Y) ≈⟨ cancelʳ commutative ⟩ + (F.₁ B⇐ ∘ t.η (Y , X) ∘ B (F.₀ X , Y)) ∘ (η.η X ⊗₁ id) ≈⟨ pullʳ (pullʳ (braiding.⇒.commute (η.η X , id))) ⟩ + F.₁ B⇐ ∘ t.η (Y , X) ∘ ((id ⊗₁ η.η X) ∘ B (X , Y)) ≈⟨ (refl⟩∘⟨ (pullˡ strength.η-comm)) ⟩ + F.₁ B⇐ ∘ η.η (Y ⊗₀ X) ∘ B (X , Y) ≈⟨ pullˡ (⟺ (η.commute B⇐)) ⟩ + (η.η (X ⊗₀ Y) ∘ B⇐) ∘ B (X , Y) ≈⟨ cancelʳ (braiding.iso.isoˡ _) ⟩ η.η (X ⊗₀ Y) ∎ μ-η-comm' : ∀ {X Y : Obj} → μ.η (X ⊗₀ Y) ∘ F.₁ (τ (X , Y)) ∘ τ (F.₀ X , Y) ≈ τ (X , Y) ∘ μ.η X ⊗₁ id μ-η-comm' {X} {Y} = begin - μ.η (X ⊗₀ Y) ∘ F.F₁ (τ (X , Y)) ∘ F.₁ (B (Y , F.₀ X)) ∘ t.η (Y , F.₀ X) ∘ B (F.₀ (F.₀ X) , Y) ≈⟨ (refl⟩∘⟨ (pullˡ (⟺ F.homomorphism))) ⟩ - μ.η (X ⊗₀ Y) ∘ F.₁ (τ (X , Y) ∘ B (Y , F.₀ X)) ∘ t.η (Y , F.₀ X) ∘ B (F.₀ (F.₀ X) , Y) ≈⟨ (refl⟩∘⟨ ((F.F-resp-≈ (pullʳ (cancelʳ commutative))) ⟩∘⟨refl)) ⟩ - μ.η (X ⊗₀ Y) ∘ F.₁ (F.₁ (B (Y , X)) ∘ t.η (Y , X)) ∘ t.η (Y , F.₀ X) ∘ B (F.₀ (F.₀ X) , Y) ≈⟨ (refl⟩∘⟨ (F.homomorphism ⟩∘⟨refl)) ⟩ - μ.η (X ⊗₀ Y) ∘ (F.₁ (F.₁ (B (Y , X))) ∘ F.₁ (t.η (Y , X))) ∘ t.η (Y , F.₀ X) ∘ B (F.₀ (F.₀ X) , Y) ≈⟨ pullˡ (pullˡ (μ.commute (B (Y , X)))) ⟩ - ((F.₁ (B (Y , X)) ∘ μ.η (Y ⊗₀ X)) ∘ F.₁ (t.η (Y , X))) ∘ t.η (Y , F.₀ X) ∘ B (F.₀ (F.₀ X) , Y) ≈⟨ (assoc² ○ (refl⟩∘⟨ ⟺ assoc²')) ⟩ - F.₁ (B (Y , X)) ∘ (μ.η (Y ⊗₀ X) ∘ F.₁ (t.η (Y , X)) ∘ t.η (Y , F.₀ X)) ∘ B ((F.₀ (F.₀ X)) , Y) ≈⟨ refl⟩∘⟨ pushˡ strength.μ-η-comm ⟩ - F.₁ (B (Y , X)) ∘ t.η (Y , X) ∘ (id ⊗₁ μ.η X) ∘ B ((F.₀ (F.₀ X)) , Y) ≈˘⟨ pullʳ (pullʳ (braiding.⇒.commute (μ.η X , id))) ⟩ + μ.η (X ⊗₀ Y) ∘ F.₁ (τ (X , Y)) ∘ F.₁ B⇐ ∘ t.η (Y , F.₀ X) ∘ B (F.₀ (F.₀ X) , Y) ≈⟨ refl⟩∘⟨ pullˡ (⟺ F.homomorphism) ⟩ + μ.η (X ⊗₀ Y) ∘ F.₁ (τ (X , Y) ∘ B⇐) ∘ t.η (Y , F.₀ X) ∘ B (F.₀ (F.₀ X) , Y) ≈⟨ (refl⟩∘⟨ ((F.F-resp-≈ (pullʳ (cancelʳ (braiding.iso.isoʳ _)))) ⟩∘⟨refl)) ⟩ + μ.η (X ⊗₀ Y) ∘ F.₁ (F.₁ B⇐ ∘ t.η (Y , X)) ∘ t.η (Y , F.₀ X) ∘ B (F.₀ (F.₀ X) , Y) ≈⟨ (refl⟩∘⟨ (F.homomorphism ⟩∘⟨refl)) ⟩ + μ.η (X ⊗₀ Y) ∘ (F.₁ (F.₁ B⇐) ∘ F.₁ (t.η (Y , X))) ∘ t.η (Y , F.₀ X) ∘ B (F.₀ (F.₀ X) , Y) ≈⟨ pullˡ (pullˡ (μ.commute B⇐)) ⟩ + ((F.₁ B⇐ ∘ μ.η (Y ⊗₀ X)) ∘ F.₁ (t.η (Y , X))) ∘ t.η (Y , F.₀ X) ∘ B (F.₀ (F.₀ X) , Y) ≈⟨ (assoc² ○ (refl⟩∘⟨ ⟺ assoc²')) ⟩ + F.₁ B⇐ ∘ (μ.η (Y ⊗₀ X) ∘ F.₁ (t.η (Y , X)) ∘ t.η (Y , F.₀ X)) ∘ B ((F.₀ (F.₀ X)) , Y) ≈⟨ refl⟩∘⟨ pushˡ strength.μ-η-comm ⟩ + F.₁ B⇐ ∘ t.η (Y , X) ∘ (id ⊗₁ μ.η X) ∘ B ((F.₀ (F.₀ X)) , Y) ≈˘⟨ pullʳ (pullʳ (braiding.⇒.commute (μ.η X , id))) ⟩ τ (X , Y) ∘ μ.η X ⊗₁ id ∎ StrongMonad⇒RightStrongMonad : StrongMonad V → RightStrongMonad V