{-# OPTIONS --without-K --safe #-}
module Categories.Monad.Commutative where
open import Level using (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
import Categories.Category.Monoidal.Braided.Properties as BraidedProps
import Categories.Morphism.Reasoning as MR
private
variable
o ℓ e : Level
module _ {C : Category o ℓ e} {V : Monoidal C} (BV : Braided V) where
record Commutative (LSM : StrongMonad V) : Set (o ⊔ ℓ ⊔ e) where
open Category C using (_⇒_; _∘_; _≈_; module HomReasoning; module Equiv)
open Braided BV using (_⊗₀_)
open StrongMonad LSM using (M; strength)
open StrongProps.Left.Shorthands strength
open BraidedProps.Shorthands BV renaming (σ to B; σ⇒ to B⇒; σ⇐ to B⇐)
rightStrength : RightStrength V M
rightStrength = StrongProps.Strength⇒RightStrength BV strength
open StrongProps.Right.Shorthands rightStrength
field
commutes : ∀ {X Y} → (M.μ.η (X ⊗₀ Y) ∘ M.F.₁ τ) ∘ σ ≈ (M.μ.η (X ⊗₀ Y) ∘ M.F.₁ σ) ∘ τ
σ-τ : ∀ {X} {Y} → σ {X} {Y} ≈ M.F.₁ B⇒ ∘ τ ∘ B⇐
σ-τ = begin
σ ≈˘⟨ cancelʳ (Braided.braiding.iso.isoʳ BV _) ⟩
(σ ∘ B⇒) ∘ B⇐ ≈˘⟨ pullˡ (cancelˡ (sym M.F.homomorphism ○ M.F.F-resp-≈ (Braided.braiding.iso.isoʳ BV _) ○ M.F.identity)) ⟩
M.F.₁ B⇒ ∘ (M.F.₁ B⇐ ∘ σ ∘ B⇒) ∘ B⇐ ∎
where
open HomReasoning
open MR C
open Equiv
record CommutativeMonad : Set (o ⊔ ℓ ⊔ e) where
field
strongMonad : StrongMonad V
commutative : Commutative strongMonad
open StrongMonad strongMonad public
open Commutative commutative public