diff --git a/src/Categories/Category/Monoidal/Braided/Properties.agda b/src/Categories/Category/Monoidal/Braided/Properties.agda index a63e7fe31..c10b45946 100644 --- a/src/Categories/Category/Monoidal/Braided/Properties.agda +++ b/src/Categories/Category/Monoidal/Braided/Properties.agda @@ -156,3 +156,23 @@ inv-braiding-coherence : [ unit ⊗₀ X ⇒ X ]⟨ ≈ λ⇒ ⟩ inv-braiding-coherence = ⟺ (switch-fromtoʳ σ braiding-coherence) + +-- Reversing a ternary product via braiding commutes with the associator. + +assoc-reverse : [ X ⊗₀ (Y ⊗₀ Z) ⇒ (X ⊗₀ Y) ⊗₀ Z ]⟨ + id ⊗₁ σ⇒ ⇒⟨ X ⊗₀ (Z ⊗₀ Y) ⟩ + σ⇒ ⇒⟨ (Z ⊗₀ Y) ⊗₀ X ⟩ + α⇒ ⇒⟨ Z ⊗₀ (Y ⊗₀ X) ⟩ + id ⊗₁ σ⇐ ⇒⟨ Z ⊗₀ (X ⊗₀ Y) ⟩ + σ⇐ + ≈ α⇐ + ⟩ +assoc-reverse = begin + σ⇐ ∘ id ⊗₁ σ⇐ ∘ α⇒ ∘ σ⇒ ∘ id ⊗₁ σ⇒ ≈˘⟨ refl⟩∘⟨ assoc²' ⟩ + σ⇐ ∘ (id ⊗₁ σ⇐ ∘ α⇒ ∘ σ⇒) ∘ id ⊗₁ σ⇒ ≈⟨ refl⟩∘⟨ pushˡ hex₁' ⟩ + σ⇐ ∘ (α⇒ ∘ σ⇒ ⊗₁ id) ∘ α⇐ ∘ id ⊗₁ σ⇒ ≈⟨ refl⟩∘⟨ pullʳ (sym-assoc ○ hexagon₂) ⟩ + σ⇐ ∘ α⇒ ∘ (α⇐ ∘ σ⇒) ∘ α⇐ ≈⟨ refl⟩∘⟨ pullˡ (cancelˡ associator.isoʳ) ⟩ + σ⇐ ∘ σ⇒ ∘ α⇐ ≈⟨ cancelˡ (braiding.iso.isoˡ _) ⟩ + α⇐ ∎ + where + hex₁' = conjugate-from associator (idᵢ ⊗ᵢ σ) (⟺ (hexagon₁ ○ sym-assoc)) diff --git a/src/Categories/Category/Monoidal/Construction/Reverse.agda b/src/Categories/Category/Monoidal/Construction/Reverse.agda new file mode 100644 index 000000000..a4f338071 --- /dev/null +++ b/src/Categories/Category/Monoidal/Construction/Reverse.agda @@ -0,0 +1,126 @@ +{-# OPTIONS --without-K --safe #-} + +module Categories.Category.Monoidal.Construction.Reverse where + +-- The reverse monoidal category of a monoidal category V has the same +-- underlying category and unit as V but reversed monoidal product, +-- and similarly for tensors of morphisms. +-- +-- https://ncatlab.org/nlab/show/reverse+monoidal+category + +open import Level using (_⊔_) +open import Data.Product using (_,_; swap) +import Function + +open import Categories.Category using (Category) +open import Categories.Category.Monoidal +open import Categories.Category.Monoidal.Braided using (Braided) +import Categories.Category.Monoidal.Braided.Properties as BraidedProperties +import Categories.Category.Monoidal.Symmetric.Properties as SymmetricProperties +open import Categories.Category.Monoidal.Symmetric using (Symmetric) +import Categories.Category.Monoidal.Utilities as MonoidalUtils +import Categories.Morphism as Morphism +import Categories.Morphism.Reasoning as MorphismReasoning +open import Categories.Functor.Bifunctor using (Bifunctor) +open import Categories.NaturalTransformation.NaturalIsomorphism using (niHelper) + +open Category using (Obj) + +module _ {o ℓ e} {C : Category o ℓ e} (M : Monoidal C) where + + private module M = Monoidal M + + open Function using (_∘_) + open Category C using (sym-assoc) + open Category.HomReasoning C using (⟺; _○_) + open Morphism C using (module ≅) + open MorphismReasoning C using (switch-fromtoʳ) + open MonoidalUtils M using (pentagon-inv) + + ⊗ : Bifunctor C C C + ⊗ = record + { F₀ = M.⊗.₀ ∘ swap + ; F₁ = M.⊗.₁ ∘ swap + ; identity = M.⊗.identity + ; homomorphism = M.⊗.homomorphism + ; F-resp-≈ = M.⊗.F-resp-≈ ∘ swap + } + + Reverse-Monoidal : Monoidal C + Reverse-Monoidal = record + { ⊗ = ⊗ + ; unit = M.unit + ; unitorˡ = M.unitorʳ + ; unitorʳ = M.unitorˡ + ; associator = ≅.sym M.associator + ; unitorˡ-commute-from = M.unitorʳ-commute-from + ; unitorˡ-commute-to = M.unitorʳ-commute-to + ; unitorʳ-commute-from = M.unitorˡ-commute-from + ; unitorʳ-commute-to = M.unitorˡ-commute-to + ; assoc-commute-from = M.assoc-commute-to + ; assoc-commute-to = M.assoc-commute-from + ; triangle = ⟺ (switch-fromtoʳ M.associator M.triangle) + ; pentagon = sym-assoc ○ pentagon-inv + } + +module _ {o ℓ e} {C : Category o ℓ e} {M : Monoidal C} where + + open Category C using (assoc; sym-assoc) + open Category.HomReasoning C using (_○_) + + -- The reverse of a braided category is again braided. + + Reverse-Braided : Braided M → Braided (Reverse-Monoidal M) + Reverse-Braided BM = record + { braiding = niHelper (record + { η = braiding.⇐.η + ; η⁻¹ = braiding.⇒.η + ; commute = braiding.⇐.commute + ; iso = λ XY → record + { isoˡ = braiding.iso.isoʳ XY + ; isoʳ = braiding.iso.isoˡ XY } + }) + ; hexagon₁ = sym-assoc ○ hexagon₁-inv ○ assoc + ; hexagon₂ = assoc ○ hexagon₂-inv ○ sym-assoc + } + where + open Braided BM + open BraidedProperties BM using (hexagon₁-inv; hexagon₂-inv) + + -- The reverse of a symmetric category is again symmetric. + + Reverse-Symmetric : Symmetric M → Symmetric (Reverse-Monoidal M) + Reverse-Symmetric SM = record + { braided = Reverse-Braided braided + ; commutative = inv-commutative + } + where + open Symmetric SM using (braided) + open SymmetricProperties SM using (inv-commutative) + +-- Bundled versions of the above + +Reverse-MonoidalCategory : ∀ {o ℓ e} → MonoidalCategory o ℓ e → MonoidalCategory o ℓ e +Reverse-MonoidalCategory C = record + { U = U + ; monoidal = Reverse-Monoidal monoidal + } + where open MonoidalCategory C + +Reverse-BraidedMonoidalCategory : ∀ {o ℓ e} → + BraidedMonoidalCategory o ℓ e → BraidedMonoidalCategory o ℓ e +Reverse-BraidedMonoidalCategory C = record + { U = U + ; monoidal = Reverse-Monoidal monoidal + ; braided = Reverse-Braided braided + } + where open BraidedMonoidalCategory C + +Reverse-SymmetricMonoidalCategory : ∀ {o ℓ e} → + SymmetricMonoidalCategory o ℓ e → SymmetricMonoidalCategory o ℓ e +Reverse-SymmetricMonoidalCategory C = record + { U = U + ; monoidal = Reverse-Monoidal monoidal + ; symmetric = Reverse-Symmetric symmetric + } + where open SymmetricMonoidalCategory C diff --git a/src/Categories/Category/Monoidal/Symmetric/Properties.agda b/src/Categories/Category/Monoidal/Symmetric/Properties.agda new file mode 100644 index 000000000..5bd48e767 --- /dev/null +++ b/src/Categories/Category/Monoidal/Symmetric/Properties.agda @@ -0,0 +1,29 @@ +{-# OPTIONS --without-K --safe #-} + +open import Categories.Category using (Category) +open import Categories.Category.Monoidal using (Monoidal) +open import Categories.Category.Monoidal.Symmetric using (Symmetric) + +module Categories.Category.Monoidal.Symmetric.Properties + {o ℓ e} {C : Category o ℓ e} {M : Monoidal C} (SM : Symmetric M) where + +open import Data.Product using (_,_) + +import Categories.Category.Monoidal.Braided.Properties as BraidedProperties +open import Categories.Morphism.Reasoning C + +open Category C +open HomReasoning +open Symmetric SM + +-- Shorthands for the braiding + +open BraidedProperties braided public using (module Shorthands) + +-- Extra properties of the braiding in a symmetric monoidal category + +braiding-selfInverse : ∀ {X Y} → braiding.⇐.η (X , Y) ≈ braiding.⇒.η (Y , X) +braiding-selfInverse = introʳ commutative ○ cancelˡ (braiding.iso.isoˡ _) + +inv-commutative : ∀ {X Y} → braiding.⇐.η (X , Y) ∘ braiding.⇐.η (Y , X) ≈ id +inv-commutative = ∘-resp-≈ braiding-selfInverse braiding-selfInverse ○ commutative diff --git a/src/Categories/Monad/Commutative.agda b/src/Categories/Monad/Commutative.agda new file mode 100644 index 000000000..2f75e000a --- /dev/null +++ b/src/Categories/Monad/Commutative.agda @@ -0,0 +1,44 @@ +{-# OPTIONS --without-K --safe #-} + +-- Commutative Monad on a braided monoidal category +-- https://ncatlab.org/nlab/show/commutative+monad + +module Categories.Monad.Commutative where + +open import Level +open import Data.Product using (_,_) + +open import Categories.Category.Core using (Category) +open import Categories.Category.Monoidal using (Monoidal) +open import Categories.Category.Monoidal.Braided using (Braided) +open import Categories.Monad using (Monad) +open import Categories.Monad.Strong using (StrongMonad; RightStrength; Strength) +import Categories.Monad.Strong.Properties as StrongProps + +private + variable + o ℓ e : Level + +module _ {C : Category o ℓ e} {V : Monoidal C} (B : Braided V) where + record Commutative (LSM : StrongMonad V) : Set (o ⊔ ℓ ⊔ e) where + open Category C using (_⇒_; _∘_; _≈_) + open Braided B using (_⊗₀_) + open StrongMonad LSM using (M; strength) + open StrongProps.Left.Shorthands strength + + rightStrength : RightStrength V M + rightStrength = StrongProps.Strength⇒RightStrength B strength + + open StrongProps.Right.Shorthands rightStrength + + field + commutes : ∀ {X Y} → M.μ.η (X ⊗₀ Y) ∘ M.F.₁ τ ∘ σ ≈ M.μ.η (X ⊗₀ Y) ∘ M.F.₁ σ ∘ τ + + record CommutativeMonad : Set (o ⊔ ℓ ⊔ e) where + field + strongMonad : StrongMonad V + commutative : Commutative strongMonad + + open StrongMonad strongMonad public + open Commutative commutative public + diff --git a/src/Categories/Monad/Strong.agda b/src/Categories/Monad/Strong.agda index 95dbd0bb3..90ed6353c 100644 --- a/src/Categories/Monad/Strong.agda +++ b/src/Categories/Monad/Strong.agda @@ -22,6 +22,8 @@ private variable o ℓ e : Level +-- (left) strength on a monad + record Strength {C : Category o ℓ e} (V : Monoidal C) (M : Monad C) : Set (o ⊔ ℓ ⊔ e) where open Category C open Monoidal V @@ -42,13 +44,13 @@ record Strength {C : Category o ℓ e} (V : Monoidal C) (M : Monad C) : Set (o -- strengthening with 1 is irrelevant identityˡ : {A : Obj} → F₁ (unitorˡ.from) ∘ t.η (unit , A) ≈ unitorˡ.from -- commutes with unit (of monad) - η-comm : {A B : Obj} → t.η (A , B) ∘ (id ⊗₁ η B) ≈ η (A ⊗₀ B) + η-comm : {A B : Obj} → t.η (A , B) ∘ (id ⊗₁ η B) ≈ η (A ⊗₀ B) -- strength commutes with multiplication μ-η-comm : {A B : Obj} → μ (A ⊗₀ B) ∘ F₁ (t.η (A , B)) ∘ t.η (A , F₀ B) - ≈ t.η (A , B) ∘ id ⊗₁ μ B + ≈ t.η (A , B) ∘ (id ⊗₁ μ B) -- consecutive applications of strength commute (i.e. strength is associative) strength-assoc : {A B C : Obj} → F₁ associator.from ∘ t.η (A ⊗₀ B , C) - ≈ t.η (A , B ⊗₀ C) ∘ id ⊗₁ t.η (B , C) ∘ associator.from + ≈ t.η (A , B ⊗₀ C) ∘ (id ⊗₁ t.η (B , C)) ∘ associator.from record StrongMonad {C : Category o ℓ e} (V : Monoidal C) : Set (o ⊔ ℓ ⊔ e) where field @@ -57,3 +59,41 @@ record StrongMonad {C : Category o ℓ e} (V : Monoidal C) : Set (o ⊔ ℓ ⊔ module M = Monad M open Strength strength public + +-- right strength + +record RightStrength {C : Category o ℓ e} (V : Monoidal C) (M : Monad C) : Set (o ⊔ ℓ ⊔ e) where + open Category C + open Monoidal V + private + module M = Monad M + open M using (F) + open NaturalTransformation M.η using (η) + open NaturalTransformation M.μ renaming (η to μ) + open Functor F + field + strengthen : NaturalTransformation (⊗ ∘F (F ⁂ idF)) (F ∘F ⊗) + + module strengthen = NaturalTransformation strengthen + private + module u = strengthen + + field + -- strengthening with 1 is irrelevant + identityˡ : {A : Obj} → F₁ (unitorʳ.from) ∘ u.η (A , unit) ≈ unitorʳ.from + -- commutes with unit (of monad) + η-comm : {A B : Obj} → u.η (A , B) ∘ (η A ⊗₁ id) ≈ η (A ⊗₀ B) + -- strength commutes with multiplication + μ-η-comm : {A B : Obj} → μ (A ⊗₀ B) ∘ F₁ (u.η (A , B)) ∘ u.η (F₀ A , B) + ≈ u.η (A , B) ∘ (μ A ⊗₁ id) + -- consecutive applications of strength commute (i.e. strength is associative) + strength-assoc : {A B C : Obj} → F₁ associator.to ∘ u.η (A , B ⊗₀ C) + ≈ u.η (A ⊗₀ B , C) ∘ (u.η (A , B) ⊗₁ id) ∘ associator.to + +record RightStrongMonad {C : Category o ℓ e} (V : Monoidal C) : Set (o ⊔ ℓ ⊔ e) where + field + M : Monad C + rightStrength : RightStrength V M + + module M = Monad M + open RightStrength rightStrength public \ No newline at end of file diff --git a/src/Categories/Monad/Strong/Properties.agda b/src/Categories/Monad/Strong/Properties.agda new file mode 100644 index 000000000..9ce9de1b9 --- /dev/null +++ b/src/Categories/Monad/Strong/Properties.agda @@ -0,0 +1,267 @@ +{-# OPTIONS --without-K --safe #-} + +open import Categories.Category using (Category; module Commutation) + +module Categories.Monad.Strong.Properties {o ℓ e} {C : Category o ℓ e} where + +open import Level +open import Data.Product using (_,_; _×_) + +import Categories.Category.Construction.Core as Core +open import Categories.Category.Product +open import Categories.Functor renaming (id to idF) +open import Categories.Category.Monoidal using (Monoidal) +open import Categories.Category.Monoidal.Braided using (Braided) +open import Categories.Category.Monoidal.Construction.Reverse + using (Reverse-Monoidal; Reverse-Braided) +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.Monad using (Monad) +open import Categories.Monad.Strong using (Strength; RightStrength; StrongMonad; RightStrongMonad) +import Categories.Morphism.Reasoning as MR +open import Categories.NaturalTransformation using (NaturalTransformation; ntHelper) + +-- A left strength is a right strength in the reversed category. + +rightInReversed : {V : Monoidal C} {M : Monad C} → + Strength V M → RightStrength (Reverse-Monoidal V) M +rightInReversed left = record + { strengthen = ntHelper (record + { η = λ{ (X , Y) → strengthen.η (Y , X) } + ; commute = λ{ (f , g) → strengthen.commute (g , f) } + }) + ; identityˡ = identityˡ + ; η-comm = η-comm + ; μ-η-comm = μ-η-comm + ; strength-assoc = strength-assoc + } + where open Strength left + +-- A right strength is a left strength in the reversed category. + +leftInReversed : {V : Monoidal C} {M : Monad C} → + RightStrength V M → Strength (Reverse-Monoidal V) M +leftInReversed right = record + { strengthen = ntHelper (record + { η = λ{ (X , Y) → strengthen.η (Y , X) } + ; commute = λ{ (f , g) → strengthen.commute (g , f) } + }) + ; identityˡ = identityˡ + ; η-comm = η-comm + ; μ-η-comm = μ-η-comm + ; strength-assoc = strength-assoc + } + where open RightStrength right + +open Category C hiding (identityˡ) +open MR C +open Commutation C + +module Left {V : Monoidal C} {M : Monad C} (left : Strength V M) where + open Category C using (identityˡ) + open Monoidal V using (_⊗₀_) + open MonoidalUtils V using (_⊗ᵢ_) + open Core.Shorthands C -- for idᵢ, _∘ᵢ_, ... + open MonoidalUtils.Shorthands V -- for λ⇒, ρ⇒, α⇒, ... + open MonoidalReasoning V + open Monad M using (F; μ; η) + + private + module left = Strength left + variable + X Y Z W : Obj + + module Shorthands where + module σ = left.strengthen + + σ : ∀ {X Y} → X ⊗₀ F.₀ Y ⇒ F.₀ (X ⊗₀ Y) + σ {X} {Y} = σ.η (X , Y) + + open Shorthands + + -- In a braided monoidal category, a left strength induces a right strength. + + module _ (BV : Braided V) where + open Braided BV hiding (_⊗₀_) + open BraidedProps BV using (braiding-coherence; inv-braiding-coherence; assoc-reverse) + open BraidedProps.Shorthands BV renaming (σ to B; σ⇒ to B⇒; σ⇐ to B⇐) + + private + τ : ∀ {X Y} → F.₀ X ⊗₀ Y ⇒ F.₀ (X ⊗₀ Y) + τ {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 (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 + { η = λ _ → τ + ; commute = λ (f , g) → τ-commute f g + }) + + private module τ = NaturalTransformation right-strengthen + + -- The strengths commute with braiding. + + left-right-braiding-comm : ∀ {X Y} → F.₁ B⇐ ∘ σ {X} {Y} ≈ τ ∘ B⇐ + left-right-braiding-comm = begin + 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-≈ (braiding.iso.isoʳ _) ⟩∘⟨refl ⟩ + F.₁ id ∘ σ ∘ B⇒ ≈⟨ elimˡ F.identity ⟩ + σ ∘ B⇒ ∎ + + right-identityˡ : ∀ {X} → F.₁ ρ⇒ ∘ τ {X} {unit} ≈ ρ⇒ + right-identityˡ = begin + F.₁ ρ⇒ ∘ F.₁ B⇐ ∘ σ ∘ B⇒ ≈⟨ pullˡ (⟺ F.homomorphism) ⟩ + F.₁ (ρ⇒ ∘ B⇐) ∘ σ ∘ B⇒ ≈⟨ F.F-resp-≈ (inv-braiding-coherence) ⟩∘⟨refl ⟩ + F.₁ λ⇒ ∘ σ ∘ B⇒ ≈⟨ pullˡ left.identityˡ ⟩ + λ⇒ ∘ B⇒ ≈⟨ braiding-coherence ⟩ + ρ⇒ ∎ + + -- The induced right strength commutes with the monad unit. + + right-η-comm : ∀ {X Y} → τ ∘ η.η X ⊗₁ id ≈ η.η (X ⊗₀ Y) + right-η-comm {X} {Y} = begin + (F.₁ B⇐ ∘ σ ∘ B⇒) ∘ (η.η X ⊗₁ id) ≈⟨ pullʳ (pullʳ (braiding.⇒.commute (η.η X , id))) ⟩ + F.₁ B⇐ ∘ σ ∘ (id ⊗₁ η.η X) ∘ B⇒ ≈⟨ refl⟩∘⟨ pullˡ left.η-comm ⟩ + F.₁ B⇐ ∘ η.η (Y ⊗₀ X) ∘ B⇒ ≈⟨ pullˡ (⟺ (η.commute B⇐)) ⟩ + (η.η (X ⊗₀ Y) ∘ B⇐) ∘ B⇒ ≈⟨ cancelʳ (braiding.iso.isoˡ _) ⟩ + η.η (X ⊗₀ Y) ∎ + + -- The induced right strength commutes with the monad multiplication. + + right-μ-η-comm : ∀ {X Y} → μ.η (X ⊗₀ Y) ∘ F.₁ τ ∘ τ ≈ τ ∘ μ.η X ⊗₁ id + right-μ-η-comm {X} {Y} = begin + μ.η (X ⊗₀ Y) ∘ F.₁ τ ∘ F.₁ B⇐ ∘ σ ∘ B⇒ ≈⟨ refl⟩∘⟨ pullˡ (⟺ F.homomorphism) ⟩ + μ.η (X ⊗₀ Y) ∘ F.₁ (τ ∘ B⇐) ∘ σ ∘ B⇒ ≈⟨ refl⟩∘⟨ (F.F-resp-≈ (pullʳ (cancelʳ (braiding.iso.isoʳ _))) ⟩∘⟨refl) ⟩ + μ.η (X ⊗₀ Y) ∘ F.₁ (F.₁ B⇐ ∘ σ) ∘ σ ∘ B⇒ ≈⟨ refl⟩∘⟨ F.homomorphism ⟩∘⟨refl ⟩ + μ.η (X ⊗₀ Y) ∘ (F.₁ (F.₁ B⇐) ∘ F.₁ σ) ∘ σ ∘ B⇒ ≈⟨ pullˡ (pullˡ (μ.commute B⇐)) ⟩ + ((F.₁ B⇐ ∘ μ.η (Y ⊗₀ X)) ∘ F.₁ σ) ∘ σ ∘ B⇒ ≈⟨ assoc² ○ (refl⟩∘⟨ ⟺ assoc²') ⟩ + F.₁ B⇐ ∘ (μ.η (Y ⊗₀ X) ∘ F.₁ σ ∘ σ) ∘ B⇒ ≈⟨ refl⟩∘⟨ pushˡ left.μ-η-comm ⟩ + F.₁ B⇐ ∘ σ ∘ (id ⊗₁ μ.η X) ∘ B⇒ ≈˘⟨ pullʳ (pullʳ (braiding.⇒.commute (μ.η X , id))) ⟩ + τ ∘ μ.η X ⊗₁ id ∎ + + -- The induced right strength commutes with the associator + + right-strength-assoc : [ F.₀ X ⊗₀ (Y ⊗₀ Z) ⇒ F.₀ ((X ⊗₀ Y) ⊗₀ Z) ]⟨ + τ ⇒⟨ F.₀ (X ⊗₀ (Y ⊗₀ Z)) ⟩ + F.₁ α⇐ + ≈ α⇐ ⇒⟨ (F.₀ X ⊗₀ Y) ⊗₀ Z ⟩ + τ ⊗₁ id ⇒⟨ F.₀ (X ⊗₀ Y) ⊗₀ Z ⟩ + τ + ⟩ + right-strength-assoc = begin + F.₁ α⇐ ∘ τ + ≈˘⟨ F.F-resp-≈ assoc-reverse ⟩∘⟨refl ⟩ + F.₁ (B⇐ ∘ id ⊗₁ B⇐ ∘ α⇒ ∘ B⇒ ∘ id ⊗₁ B⇒) ∘ τ + ≈⟨ pushˡ F.homomorphism ⟩ + F.₁ B⇐ ∘ F.₁ (id ⊗₁ B⇐ ∘ α⇒ ∘ 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⇒) ∘ τ + ≈˘⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ τ.commute (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⇒ + ≈⟨ refl⟩∘⟨ refl⟩∘⟨ extendʳ left.strength-assoc ⟩ + 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⇒ + ≈⟨ extendʳ left-right-braiding-comm ⟩ + τ ∘ 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⟩∘⟨ Equiv.refl ⟩∘⟨ (refl⟩⊗⟨ Equiv.refl) ⟩∘⟨refl ⟩ + τ ∘ τ ⊗₁ id ∘ B⇐ ∘ id ⊗₁ B⇐ ∘ α⇒ ∘ B⇒ ∘ id ⊗₁ B⇒ + ≈⟨ refl⟩∘⟨ refl⟩∘⟨ assoc-reverse ⟩ + τ ∘ τ ⊗₁ id ∘ α⇐ + ∎ + + -- The induced right strength + + right : RightStrength V M + right = record + { strengthen = right-strengthen + ; identityˡ = right-identityˡ + ; η-comm = right-η-comm + ; μ-η-comm = right-μ-η-comm + ; strength-assoc = right-strength-assoc + } + +Strength⇒RightStrength : {V : Monoidal C} {M : Monad C} → + Braided V → Strength V M → RightStrength V M +Strength⇒RightStrength BV left = Left.right left BV + +StrongMonad⇒RightStrongMonad : {V : Monoidal C} → + Braided V → StrongMonad V → RightStrongMonad V +StrongMonad⇒RightStrongMonad BV SM = record + { M = M + ; rightStrength = Strength⇒RightStrength BV strength + } + where open StrongMonad SM + +module Right {V : Monoidal C} {M : Monad C} (right : RightStrength V M) where + open Monoidal V using (_⊗₀_) + open Monad M using (F) + + module Shorthands where + module τ = RightStrength.strengthen right + + τ : ∀ {X Y} → F.₀ X ⊗₀ Y ⇒ F.₀ (X ⊗₀ Y) + τ {X} {Y} = τ.η (X , Y) + +-- In a braided monoidal category, a right strength induces a left strength. + +RightStrength⇒Strength : {V : Monoidal C} {M : Monad C} → + Braided V → RightStrength V M → Strength V M +RightStrength⇒Strength {V} {M} BV right = record + { strengthen = strengthen + ; identityˡ = identityˡ + ; η-comm = η-comm + ; μ-η-comm = μ-η-comm + ; strength-assoc = strength-assoc + } + where + left₁ : Strength (Reverse-Monoidal V) M + left₁ = leftInReversed right + + right₂ : RightStrength (Reverse-Monoidal V) M + right₂ = Strength⇒RightStrength (Reverse-Braided BV) left₁ + + -- Note: this is almost what we need, but Reverse-Monoidal is + -- not a strict involution (some of the coherence laws are + -- have proofs that are not strictly identical to their + -- original counterparts). But this does not matter + -- structurally, so we can just re-package the components we + -- need. + left₂ : Strength (Reverse-Monoidal (Reverse-Monoidal V)) M + left₂ = leftInReversed right₂ + + open Strength left₂ + +RightStrongMonad⇒StrongMonad : {V : Monoidal C} → + Braided V → RightStrongMonad V → StrongMonad V +RightStrongMonad⇒StrongMonad BV RSM = record + { M = M + ; strength = RightStrength⇒Strength BV rightStrength + } + where open RightStrongMonad RSM