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