Skip to content

Commit 4c5a249

Browse files
JacquesCaretteJacquesCarette
authored
Merge pull request #480 from Reijix/2-copycats-kleislisymmetric
Restriction Kleisli Category #2: Kleisli Category is monoidal symmetric
2 parents aabe490 + 9fcbe0f commit 4c5a249

File tree

3 files changed

+343
-0
lines changed

3 files changed

+343
-0
lines changed

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

Lines changed: 189 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,189 @@
1+
{-# OPTIONS --without-K --safe #-}
2+
module Categories.Category.Monoidal.Construction.Kleisli where
3+
4+
open import Level
5+
open import Data.Product using (_,_)
6+
7+
open import Categories.Category.Core using (Category)
8+
open import Categories.Monad using (Monad)
9+
open import Categories.Monad.Strong using (Strength; RightStrength)
10+
open import Categories.Monad.Commutative using (CommutativeMonad)
11+
open import Categories.Monad.Commutative.Properties using (module CommutativeProperties; module SymmetricProperties)
12+
open import Categories.Category.Construction.Kleisli using (Kleisli; module TripleNotation)
13+
open import Categories.Category.Monoidal using (Monoidal)
14+
open import Categories.Category.Monoidal.Symmetric using (Symmetric)
15+
open import Categories.Functor.Bifunctor using (Bifunctor)
16+
17+
18+
import Categories.Morphism as MC
19+
import Categories.Morphism.Reasoning as MR
20+
import Categories.Monad.Strong.Properties as StrongProps
21+
import Categories.Category.Monoidal.Utilities as MonoidalUtils
22+
23+
private
24+
variable
25+
o ℓ e : Level
26+
27+
-- The Kleisli category of a commutative monad (where 𝒞 is symmetric) is monoidal.
28+
29+
module _ {𝒞 : Category o ℓ e} {monoidal : Monoidal 𝒞} (symmetric : Symmetric monoidal) (CM : CommutativeMonad (Symmetric.braided symmetric)) where
30+
open Category 𝒞
31+
open MR 𝒞
32+
open HomReasoning
33+
open Equiv
34+
35+
open CommutativeMonad CM hiding (identityˡ)
36+
open Monad M using (μ)
37+
open TripleNotation M
38+
39+
open StrongProps.Left.Shorthands strength
40+
open StrongProps.Right.Shorthands rightStrength
41+
open MonoidalUtils.Shorthands monoidal using (α⇒; α⇐; λ⇒; λ⇐; ρ⇒; ρ⇐)
42+
43+
44+
open Symmetric symmetric
45+
open CommutativeProperties braided CM
46+
open SymmetricProperties symmetric CM
47+
48+
open MC (Kleisli M) using (_≅_)
49+
50+
⊗' : Bifunctor (Kleisli M) (Kleisli M) (Kleisli M)
51+
⊗' = record
52+
{ F₀ = λ (X , Y) → X ⊗₀ Y
53+
; F₁ = λ (f , g) → ψ ∘ (f ⊗₁ g)
54+
; identity = identity'
55+
; homomorphism = λ {(X₁ , X₂)} {(Y₁ , Y₂)} {(Z₁ , Z₂)} {(f , g)} {(h , i)} → homomorphism' {X₁} {X₂} {Y₁} {Y₂} {Z₁} {Z₂} {f} {g} {h} {i}
56+
; F-resp-≈ = λ (f≈g , h≈i) → ∘-resp-≈ʳ (⊗.F-resp-≈ (f≈g , h≈i))
57+
}
58+
where
59+
identity' : ∀ {X} {Y} → ψ ∘ (η {X} ⊗₁ η {Y}) ≈ η
60+
identity' = begin
61+
(τ * ∘ σ) ∘ (η ⊗₁ η) ≈˘⟨ refl⟩∘⟨ (sym ⊗.homomorphism ○ ⊗.F-resp-≈ (identityˡ , identityʳ)) ⟩
62+
(τ * ∘ σ) ∘ (id ⊗₁ η) ∘ (η ⊗₁ id) ≈⟨ pullʳ (pullˡ η-comm) ⟩
63+
τ * ∘ η ∘ (η ⊗₁ id) ≈⟨ pullˡ *-identityʳ ⟩
64+
τ ∘ (η ⊗₁ id) ≈⟨ RightStrength.η-comm rightStrength ⟩
65+
η ∎
66+
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)
67+
homomorphism' {f = f} {g} {h} {i} = begin
68+
ψ ∘ ((h * ∘ f) ⊗₁ (i * ∘ g)) ≈˘⟨ refl⟩∘⟨ (pullˡ (sym ⊗.homomorphism) ○ sym ⊗.homomorphism) ⟩
69+
ψ ∘ (μ.η _ ⊗₁ μ.η _) ∘ (M.F.₁ h ⊗₁ M.F.₁ i) ∘ (f ⊗₁ g) ≈˘⟨ extendʳ ψ-μ ⟩
70+
ψ * ∘ ψ ∘ (M.F.₁ h ⊗₁ M.F.₁ i) ∘ (f ⊗₁ g) ≈⟨ refl⟩∘⟨ extendʳ ψ-comm ⟩
71+
ψ * ∘ M.F.₁ (h ⊗₁ i) ∘ ψ ∘ (f ⊗₁ g) ≈⟨ pullˡ *∘F₁ ⟩
72+
(ψ ∘ (h ⊗₁ i)) * ∘ ψ ∘ (f ⊗₁ g) ∎
73+
74+
unitorˡ' : ∀ {X} → unit ⊗₀ X ≅ X
75+
unitorˡ' = record { from = η ∘ λ⇒ ; to = η ∘ λ⇐ ; iso = record
76+
{ isoˡ = pullˡ *-identityʳ ○ cancelʳ unitorˡ.isoˡ
77+
; isoʳ = pullˡ *-identityʳ ○ cancelʳ unitorˡ.isoʳ
78+
} }
79+
80+
unitorʳ' : ∀ {X} → X ⊗₀ unit ≅ X
81+
unitorʳ' = record { from = η ∘ ρ⇒ ; to = η ∘ ρ⇐ ; iso = record
82+
{ isoˡ = pullˡ *-identityʳ ○ cancelʳ unitorʳ.isoˡ
83+
; isoʳ = pullˡ *-identityʳ ○ cancelʳ unitorʳ.isoʳ
84+
} }
85+
86+
associator' : ∀ {X Y Z} → (X ⊗₀ Y) ⊗₀ Z ≅ X ⊗₀ (Y ⊗₀ Z)
87+
associator' = record { from = η ∘ α⇒ ; to = η ∘ α⇐ ; iso = record
88+
{ isoˡ = pullˡ *-identityʳ ○ cancelʳ associator.isoˡ
89+
; isoʳ = pullˡ *-identityʳ ○ cancelʳ associator.isoʳ
90+
} }
91+
92+
Kleisli-Monoidal : Monoidal (Kleisli M)
93+
Kleisli-Monoidal = record
94+
{ ⊗ = ⊗'
95+
; unit = unit
96+
; unitorˡ = unitorˡ'
97+
; unitorʳ = unitorʳ'
98+
; associator = associator'
99+
; unitorˡ-commute-from = unitorˡ-commute-from'
100+
; unitorˡ-commute-to = unitorˡ-commute-to'
101+
; unitorʳ-commute-from = unitorʳ-commute-from'
102+
; unitorʳ-commute-to = unitorʳ-commute-to'
103+
; assoc-commute-from = assoc-commute-from'
104+
; assoc-commute-to = assoc-commute-to'
105+
; triangle = triangle'
106+
; pentagon = pentagon'
107+
}
108+
where
109+
unitorˡ-commute-from' : ∀ {X} {Y} {f : X ⇒ M.F.₀ Y} → (η ∘ λ⇒) * ∘ ψ ∘ (η ⊗₁ f) ≈ f * ∘ η ∘ λ⇒
110+
unitorˡ-commute-from' {f = f} = begin
111+
(η ∘ λ⇒) * ∘ ψ ∘ (η ⊗₁ f) ≈⟨ *⇒F₁ ⟩∘⟨ ψ-σ' ⟩
112+
M.F.₁ λ⇒ ∘ σ ∘ (id ⊗₁ f) ≈⟨ pullˡ (Strength.identityˡ strength) ⟩
113+
λ⇒ ∘ (id ⊗₁ f) ≈⟨ unitorˡ-commute-from ⟩
114+
f ∘ λ⇒ ≈˘⟨ pullˡ *-identityʳ ⟩
115+
f * ∘ η ∘ λ⇒ ∎
116+
unitorˡ-commute-to' : ∀ {X} {Y} {f : X ⇒ M.F.₀ Y} → (η ∘ λ⇐) * ∘ f ≈ (ψ ∘ (η ⊗₁ f)) * ∘ η ∘ λ⇐
117+
unitorˡ-commute-to' {f = f} = begin
118+
(η ∘ λ⇐) * ∘ f ≈⟨ *⇒F₁ ⟩∘⟨refl ⟩
119+
M.F.₁ λ⇐ ∘ f ≈˘⟨ refl⟩∘⟨ (cancelˡ unitorˡ.isoʳ) ⟩
120+
M.F.₁ λ⇐ ∘ λ⇒ ∘ λ⇐ ∘ f ≈˘⟨ pullʳ (pullˡ (Strength.identityˡ strength)) ⟩
121+
(M.F.₁ λ⇐ ∘ M.F.₁ λ⇒) ∘ σ ∘ λ⇐ ∘ f ≈⟨ elimˡ (sym M.F.homomorphism ○ (M.F.F-resp-≈ unitorˡ.isoˡ ○ M.F.identity)) ⟩
122+
σ ∘ λ⇐ ∘ f ≈˘⟨ pullʳ (sym unitorˡ-commute-to) ⟩
123+
(σ ∘ (id ⊗₁ f)) ∘ λ⇐ ≈˘⟨ ψ-σ' ⟩∘⟨refl ⟩
124+
(ψ ∘ (η ⊗₁ f)) ∘ λ⇐ ≈˘⟨ pullˡ *-identityʳ ⟩
125+
(ψ ∘ (η ⊗₁ f)) * ∘ η ∘ λ⇐ ∎
126+
unitorʳ-commute-from' : ∀ {X} {Y} {f : X ⇒ M.F.₀ Y} → (η ∘ ρ⇒) * ∘ ψ ∘ (f ⊗₁ η) ≈ f * ∘ η ∘ ρ⇒
127+
unitorʳ-commute-from' {f = f} = begin
128+
(η ∘ ρ⇒) * ∘ ψ ∘ (f ⊗₁ η) ≈⟨ *⇒F₁ ⟩∘⟨ ψ-τ' ⟩
129+
M.F.₁ ρ⇒ ∘ τ ∘ (f ⊗₁ id) ≈⟨ pullˡ (RightStrength.identityˡ rightStrength) ⟩
130+
ρ⇒ ∘ (f ⊗₁ id) ≈⟨ unitorʳ-commute-from ⟩
131+
f ∘ ρ⇒ ≈˘⟨ pullˡ *-identityʳ ⟩
132+
f * ∘ η ∘ ρ⇒ ∎
133+
unitorʳ-commute-to' : ∀ {X} {Y} {f : X ⇒ M.F.₀ Y} → (η ∘ ρ⇐) * ∘ f ≈ (ψ ∘ (f ⊗₁ η)) * ∘ η ∘ ρ⇐
134+
unitorʳ-commute-to' {f = f} = begin
135+
(η ∘ ρ⇐) * ∘ f ≈⟨ *⇒F₁ ⟩∘⟨refl ⟩
136+
M.F.₁ ρ⇐ ∘ f ≈˘⟨ refl⟩∘⟨ (cancelˡ unitorʳ.isoʳ) ⟩
137+
M.F.₁ ρ⇐ ∘ ρ⇒ ∘ ρ⇐ ∘ f ≈˘⟨ pullʳ (pullˡ (RightStrength.identityˡ rightStrength)) ⟩
138+
(M.F.₁ ρ⇐ ∘ M.F.₁ ρ⇒) ∘ τ ∘ ρ⇐ ∘ f ≈⟨ elimˡ (sym M.F.homomorphism ○ (M.F.F-resp-≈ unitorʳ.isoˡ ○ M.F.identity)) ⟩
139+
τ ∘ ρ⇐ ∘ f ≈˘⟨ pullʳ (sym unitorʳ-commute-to) ⟩
140+
(τ ∘ (f ⊗₁ id)) ∘ ρ⇐ ≈˘⟨ ψ-τ' ⟩∘⟨refl ⟩
141+
(ψ ∘ (f ⊗₁ η)) ∘ ρ⇐ ≈˘⟨ pullˡ *-identityʳ ⟩
142+
(ψ ∘ (f ⊗₁ η)) * ∘ η ∘ ρ⇐ ∎
143+
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)))) * ∘ (η ∘ α⇒)
144+
assoc-commute-from' {f = f} {g = g} {h = h} = begin
145+
(η ∘ α⇒) * ∘ ψ ∘ ((ψ ∘ (f ⊗₁ g)) ⊗₁ h) ≈⟨ *⇒F₁ ⟩∘⟨refl ⟩
146+
M.F.₁ α⇒ ∘ ψ ∘ ((ψ ∘ (f ⊗₁ g)) ⊗₁ h) ≈˘⟨ refl⟩∘⟨ refl⟩∘⟨ (sym ⊗.homomorphism ○ ⊗.F-resp-≈ (refl , identityˡ)) ⟩
147+
M.F.₁ α⇒ ∘ ψ ∘ (ψ ⊗₁ id) ∘ ((f ⊗₁ g) ⊗₁ h) ≈⟨ (sym-assoc ○ pullˡ (assoc ○ ψ-assoc-from) ○ assoc²βε) ⟩
148+
ψ ∘ (id ⊗₁ ψ) ∘ α⇒ ∘ ((f ⊗₁ g) ⊗₁ h) ≈˘⟨ pullʳ (pullʳ (sym assoc-commute-from)) ⟩
149+
(ψ ∘ (id ⊗₁ ψ) ∘ (f ⊗₁ (g ⊗₁ h))) ∘ α⇒ ≈⟨ (refl⟩∘⟨ (sym ⊗.homomorphism ○ ⊗.F-resp-≈ (identityˡ , refl))) ⟩∘⟨refl ⟩
150+
(ψ ∘ (f ⊗₁ (ψ ∘ (g ⊗₁ h)))) ∘ α⇒ ≈˘⟨ pullˡ *-identityʳ ⟩
151+
(ψ ∘ (f ⊗₁ (ψ ∘ (g ⊗₁ h)))) * ∘ (η ∘ α⇒) ∎
152+
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)) * ∘ (η ∘ α⇐)
153+
assoc-commute-to' {f = f} {g = g} {h = h} = begin
154+
(η ∘ α⇐) * ∘ ψ ∘ (f ⊗₁ (ψ ∘ (g ⊗₁ h))) ≈⟨ *⇒F₁ ⟩∘⟨refl ⟩
155+
M.F.₁ α⇐ ∘ ψ ∘ (f ⊗₁ (ψ ∘ (g ⊗₁ h))) ≈˘⟨ refl⟩∘⟨ refl⟩∘⟨ (sym ⊗.homomorphism ○ ⊗.F-resp-≈ (identityˡ , refl)) ⟩
156+
M.F.₁ α⇐ ∘ ψ ∘ (id ⊗₁ ψ) ∘ (f ⊗₁ (g ⊗₁ h)) ≈⟨ (sym-assoc ○ (pullˡ (assoc ○ ψ-assoc-to) ○ assoc²βε)) ⟩
157+
ψ ∘ (ψ ⊗₁ id) ∘ α⇐ ∘ (f ⊗₁ (g ⊗₁ h)) ≈˘⟨ pullʳ (pullʳ (sym assoc-commute-to)) ⟩
158+
(ψ ∘ (ψ ⊗₁ id) ∘ ((f ⊗₁ g) ⊗₁ h)) ∘ α⇐ ≈⟨ (refl⟩∘⟨ (sym ⊗.homomorphism ○ ⊗.F-resp-≈ (refl , identityˡ))) ⟩∘⟨refl ⟩
159+
(ψ ∘ ((ψ ∘ (f ⊗₁ g)) ⊗₁ h)) ∘ α⇐ ≈˘⟨ pullˡ *-identityʳ ⟩
160+
(ψ ∘ ((ψ ∘ (f ⊗₁ g)) ⊗₁ h)) * ∘ (η ∘ α⇐) ∎
161+
triangle' : ∀ {X} {Y} → (ψ ∘ (η {X} ⊗₁ (η ∘ λ⇒))) * ∘ (η ∘ α⇒) ≈ ψ ∘ ((η ∘ ρ⇒) ⊗₁ η {Y})
162+
triangle' = begin
163+
(ψ ∘ (η ⊗₁ (η ∘ λ⇒))) * ∘ (η ∘ α⇒) ≈⟨ pullˡ *-identityʳ ⟩
164+
(ψ ∘ (η ⊗₁ (η ∘ λ⇒))) ∘ α⇒ ≈˘⟨ pullˡ (pullʳ (sym ⊗.homomorphism ○ ⊗.F-resp-≈ (identityʳ , refl))) ⟩
165+
(ψ ∘ (η ⊗₁ η)) ∘ (id ⊗₁ λ⇒) ∘ α⇒ ≈⟨ (refl⟩∘⟨ triangle) ⟩
166+
(ψ ∘ (η ⊗₁ η)) ∘ (ρ⇒ ⊗₁ id) ≈⟨ pullʳ (sym ⊗.homomorphism ○ ⊗.F-resp-≈ (refl , identityʳ)) ⟩
167+
ψ ∘ ((η ∘ ρ⇒) ⊗₁ η) ∎
168+
pentagon' : ∀ {A B C D : Obj} → (ψ {A} {B ⊗₀ (C ⊗₀ D)} ∘ (η ⊗₁ (η ∘ α⇒))) * ∘ (η ∘ α⇒) * ∘ (ψ ∘ ((η ∘ α⇒) ⊗₁ η)) ≈ (η ∘ α⇒) * ∘ (η ∘ α⇒)
169+
pentagon' = begin
170+
(ψ ∘ (η ⊗₁ (η ∘ α⇒))) * ∘ (η ∘ α⇒) * ∘ (ψ ∘ ((η ∘ α⇒) ⊗₁ η))
171+
≈⟨ refl⟩∘⟨ *⇒F₁ ⟩∘⟨refl ⟩
172+
(ψ ∘ (η ⊗₁ (η ∘ α⇒))) * ∘ M.F.₁ α⇒ ∘ (ψ ∘ ((η ∘ α⇒) ⊗₁ η))
173+
≈⟨ pullˡ (*∘F₁ ○ *-resp-≈ assoc) ⟩
174+
(ψ ∘ (η ⊗₁ (η ∘ α⇒)) ∘ α⇒) * ∘ (ψ ∘ ((η ∘ α⇒) ⊗₁ η))
175+
≈˘⟨ refl⟩∘⟨ refl⟩∘⟨ (sym ⊗.homomorphism ○ ⊗.F-resp-≈ (refl , identityʳ)) ⟩
176+
(ψ ∘ (η ⊗₁ (η ∘ α⇒)) ∘ α⇒) * ∘ (ψ ∘ (η ⊗₁ η) ∘ (α⇒ ⊗₁ id))
177+
≈⟨ refl⟩∘⟨ pullˡ ψ-η ⟩
178+
(ψ ∘ (η ⊗₁ (η ∘ α⇒)) ∘ α⇒) * ∘ (η ∘ (α⇒ ⊗₁ id))
179+
≈⟨ pullˡ *-identityʳ ⟩
180+
(ψ ∘ (η ⊗₁ (η ∘ α⇒)) ∘ α⇒) ∘ (α⇒ ⊗₁ id)
181+
≈˘⟨ sym-assoc ○ (∘-resp-≈ʳ sym-assoc ○ pullˡ (pullʳ (pullˡ (sym ⊗.homomorphism ○ ⊗.F-resp-≈ (identityʳ , refl))))) ⟩
182+
ψ ∘ (η ⊗₁ η) ∘ (id ⊗₁ α⇒) ∘ α⇒ ∘ (α⇒ ⊗₁ id)
183+
≈⟨ (refl⟩∘⟨ refl⟩∘⟨ pentagon) ⟩
184+
ψ ∘ (η ⊗₁ η) ∘ (α⇒ ∘ α⇒)
185+
≈⟨ (pullˡ ψ-η) ○ sym-assoc ⟩
186+
(η ∘ α⇒) ∘ α⇒
187+
≈˘⟨ pullˡ *-identityʳ ⟩
188+
(η ∘ α⇒) * ∘ (η ∘ α⇒)
189+
∎

0 commit comments

Comments
 (0)