{-# OPTIONS --without-K --safe #-}
module Categories.Category.Monoidal.Construction.Kleisli where
open import Level
open import Data.Product using (_,_)
open import Categories.Category.Core using (Category)
open import Categories.Monad using (Monad)
open import Categories.Monad.Strong using (Strength; RightStrength)
open import Categories.Monad.Commutative using (CommutativeMonad)
open import Categories.Monad.Commutative.Properties using (module CommutativeProperties; module SymmetricProperties)
open import Categories.Category.Construction.Kleisli using (Kleisli; module TripleNotation)
open import Categories.Category.Monoidal using (Monoidal)
open import Categories.Category.Monoidal.Symmetric using (Symmetric)
open import Categories.Functor.Bifunctor using (Bifunctor)
import Categories.Morphism as MC
import Categories.Morphism.Reasoning as MR
import Categories.Monad.Strong.Properties as StrongProps
import Categories.Category.Monoidal.Utilities as MonoidalUtils
private
variable
o ℓ e : Level
module _ {𝒞 : Category o ℓ e} {monoidal : Monoidal 𝒞} (symmetric : Symmetric monoidal) (CM : CommutativeMonad (Symmetric.braided symmetric)) where
open Category 𝒞
open MR 𝒞
open HomReasoning
open Equiv
open CommutativeMonad CM hiding (identityˡ)
open Monad M using (μ)
open TripleNotation M
open StrongProps.Left.Shorthands strength
open StrongProps.Right.Shorthands rightStrength
open MonoidalUtils.Shorthands monoidal using (α⇒; α⇐; λ⇒; λ⇐; ρ⇒; ρ⇐)
open Symmetric symmetric
open CommutativeProperties braided CM
open SymmetricProperties symmetric CM
open MC (Kleisli M) using (_≅_)
⊗' : Bifunctor (Kleisli M) (Kleisli M) (Kleisli M)
⊗' = record
{ F₀ = λ (X , Y) → X ⊗₀ Y
; F₁ = λ (f , g) → ψ ∘ (f ⊗₁ g)
; identity = identity'
; homomorphism = λ {(X₁ , X₂)} {(Y₁ , Y₂)} {(Z₁ , Z₂)} {(f , g)} {(h , i)} → homomorphism' {X₁} {X₂} {Y₁} {Y₂} {Z₁} {Z₂} {f} {g} {h} {i}
; F-resp-≈ = λ (f≈g , h≈i) → ∘-resp-≈ʳ (⊗.F-resp-≈ (f≈g , h≈i))
}
where
identity' : ∀ {X} {Y} → ψ ∘ (η {X} ⊗₁ η {Y}) ≈ η
identity' = begin
(τ * ∘ σ) ∘ (η ⊗₁ η) ≈˘⟨ refl⟩∘⟨ (sym ⊗.homomorphism ○ ⊗.F-resp-≈ (identityˡ , identityʳ)) ⟩
(τ * ∘ σ) ∘ (id ⊗₁ η) ∘ (η ⊗₁ id) ≈⟨ pullʳ (pullˡ η-comm) ⟩
τ * ∘ η ∘ (η ⊗₁ id) ≈⟨ pullˡ *-identityʳ ⟩
τ ∘ (η ⊗₁ id) ≈⟨ RightStrength.η-comm rightStrength ⟩
η ∎
homomorphism' : ∀ {X₁ X₂ Y₁ Y₂ Z₁ Z₂ : Obj} {f : X₁ ⇒ M.F.₀ Y₁} {g : X₂ ⇒ M.F.₀ Y₂} {h : Y₁ ⇒ M.F.₀ Z₁} {i : Y₂ ⇒ M.F.₀ Z₂} → ψ ∘ ((h * ∘ f) ⊗₁ (i * ∘ g)) ≈ (ψ ∘ (h ⊗₁ i)) * ∘ ψ ∘ (f ⊗₁ g)
homomorphism' {f = f} {g} {h} {i} = begin
ψ ∘ ((h * ∘ f) ⊗₁ (i * ∘ g)) ≈˘⟨ refl⟩∘⟨ (pullˡ (sym ⊗.homomorphism) ○ sym ⊗.homomorphism) ⟩
ψ ∘ (μ.η _ ⊗₁ μ.η _) ∘ (M.F.₁ h ⊗₁ M.F.₁ i) ∘ (f ⊗₁ g) ≈˘⟨ extendʳ ψ-μ ⟩
ψ * ∘ ψ ∘ (M.F.₁ h ⊗₁ M.F.₁ i) ∘ (f ⊗₁ g) ≈⟨ refl⟩∘⟨ extendʳ ψ-comm ⟩
ψ * ∘ M.F.₁ (h ⊗₁ i) ∘ ψ ∘ (f ⊗₁ g) ≈⟨ pullˡ *∘F₁ ⟩
(ψ ∘ (h ⊗₁ i)) * ∘ ψ ∘ (f ⊗₁ g) ∎
unitorˡ' : ∀ {X} → unit ⊗₀ X ≅ X
unitorˡ' = record { from = η ∘ λ⇒ ; to = η ∘ λ⇐ ; iso = record
{ isoˡ = pullˡ *-identityʳ ○ cancelʳ unitorˡ.isoˡ
; isoʳ = pullˡ *-identityʳ ○ cancelʳ unitorˡ.isoʳ
} }
unitorʳ' : ∀ {X} → X ⊗₀ unit ≅ X
unitorʳ' = record { from = η ∘ ρ⇒ ; to = η ∘ ρ⇐ ; iso = record
{ isoˡ = pullˡ *-identityʳ ○ cancelʳ unitorʳ.isoˡ
; isoʳ = pullˡ *-identityʳ ○ cancelʳ unitorʳ.isoʳ
} }
associator' : ∀ {X Y Z} → (X ⊗₀ Y) ⊗₀ Z ≅ X ⊗₀ (Y ⊗₀ Z)
associator' = record { from = η ∘ α⇒ ; to = η ∘ α⇐ ; iso = record
{ isoˡ = pullˡ *-identityʳ ○ cancelʳ associator.isoˡ
; isoʳ = pullˡ *-identityʳ ○ cancelʳ associator.isoʳ
} }
Kleisli-Monoidal : Monoidal (Kleisli M)
Kleisli-Monoidal = record
{ ⊗ = ⊗'
; unit = unit
; unitorˡ = unitorˡ'
; unitorʳ = unitorʳ'
; associator = associator'
; unitorˡ-commute-from = unitorˡ-commute-from'
; unitorˡ-commute-to = unitorˡ-commute-to'
; unitorʳ-commute-from = unitorʳ-commute-from'
; unitorʳ-commute-to = unitorʳ-commute-to'
; assoc-commute-from = assoc-commute-from'
; assoc-commute-to = assoc-commute-to'
; triangle = triangle'
; pentagon = pentagon'
}
where
unitorˡ-commute-from' : ∀ {X} {Y} {f : X ⇒ M.F.₀ Y} → (η ∘ λ⇒) * ∘ ψ ∘ (η ⊗₁ f) ≈ f * ∘ η ∘ λ⇒
unitorˡ-commute-from' {f = f} = begin
(η ∘ λ⇒) * ∘ ψ ∘ (η ⊗₁ f) ≈⟨ *⇒F₁ ⟩∘⟨ ψ-σ' ⟩
M.F.₁ λ⇒ ∘ σ ∘ (id ⊗₁ f) ≈⟨ pullˡ (Strength.identityˡ strength) ⟩
λ⇒ ∘ (id ⊗₁ f) ≈⟨ unitorˡ-commute-from ⟩
f ∘ λ⇒ ≈˘⟨ pullˡ *-identityʳ ⟩
f * ∘ η ∘ λ⇒ ∎
unitorˡ-commute-to' : ∀ {X} {Y} {f : X ⇒ M.F.₀ Y} → (η ∘ λ⇐) * ∘ f ≈ (ψ ∘ (η ⊗₁ f)) * ∘ η ∘ λ⇐
unitorˡ-commute-to' {f = f} = begin
(η ∘ λ⇐) * ∘ f ≈⟨ *⇒F₁ ⟩∘⟨refl ⟩
M.F.₁ λ⇐ ∘ f ≈˘⟨ refl⟩∘⟨ (cancelˡ unitorˡ.isoʳ) ⟩
M.F.₁ λ⇐ ∘ λ⇒ ∘ λ⇐ ∘ f ≈˘⟨ pullʳ (pullˡ (Strength.identityˡ strength)) ⟩
(M.F.₁ λ⇐ ∘ M.F.₁ λ⇒) ∘ σ ∘ λ⇐ ∘ f ≈⟨ elimˡ (sym M.F.homomorphism ○ (M.F.F-resp-≈ unitorˡ.isoˡ ○ M.F.identity)) ⟩
σ ∘ λ⇐ ∘ f ≈˘⟨ pullʳ (sym unitorˡ-commute-to) ⟩
(σ ∘ (id ⊗₁ f)) ∘ λ⇐ ≈˘⟨ ψ-σ' ⟩∘⟨refl ⟩
(ψ ∘ (η ⊗₁ f)) ∘ λ⇐ ≈˘⟨ pullˡ *-identityʳ ⟩
(ψ ∘ (η ⊗₁ f)) * ∘ η ∘ λ⇐ ∎
unitorʳ-commute-from' : ∀ {X} {Y} {f : X ⇒ M.F.₀ Y} → (η ∘ ρ⇒) * ∘ ψ ∘ (f ⊗₁ η) ≈ f * ∘ η ∘ ρ⇒
unitorʳ-commute-from' {f = f} = begin
(η ∘ ρ⇒) * ∘ ψ ∘ (f ⊗₁ η) ≈⟨ *⇒F₁ ⟩∘⟨ ψ-τ' ⟩
M.F.₁ ρ⇒ ∘ τ ∘ (f ⊗₁ id) ≈⟨ pullˡ (RightStrength.identityˡ rightStrength) ⟩
ρ⇒ ∘ (f ⊗₁ id) ≈⟨ unitorʳ-commute-from ⟩
f ∘ ρ⇒ ≈˘⟨ pullˡ *-identityʳ ⟩
f * ∘ η ∘ ρ⇒ ∎
unitorʳ-commute-to' : ∀ {X} {Y} {f : X ⇒ M.F.₀ Y} → (η ∘ ρ⇐) * ∘ f ≈ (ψ ∘ (f ⊗₁ η)) * ∘ η ∘ ρ⇐
unitorʳ-commute-to' {f = f} = begin
(η ∘ ρ⇐) * ∘ f ≈⟨ *⇒F₁ ⟩∘⟨refl ⟩
M.F.₁ ρ⇐ ∘ f ≈˘⟨ refl⟩∘⟨ (cancelˡ unitorʳ.isoʳ) ⟩
M.F.₁ ρ⇐ ∘ ρ⇒ ∘ ρ⇐ ∘ f ≈˘⟨ pullʳ (pullˡ (RightStrength.identityˡ rightStrength)) ⟩
(M.F.₁ ρ⇐ ∘ M.F.₁ ρ⇒) ∘ τ ∘ ρ⇐ ∘ f ≈⟨ elimˡ (sym M.F.homomorphism ○ (M.F.F-resp-≈ unitorʳ.isoˡ ○ M.F.identity)) ⟩
τ ∘ ρ⇐ ∘ f ≈˘⟨ pullʳ (sym unitorʳ-commute-to) ⟩
(τ ∘ (f ⊗₁ id)) ∘ ρ⇐ ≈˘⟨ ψ-τ' ⟩∘⟨refl ⟩
(ψ ∘ (f ⊗₁ η)) ∘ ρ⇐ ≈˘⟨ pullˡ *-identityʳ ⟩
(ψ ∘ (f ⊗₁ η)) * ∘ η ∘ ρ⇐ ∎
assoc-commute-from' : ∀ {X Y} {f : X ⇒ M.F.₀ Y} {A B} {g : A ⇒ M.F.₀ B} {U V} {h : U ⇒ M.F.₀ V} → (η ∘ α⇒) * ∘ ψ ∘ ((ψ ∘ (f ⊗₁ g)) ⊗₁ h) ≈ (ψ ∘ (f ⊗₁ (ψ ∘ (g ⊗₁ h)))) * ∘ (η ∘ α⇒)
assoc-commute-from' {f = f} {g = g} {h = h} = begin
(η ∘ α⇒) * ∘ ψ ∘ ((ψ ∘ (f ⊗₁ g)) ⊗₁ h) ≈⟨ *⇒F₁ ⟩∘⟨refl ⟩
M.F.₁ α⇒ ∘ ψ ∘ ((ψ ∘ (f ⊗₁ g)) ⊗₁ h) ≈˘⟨ refl⟩∘⟨ refl⟩∘⟨ (sym ⊗.homomorphism ○ ⊗.F-resp-≈ (refl , identityˡ)) ⟩
M.F.₁ α⇒ ∘ ψ ∘ (ψ ⊗₁ id) ∘ ((f ⊗₁ g) ⊗₁ h) ≈⟨ (sym-assoc ○ pullˡ (assoc ○ ψ-assoc-from) ○ assoc²βε) ⟩
ψ ∘ (id ⊗₁ ψ) ∘ α⇒ ∘ ((f ⊗₁ g) ⊗₁ h) ≈˘⟨ pullʳ (pullʳ (sym assoc-commute-from)) ⟩
(ψ ∘ (id ⊗₁ ψ) ∘ (f ⊗₁ (g ⊗₁ h))) ∘ α⇒ ≈⟨ (refl⟩∘⟨ (sym ⊗.homomorphism ○ ⊗.F-resp-≈ (identityˡ , refl))) ⟩∘⟨refl ⟩
(ψ ∘ (f ⊗₁ (ψ ∘ (g ⊗₁ h)))) ∘ α⇒ ≈˘⟨ pullˡ *-identityʳ ⟩
(ψ ∘ (f ⊗₁ (ψ ∘ (g ⊗₁ h)))) * ∘ (η ∘ α⇒) ∎
assoc-commute-to' : ∀ {X Y} {f : X ⇒ M.F.₀ Y} {A B} {g : A ⇒ M.F.₀ B} {U V} {h : U ⇒ M.F.₀ V} → (η ∘ α⇐) * ∘ ψ ∘ (f ⊗₁ (ψ ∘ (g ⊗₁ h))) ≈ (ψ ∘ ((ψ ∘ (f ⊗₁ g)) ⊗₁ h)) * ∘ (η ∘ α⇐)
assoc-commute-to' {f = f} {g = g} {h = h} = begin
(η ∘ α⇐) * ∘ ψ ∘ (f ⊗₁ (ψ ∘ (g ⊗₁ h))) ≈⟨ *⇒F₁ ⟩∘⟨refl ⟩
M.F.₁ α⇐ ∘ ψ ∘ (f ⊗₁ (ψ ∘ (g ⊗₁ h))) ≈˘⟨ refl⟩∘⟨ refl⟩∘⟨ (sym ⊗.homomorphism ○ ⊗.F-resp-≈ (identityˡ , refl)) ⟩
M.F.₁ α⇐ ∘ ψ ∘ (id ⊗₁ ψ) ∘ (f ⊗₁ (g ⊗₁ h)) ≈⟨ (sym-assoc ○ (pullˡ (assoc ○ ψ-assoc-to) ○ assoc²βε)) ⟩
ψ ∘ (ψ ⊗₁ id) ∘ α⇐ ∘ (f ⊗₁ (g ⊗₁ h)) ≈˘⟨ pullʳ (pullʳ (sym assoc-commute-to)) ⟩
(ψ ∘ (ψ ⊗₁ id) ∘ ((f ⊗₁ g) ⊗₁ h)) ∘ α⇐ ≈⟨ (refl⟩∘⟨ (sym ⊗.homomorphism ○ ⊗.F-resp-≈ (refl , identityˡ))) ⟩∘⟨refl ⟩
(ψ ∘ ((ψ ∘ (f ⊗₁ g)) ⊗₁ h)) ∘ α⇐ ≈˘⟨ pullˡ *-identityʳ ⟩
(ψ ∘ ((ψ ∘ (f ⊗₁ g)) ⊗₁ h)) * ∘ (η ∘ α⇐) ∎
triangle' : ∀ {X} {Y} → (ψ ∘ (η {X} ⊗₁ (η ∘ λ⇒))) * ∘ (η ∘ α⇒) ≈ ψ ∘ ((η ∘ ρ⇒) ⊗₁ η {Y})
triangle' = begin
(ψ ∘ (η ⊗₁ (η ∘ λ⇒))) * ∘ (η ∘ α⇒) ≈⟨ pullˡ *-identityʳ ⟩
(ψ ∘ (η ⊗₁ (η ∘ λ⇒))) ∘ α⇒ ≈˘⟨ pullˡ (pullʳ (sym ⊗.homomorphism ○ ⊗.F-resp-≈ (identityʳ , refl))) ⟩
(ψ ∘ (η ⊗₁ η)) ∘ (id ⊗₁ λ⇒) ∘ α⇒ ≈⟨ (refl⟩∘⟨ triangle) ⟩
(ψ ∘ (η ⊗₁ η)) ∘ (ρ⇒ ⊗₁ id) ≈⟨ pullʳ (sym ⊗.homomorphism ○ ⊗.F-resp-≈ (refl , identityʳ)) ⟩
ψ ∘ ((η ∘ ρ⇒) ⊗₁ η) ∎
pentagon' : ∀ {A B C D : Obj} → (ψ {A} {B ⊗₀ (C ⊗₀ D)} ∘ (η ⊗₁ (η ∘ α⇒))) * ∘ (η ∘ α⇒) * ∘ (ψ ∘ ((η ∘ α⇒) ⊗₁ η)) ≈ (η ∘ α⇒) * ∘ (η ∘ α⇒)
pentagon' = begin
(ψ ∘ (η ⊗₁ (η ∘ α⇒))) * ∘ (η ∘ α⇒) * ∘ (ψ ∘ ((η ∘ α⇒) ⊗₁ η))
≈⟨ refl⟩∘⟨ *⇒F₁ ⟩∘⟨refl ⟩
(ψ ∘ (η ⊗₁ (η ∘ α⇒))) * ∘ M.F.₁ α⇒ ∘ (ψ ∘ ((η ∘ α⇒) ⊗₁ η))
≈⟨ pullˡ (*∘F₁ ○ *-resp-≈ assoc) ⟩
(ψ ∘ (η ⊗₁ (η ∘ α⇒)) ∘ α⇒) * ∘ (ψ ∘ ((η ∘ α⇒) ⊗₁ η))
≈˘⟨ refl⟩∘⟨ refl⟩∘⟨ (sym ⊗.homomorphism ○ ⊗.F-resp-≈ (refl , identityʳ)) ⟩
(ψ ∘ (η ⊗₁ (η ∘ α⇒)) ∘ α⇒) * ∘ (ψ ∘ (η ⊗₁ η) ∘ (α⇒ ⊗₁ id))
≈⟨ refl⟩∘⟨ pullˡ ψ-η ⟩
(ψ ∘ (η ⊗₁ (η ∘ α⇒)) ∘ α⇒) * ∘ (η ∘ (α⇒ ⊗₁ id))
≈⟨ pullˡ *-identityʳ ⟩
(ψ ∘ (η ⊗₁ (η ∘ α⇒)) ∘ α⇒) ∘ (α⇒ ⊗₁ id)
≈˘⟨ sym-assoc ○ (∘-resp-≈ʳ sym-assoc ○ pullˡ (pullʳ (pullˡ (sym ⊗.homomorphism ○ ⊗.F-resp-≈ (identityʳ , refl))))) ⟩
ψ ∘ (η ⊗₁ η) ∘ (id ⊗₁ α⇒) ∘ α⇒ ∘ (α⇒ ⊗₁ id)
≈⟨ (refl⟩∘⟨ refl⟩∘⟨ pentagon) ⟩
ψ ∘ (η ⊗₁ η) ∘ (α⇒ ∘ α⇒)
≈⟨ (pullˡ ψ-η) ○ sym-assoc ⟩
(η ∘ α⇒) ∘ α⇒
≈˘⟨ pullˡ *-identityʳ ⟩
(η ∘ α⇒) * ∘ (η ∘ α⇒)
∎