{-# OPTIONS --without-K --safe #-}
module Categories.Category.Monoidal.Construction.Kleisli.Symmetric where
open import Level
open import Data.Product using (_,_)
open import Categories.Category.Core using (Category)
open import Categories.Functor.Bifunctor using (flip-bifunctor)
open import Categories.Monad using (Monad)
open import Categories.Monad.Commutative using (CommutativeMonad)
open import Categories.Monad.Commutative.Properties using (module CommutativeProperties)
open import Categories.NaturalTransformation.NaturalIsomorphism using (NaturalIsomorphism)
open import Categories.NaturalTransformation using (ntHelper)
open import Categories.Category.Monoidal using (Monoidal)
open import Categories.Category.Monoidal.Braided using (Braided)
open import Categories.Category.Monoidal.Symmetric using (Symmetric)
open import Categories.Category.Construction.Kleisli using (module TripleNotation)
open import Categories.Category.Monoidal.Construction.Kleisli using (Kleisli-Monoidal; ⊗')
import Categories.Morphism.Reasoning as MR
import Categories.Monad.Strong.Properties as StrongProps
import Categories.Category.Monoidal.Symmetric.Properties as SymmProps
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 strength using (left-right-braiding-comm; right-left-braiding-comm)
open StrongProps.Left.Shorthands strength
open StrongProps.Right.Shorthands rightStrength
open MonoidalUtils.Shorthands monoidal using (α⇒; α⇐)
open Symmetric symmetric renaming (commutative to B-commutative)
open SymmProps symmetric
open CommutativeProperties braided CM
private
B : ∀ {X Y} → X ⊗₀ Y ⇒ Y ⊗₀ X
B {X} {Y} = braiding.⇒.η (X , Y)
braiding' : NaturalIsomorphism (⊗' symmetric CM) (flip-bifunctor (⊗' symmetric CM))
braiding' = record
{ F⇒G = ntHelper (record { η = λ _ → η ∘ B ; commute = λ (f , g) → swapping f g })
; F⇐G = ntHelper (record { η = λ _ → η ∘ B ; commute = λ (f , g) → swapping g f })
; iso = λ _ → record { isoˡ = pullˡ *-identityʳ ○ cancelʳ B-commutative ; isoʳ = pullˡ *-identityʳ ○ cancelʳ B-commutative }
}
where
swapping : ∀ {X Y U V} (f : X ⇒ M.F.₀ Y) (g : U ⇒ M.F.₀ V) → (η ∘ B) * ∘ ψ ∘ (f ⊗₁ g) ≈ (ψ ∘ (g ⊗₁ f)) * ∘ η ∘ B
swapping f g = begin
(η ∘ B) * ∘ ψ ∘ (f ⊗₁ g)
≈⟨ *⇒F₁ ⟩∘⟨refl ⟩
M.F.₁ B ∘ ψ ∘ (f ⊗₁ g)
≈⟨ refl⟩∘⟨ commutes ⟩∘⟨refl ⟩
M.F.₁ B ∘ (σ * ∘ τ) ∘ (f ⊗₁ g)
≈⟨ extendʳ (pullˡ F₁∘*) ⟩
(M.F.₁ B ∘ σ) * ∘ τ ∘ (f ⊗₁ g)
≈⟨ *-resp-≈ (∘-resp-≈ˡ (M.F.F-resp-≈ (sym braiding-selfInverse)) ○ left-right-braiding-comm braided ○ ∘-resp-≈ʳ braiding-selfInverse) ⟩∘⟨refl ⟩
(τ ∘ B) * ∘ τ ∘ (f ⊗₁ g)
≈˘⟨ pullˡ (pullˡ *∘F₁) ○ assoc ⟩
τ * ∘ (M.F.₁ B ∘ τ) ∘ (f ⊗₁ g)
≈˘⟨ extendʳ (pullʳ (sym (right-left-braiding-comm braided))) ⟩
ψ ∘ B ∘ (f ⊗₁ g)
≈⟨ refl⟩∘⟨ braiding.⇒.commute _ ⟩
ψ ∘ (g ⊗₁ f) ∘ B
≈˘⟨ extendʳ *-identityʳ ⟩
(ψ ∘ (g ⊗₁ f)) * ∘ η ∘ B
∎
Kleisli-Braided : Braided (Kleisli-Monoidal symmetric CM)
Kleisli-Braided = record
{ braiding = braiding'
; hexagon₁ = hexagon₁'
; hexagon₂ = hexagon₂'
}
where
hexagon₁' : ∀ {X Y Z : Obj} → (ψ {X} {Y ⊗₀ Z} ∘ (η ⊗₁ (η ∘ B))) * ∘ (η ∘ α⇒) * ∘ (ψ ∘ ((η ∘ B) ⊗₁ η)) ≈ (η ∘ α⇒) * ∘ (η ∘ B) * ∘ (η ∘ α⇒)
hexagon₁' = begin
(ψ ∘ (η ⊗₁ (η ∘ B))) * ∘ (η ∘ α⇒) * ∘ (ψ ∘ ((η ∘ B) ⊗₁ η))
≈⟨ pullˡ *-sym-assoc ⟩
((ψ ∘ (η ⊗₁ (η ∘ B))) * ∘ (η ∘ α⇒)) * ∘ (ψ ∘ ((η ∘ B) ⊗₁ η))
≈⟨ ((*-resp-≈ (pullˡ *-identityʳ)) ⟩∘⟨refl) ⟩
((ψ ∘ (η ⊗₁ (η ∘ B))) ∘ α⇒) * ∘ (ψ ∘ ((η ∘ B) ⊗₁ η))
≈˘⟨ *-resp-≈ (∘-resp-≈ˡ (∘-resp-≈ʳ (sym ⊗.homomorphism ○ ⊗.F-resp-≈ (identityʳ , refl)))) ⟩∘⟨ ∘-resp-≈ʳ (sym ⊗.homomorphism ○ ⊗.F-resp-≈ (refl , identityʳ)) ⟩
((ψ ∘ (η ⊗₁ η) ∘ (id ⊗₁ B)) ∘ α⇒) * ∘ (ψ ∘ (η ⊗₁ η) ∘ (B ⊗₁ id))
≈⟨ *-resp-≈ (∘-resp-≈ˡ (pullˡ ψ-η)) ⟩∘⟨ pullˡ ψ-η ⟩
((η ∘ (id ⊗₁ B)) ∘ α⇒) * ∘ (η ∘ (B ⊗₁ id))
≈⟨ pullˡ *-identityʳ ⟩
((η ∘ (id ⊗₁ B)) ∘ α⇒) ∘ (B ⊗₁ id)
≈⟨ (assoc ○ pullʳ hexagon₁ ○ (sym-assoc ○ sym-assoc)) ⟩
((η ∘ α⇒) ∘ B) ∘ α⇒
≈˘⟨ pullˡ (pullˡ *-identityʳ) ⟩
(η ∘ α⇒) * ∘ (η ∘ B) ∘ α⇒
≈˘⟨ refl⟩∘⟨ (pullˡ *-identityʳ) ⟩
(η ∘ α⇒) * ∘ (η ∘ B) * ∘ (η ∘ α⇒)
∎
hexagon₂' : ∀ {X Y Z : Obj} → ((ψ {X ⊗₀ Y} {Z} ∘ ((η ∘ B) ⊗₁ η)) * ∘ (η ∘ α⇐)) * ∘ (ψ ∘ (η ⊗₁ (η ∘ B))) ≈ ((η ∘ α⇐) * ∘ (η ∘ B)) * ∘ (η ∘ α⇐)
hexagon₂' = begin
((ψ ∘ ((η ∘ B) ⊗₁ η)) * ∘ (η ∘ α⇐)) * ∘ (ψ ∘ (η ⊗₁ (η ∘ B)))
≈⟨ ((*-resp-≈ (pullˡ *-identityʳ)) ⟩∘⟨refl) ⟩
((ψ ∘ ((η ∘ B) ⊗₁ η)) ∘ α⇐) * ∘ (ψ ∘ (η ⊗₁ (η ∘ B)))
≈˘⟨ *-resp-≈ (∘-resp-≈ˡ (∘-resp-≈ʳ (sym ⊗.homomorphism ○ ⊗.F-resp-≈ (refl , identityʳ)))) ⟩∘⟨ ∘-resp-≈ʳ (sym ⊗.homomorphism ○ ⊗.F-resp-≈ (identityʳ , refl)) ⟩
((ψ ∘ (η ⊗₁ η) ∘ (B ⊗₁ id)) ∘ α⇐) * ∘ (ψ ∘ (η ⊗₁ η) ∘ (id ⊗₁ B))
≈⟨ *-resp-≈ (∘-resp-≈ˡ (pullˡ ψ-η)) ⟩∘⟨ pullˡ ψ-η ⟩
((η ∘ (B ⊗₁ id)) ∘ α⇐) * ∘ (η ∘ (id ⊗₁ B))
≈⟨ pullˡ *-identityʳ ⟩
((η ∘ (B ⊗₁ id)) ∘ α⇐) ∘ (id ⊗₁ B)
≈⟨ (assoc ○ pullʳ (sym-assoc ○ hexagon₂) ○ (sym-assoc ○ ∘-resp-≈ˡ sym-assoc)) ⟩
((η ∘ α⇐) ∘ B) ∘ α⇐
≈˘⟨ pullˡ (pullˡ *-identityʳ) ⟩
(η ∘ α⇐) * ∘ (η ∘ B) ∘ α⇐
≈˘⟨ refl⟩∘⟨ (pullˡ *-identityʳ) ⟩
(η ∘ α⇐) * ∘ (η ∘ B) * ∘ (η ∘ α⇐)
≈˘⟨ *-assoc ⟩∘⟨refl ○ assoc ⟩
((η ∘ α⇐) * ∘ (η ∘ B)) * ∘ (η ∘ α⇐)
∎
Kleisli-Symmetric : Symmetric (Kleisli-Monoidal symmetric CM)
Kleisli-Symmetric = record
{ braided = Kleisli-Braided
; commutative = λ {X} {Y} → pullˡ *-identityʳ ○ cancelʳ B-commutative
}