Restriction Kleisli Category #2: Kleisli Category is monoidal symmetric

src/Categories/Category/Monoidal/Construction/Kleisli.agda

@@ -0,0 +1,189 @@
+{-# 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
+
+-- The Kleisli category of a commutative monad (where 𝒞 is symmetric) is monoidal.
+
+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ʳ ⟩ 
+      (η ∘ α⇒) * ∘ (η ∘ α⇒)                                                 
+        ∎