{-# OPTIONS --without-K --safe #-}
module Categories.Monad.Strong where
open import Level using (Level; _⊔_)
open import Data.Product using (_,_)
open import Categories.Category.Core using (Category)
open import Categories.Functor using (Functor; _∘F_) renaming (id to idF)
open import Categories.Category.Monoidal using (Monoidal)
open import Categories.Category.Product using (_⁂_)
open import Categories.NaturalTransformation using (NaturalTransformation)
open import Categories.Monad using (Monad)
import Categories.Category.Monoidal.Reasoning as MonoidalReasoning
private
variable
o ℓ e : Level
record Strength {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 (idF ⁂ F)) (F ∘F ⊗)
module strengthen = NaturalTransformation strengthen
private
module t = strengthen
field
identityˡ : {A : Obj} → F₁ (unitorˡ.from) ∘ t.η (unit , A) ≈ unitorˡ.from
η-comm : {A B : Obj} → t.η (A , B) ∘ (id ⊗₁ η B) ≈ η (A ⊗₀ B)
μ-η-comm : {A B : Obj} → μ (A ⊗₀ B) ∘ F₁ (t.η (A , B)) ∘ t.η (A , F₀ B)
≈ t.η (A , B) ∘ (id ⊗₁ μ B)
strength-assoc : {A B C : Obj} → F₁ associator.from ∘ t.η (A ⊗₀ B , C)
≈ t.η (A , B ⊗₀ C) ∘ (id ⊗₁ t.η (B , C)) ∘ associator.from
strength-natural-id : ∀ {X Y Z} (f : X ⇒ Y) → t.η (Y , Z) ∘ (f ⊗₁ id) ≈ F₁ (f ⊗₁ id) ∘ t.η (X , Z)
strength-natural-id f = begin
t.η _ ∘ (f ⊗₁ id) ≈˘⟨ refl⟩∘⟨ refl⟩⊗⟨ identity ⟩
t.η _ ∘ (f ⊗₁ F₁ id) ≈⟨ t.commute (f , id) ⟩
F₁ (f ⊗₁ id) ∘ t.η _ ∎
where
open HomReasoning
open MonoidalReasoning V using (refl⟩⊗⟨_)
record StrongMonad {C : Category o ℓ e} (V : Monoidal C) : Set (o ⊔ ℓ ⊔ e) where
field
M : Monad C
strength : Strength V M
module M = Monad M
open Strength strength public
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
identityˡ : {A : Obj} → F₁ (unitorʳ.from) ∘ u.η (A , unit) ≈ unitorʳ.from
η-comm : {A B : Obj} → u.η (A , B) ∘ (η A ⊗₁ id) ≈ η (A ⊗₀ B)
μ-η-comm : {A B : Obj} → μ (A ⊗₀ B) ∘ F₁ (u.η (A , B)) ∘ u.η (F₀ A , B)
≈ u.η (A , B) ∘ (μ A ⊗₁ id)
strength-assoc : {A B C : Obj} → F₁ associator.to ∘ u.η (A , B ⊗₀ C)
≈ u.η (A ⊗₀ B , C) ∘ (u.η (A , B) ⊗₁ id) ∘ associator.to
strength-natural-id : ∀ {X Y Z} (f : X ⇒ Y) → u.η (Z , Y) ∘ (id ⊗₁ f) ≈ F₁ (id ⊗₁ f) ∘ u.η (Z , X)
strength-natural-id f = begin
u.η _ ∘ (id ⊗₁ f) ≈˘⟨ refl⟩∘⟨ identity ⟩⊗⟨refl ⟩
u.η _ ∘ (F₁ id ⊗₁ f) ≈⟨ u.commute (id , f) ⟩
F₁ (id ⊗₁ f) ∘ u.η _ ∎
where
open HomReasoning
open MonoidalReasoning V using (_⟩⊗⟨refl)
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