Mercurial > hg > Members > kono > Proof > category
annotate kleisli.agda @ 820:658daaa74df3
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Wed, 01 May 2019 10:16:45 +0900 |
| parents | a5f2ca67e7c5 |
| children |
| rev | line source |
|---|---|
| 82 | 1 -- -- -- -- -- -- -- -- |
| 153 | 2 -- Monad to Kelisli Category |
| 82 | 3 -- defines U_T and F_T as a resolution of Monad |
| 4 -- checks Adjointness | |
| 5 -- | |
| 6 -- Shinji KONO <kono@ie.u-ryukyu.ac.jp> | |
| 7 -- -- -- -- -- -- -- -- | |
| 0 | 8 |
| 9 -- Monad | |
| 10 -- Category A | |
| 11 -- A = Category | |
| 22 | 12 -- Functor T : A → A |
| 0 | 13 --T(a) = t(a) |
| 14 --T(f) = tf(f) | |
| 15 | |
| 2 | 16 open import Category -- https://github.com/konn/category-agda |
| 0 | 17 open import Level |
| 56 | 18 --open import Category.HomReasoning |
| 19 open import HomReasoning | |
| 20 open import cat-utility | |
|
72
cbc30519e961
stack overflow solved by moving implicit parameters to module parameters
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
71
diff
changeset
|
21 open import Category.Cat |
|
cbc30519e961
stack overflow solved by moving implicit parameters to module parameters
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
71
diff
changeset
|
22 |
| 152 | 23 module kleisli { c₁ c₂ ℓ : Level} { A : Category c₁ c₂ ℓ } |
|
72
cbc30519e961
stack overflow solved by moving implicit parameters to module parameters
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
71
diff
changeset
|
24 { T : Functor A A } |
|
cbc30519e961
stack overflow solved by moving implicit parameters to module parameters
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
71
diff
changeset
|
25 { η : NTrans A A identityFunctor T } |
|
cbc30519e961
stack overflow solved by moving implicit parameters to module parameters
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
71
diff
changeset
|
26 { μ : NTrans A A (T ○ T) T } |
|
688
a5f2ca67e7c5
fix monad/adjunction definition
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
474
diff
changeset
|
27 { M : IsMonad A T η μ } where |
| 0 | 28 |
| 1 | 29 --T(g f) = T(g) T(f) |
| 30 | |
| 31 | 31 open Functor |
| 22 | 32 Lemma1 : {c₁ c₂ l : Level} {A : Category c₁ c₂ l} (T : Functor A A) → {a b c : Obj A} {g : Hom A b c} { f : Hom A a b } |
| 33 → A [ ( FMap T (A [ g o f ] )) ≈ (A [ FMap T g o FMap T f ]) ] | |
| 300 | 34 Lemma1 = λ t → IsFunctor.distr ( isFunctor t ) |
| 0 | 35 |
| 36 | |
| 7 | 37 open NTrans |
| 1 | 38 Lemma2 : {c₁ c₂ l : Level} {A : Category c₁ c₂ l} {F G : Functor A A} |
| 22 | 39 → (μ : NTrans A A F G) → {a b : Obj A} { f : Hom A a b } |
| 30 | 40 → A [ A [ FMap G f o TMap μ a ] ≈ A [ TMap μ b o FMap F f ] ] |
| 300 | 41 Lemma2 = λ n → IsNTrans.commute ( isNTrans n ) |
| 0 | 42 |
| 82 | 43 -- Laws of Monad |
| 44 -- | |
| 22 | 45 -- η : 1_A → T |
| 46 -- μ : TT → T | |
| 82 | 47 -- μ(a)η(T(a)) = a -- unity law 1 |
| 48 -- μ(a)T(η(a)) = a -- unity law 2 | |
| 49 -- μ(a)(μ(T(a))) = μ(a)T(μ(a)) -- association law | |
| 0 | 50 |
| 51 | |
| 2 | 52 Lemma3 : {c₁ c₂ ℓ : Level} {A : Category c₁ c₂ ℓ} |
| 53 { T : Functor A A } | |
| 7 | 54 { η : NTrans A A identityFunctor T } |
| 55 { μ : NTrans A A (T ○ T) T } | |
| 22 | 56 { a : Obj A } → |
|
688
a5f2ca67e7c5
fix monad/adjunction definition
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
474
diff
changeset
|
57 ( M : IsMonad A T η μ ) |
| 30 | 58 → A [ A [ TMap μ a o TMap μ ( FObj T a ) ] ≈ A [ TMap μ a o FMap T (TMap μ a) ] ] |
|
688
a5f2ca67e7c5
fix monad/adjunction definition
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
474
diff
changeset
|
59 Lemma3 = λ m → IsMonad.assoc m |
| 2 | 60 |
| 61 | |
| 62 Lemma4 : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) {a b : Obj A } { f : Hom A a b} | |
| 22 | 63 → A [ A [ Id {_} {_} {_} {A} b o f ] ≈ f ] |
| 300 | 64 Lemma4 = λ a → IsCategory.identityL ( Category.isCategory a ) |
| 0 | 65 |
| 3 | 66 Lemma5 : {c₁ c₂ ℓ : Level} {A : Category c₁ c₂ ℓ} |
| 67 { T : Functor A A } | |
| 7 | 68 { η : NTrans A A identityFunctor T } |
| 69 { μ : NTrans A A (T ○ T) T } | |
| 22 | 70 { a : Obj A } → |
|
688
a5f2ca67e7c5
fix monad/adjunction definition
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
474
diff
changeset
|
71 ( M : IsMonad A T η μ ) |
| 30 | 72 → A [ A [ TMap μ a o TMap η ( FObj T a ) ] ≈ Id {_} {_} {_} {A} (FObj T a) ] |
|
688
a5f2ca67e7c5
fix monad/adjunction definition
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
474
diff
changeset
|
73 Lemma5 = λ m → IsMonad.unity1 m |
| 3 | 74 |
| 75 Lemma6 : {c₁ c₂ ℓ : Level} {A : Category c₁ c₂ ℓ} | |
| 76 { T : Functor A A } | |
| 7 | 77 { η : NTrans A A identityFunctor T } |
| 78 { μ : NTrans A A (T ○ T) T } | |
| 22 | 79 { a : Obj A } → |
|
688
a5f2ca67e7c5
fix monad/adjunction definition
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
474
diff
changeset
|
80 ( M : IsMonad A T η μ ) |
| 30 | 81 → A [ A [ TMap μ a o (FMap T (TMap η a )) ] ≈ Id {_} {_} {_} {A} (FObj T a) ] |
|
688
a5f2ca67e7c5
fix monad/adjunction definition
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
474
diff
changeset
|
82 Lemma6 = λ m → IsMonad.unity2 m |
| 3 | 83 |
| 82 | 84 -- Laws of Kleisli Category |
| 85 -- | |
| 0 | 86 -- nat of η |
| 82 | 87 -- g ○ f = μ(c) T(g) f -- join definition |
| 88 -- η(b) ○ f = f -- left id (Lemma7) | |
| 89 -- f ○ η(a) = f -- right id (Lemma8) | |
| 90 -- h ○ (g ○ f) = (h ○ g) ○ f -- assocation law (Lemma9) | |
| 11 | 91 |
| 22 | 92 -- η(b) ○ f = f |
|
688
a5f2ca67e7c5
fix monad/adjunction definition
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
474
diff
changeset
|
93 |
|
a5f2ca67e7c5
fix monad/adjunction definition
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
474
diff
changeset
|
94 join : (m : IsMonad A T η μ ) → { a b : Obj A } → { c : Obj A } → |
|
a5f2ca67e7c5
fix monad/adjunction definition
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
474
diff
changeset
|
95 ( Hom A b ( FObj T c )) → ( Hom A a ( FObj T b)) → Hom A a ( FObj T c ) |
|
a5f2ca67e7c5
fix monad/adjunction definition
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
474
diff
changeset
|
96 join _ {_} {_} {c} g f = A [ TMap μ c o A [ FMap T g o f ] ] |
|
a5f2ca67e7c5
fix monad/adjunction definition
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
474
diff
changeset
|
97 |
| 73 | 98 Lemma7 : { a : Obj A } { b : Obj A } ( f : Hom A a ( FObj T b) ) |
| 130 | 99 → A [ join M (TMap η b) f ≈ f ] |
| 73 | 100 Lemma7 {_} {b} f = |
| 101 let open ≈-Reasoning (A) in | |
| 21 | 102 begin |
| 130 | 103 join M (TMap η b) f |
| 21 | 104 ≈⟨ refl-hom ⟩ |
| 73 | 105 A [ TMap μ b o A [ FMap T ((TMap η b)) o f ] ] |
| 106 ≈⟨ IsCategory.associative (Category.isCategory A) ⟩ | |
| 107 A [ A [ TMap μ b o FMap T ((TMap η b)) ] o f ] | |
|
688
a5f2ca67e7c5
fix monad/adjunction definition
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
474
diff
changeset
|
108 ≈⟨ car ( IsMonad.unity2 M ) ⟩ |
| 73 | 109 A [ id (FObj T b) o f ] |
| 110 ≈⟨ IsCategory.identityL (Category.isCategory A) ⟩ | |
| 21 | 111 f |
| 112 ∎ | |
| 7 | 113 |
| 22 | 114 -- f ○ η(a) = f |
| 73 | 115 Lemma8 : { a : Obj A } { b : Obj A } |
| 22 | 116 ( f : Hom A a ( FObj T b) ) |
| 130 | 117 → A [ join M f (TMap η a) ≈ f ] |
| 73 | 118 Lemma8 {a} {b} f = |
| 22 | 119 begin |
| 130 | 120 join M f (TMap η a) |
| 22 | 121 ≈⟨ refl-hom ⟩ |
|
72
cbc30519e961
stack overflow solved by moving implicit parameters to module parameters
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
71
diff
changeset
|
122 A [ TMap μ b o A [ FMap T f o (TMap η a) ] ] |
| 66 | 123 ≈⟨ cdr ( nat η ) ⟩ |
|
72
cbc30519e961
stack overflow solved by moving implicit parameters to module parameters
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
71
diff
changeset
|
124 A [ TMap μ b o A [ (TMap η ( FObj T b)) o f ] ] |
|
cbc30519e961
stack overflow solved by moving implicit parameters to module parameters
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
71
diff
changeset
|
125 ≈⟨ IsCategory.associative (Category.isCategory A) ⟩ |
|
cbc30519e961
stack overflow solved by moving implicit parameters to module parameters
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
71
diff
changeset
|
126 A [ A [ TMap μ b o (TMap η ( FObj T b)) ] o f ] |
|
688
a5f2ca67e7c5
fix monad/adjunction definition
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
474
diff
changeset
|
127 ≈⟨ car ( IsMonad.unity1 M ) ⟩ |
|
72
cbc30519e961
stack overflow solved by moving implicit parameters to module parameters
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
71
diff
changeset
|
128 A [ id (FObj T b) o f ] |
|
cbc30519e961
stack overflow solved by moving implicit parameters to module parameters
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
71
diff
changeset
|
129 ≈⟨ IsCategory.identityL (Category.isCategory A) ⟩ |
| 22 | 130 f |
| 131 ∎ where | |
|
72
cbc30519e961
stack overflow solved by moving implicit parameters to module parameters
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
71
diff
changeset
|
132 open ≈-Reasoning (A) |
| 5 | 133 |
| 22 | 134 -- h ○ (g ○ f) = (h ○ g) ○ f |
|
72
cbc30519e961
stack overflow solved by moving implicit parameters to module parameters
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
71
diff
changeset
|
135 Lemma9 : { a b c d : Obj A } |
| 73 | 136 ( h : Hom A c ( FObj T d) ) |
| 23 | 137 ( g : Hom A b ( FObj T c) ) |
| 73 | 138 ( f : Hom A a ( FObj T b) ) |
| 130 | 139 → A [ join M h (join M g f) ≈ join M ( join M h g) f ] |
| 73 | 140 Lemma9 {a} {b} {c} {d} h g f = |
| 24 | 141 begin |
| 130 | 142 join M h (join M g f) |
| 30 | 143 ≈⟨⟩ |
| 130 | 144 join M h ( ( TMap μ c o ( FMap T g o f ) ) ) |
| 28 | 145 ≈⟨ refl-hom ⟩ |
| 30 | 146 ( TMap μ d o ( FMap T h o ( TMap μ c o ( FMap T g o f ) ) ) ) |
| 28 | 147 ≈⟨ cdr ( cdr ( assoc )) ⟩ |
| 30 | 148 ( TMap μ d o ( FMap T h o ( ( TMap μ c o FMap T g ) o f ) ) ) |
| 28 | 149 ≈⟨ assoc ⟩ --- ( f o ( g o h ) ) = ( ( f o g ) o h ) |
| 30 | 150 ( ( TMap μ d o FMap T h ) o ( (TMap μ c o FMap T g ) o f ) ) |
| 25 | 151 ≈⟨ assoc ⟩ |
| 30 | 152 ( ( ( TMap μ d o FMap T h ) o (TMap μ c o FMap T g ) ) o f ) |
| 253 | 153 ≈↑⟨ car assoc ⟩ |
| 30 | 154 ( ( TMap μ d o ( FMap T h o ( TMap μ c o FMap T g ) ) ) o f ) |
| 28 | 155 ≈⟨ car ( cdr (assoc) ) ⟩ |
| 30 | 156 ( ( TMap μ d o ( ( FMap T h o TMap μ c ) o FMap T g ) ) o f ) |
| 28 | 157 ≈⟨ car assoc ⟩ |
| 30 | 158 ( ( ( TMap μ d o ( FMap T h o TMap μ c ) ) o FMap T g ) o f ) |
| 28 | 159 ≈⟨ car (car ( cdr ( begin |
| 30 | 160 ( FMap T h o TMap μ c ) |
| 66 | 161 ≈⟨ nat μ ⟩ |
| 30 | 162 ( TMap μ (FObj T d) o FMap T (FMap T h) ) |
| 25 | 163 ∎ |
| 164 ))) ⟩ | |
| 30 | 165 ( ( ( TMap μ d o ( TMap μ ( FObj T d) o FMap T ( FMap T h ) ) ) o FMap T g ) o f ) |
| 253 | 166 ≈↑⟨ car assoc ⟩ |
| 30 | 167 ( ( TMap μ d o ( ( TMap μ ( FObj T d) o FMap T ( FMap T h ) ) o FMap T g ) ) o f ) |
| 253 | 168 ≈↑⟨ car ( cdr assoc ) ⟩ |
| 30 | 169 ( ( TMap μ d o ( TMap μ ( FObj T d) o ( FMap T ( FMap T h ) o FMap T g ) ) ) o f ) |
| 253 | 170 ≈↑⟨ car ( cdr (cdr (distr T ))) ⟩ |
| 30 | 171 ( ( TMap μ d o ( TMap μ ( FObj T d) o FMap T ( ( FMap T h o g ) ) ) ) o f ) |
| 28 | 172 ≈⟨ car assoc ⟩ |
| 30 | 173 ( ( ( TMap μ d o TMap μ ( FObj T d) ) o FMap T ( ( FMap T h o g ) ) ) o f ) |
| 28 | 174 ≈⟨ car ( car ( |
| 27 | 175 begin |
| 30 | 176 ( TMap μ d o TMap μ (FObj T d) ) |
|
688
a5f2ca67e7c5
fix monad/adjunction definition
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
474
diff
changeset
|
177 ≈⟨ IsMonad.assoc M ⟩ |
| 30 | 178 ( TMap μ d o FMap T (TMap μ d) ) |
| 27 | 179 ∎ |
| 180 )) ⟩ | |
| 30 | 181 ( ( ( TMap μ d o FMap T ( TMap μ d) ) o FMap T ( ( FMap T h o g ) ) ) o f ) |
| 253 | 182 ≈↑⟨ car assoc ⟩ |
| 30 | 183 ( ( TMap μ d o ( FMap T ( TMap μ d ) o FMap T ( ( FMap T h o g ) ) ) ) o f ) |
| 253 | 184 ≈↑⟨ assoc ⟩ |
| 30 | 185 ( TMap μ d o ( ( FMap T ( TMap μ d ) o FMap T ( ( FMap T h o g ) ) ) o f ) ) |
| 253 | 186 ≈↑⟨ cdr ( car ( distr T )) ⟩ |
| 30 | 187 ( TMap μ d o ( FMap T ( ( ( TMap μ d ) o ( FMap T h o g ) ) ) o f ) ) |
| 23 | 188 ≈⟨ refl-hom ⟩ |
| 130 | 189 join M ( ( TMap μ d o ( FMap T h o g ) ) ) f |
| 23 | 190 ≈⟨ refl-hom ⟩ |
| 130 | 191 join M ( join M h g) f |
| 24 | 192 ∎ where open ≈-Reasoning (A) |
| 3 | 193 |
| 82 | 194 -- |
| 195 -- o-resp in Kleisli Category ( for Functor definitions ) | |
| 196 -- | |
| 300 | 197 Lemma10 : {a b c : Obj A} → (f g : Hom A a (FObj T b) ) → (h i : Hom A b (FObj T c) ) → |
| 130 | 198 A [ f ≈ g ] → A [ h ≈ i ] → A [ (join M h f) ≈ (join M i g) ] |
| 474 | 199 Lemma10 {a} {b} {c} f g h i f≈g h≈i = let open ≈-Reasoning (A) in |
|
74
49e6eb3ef9c0
Kleisli Category constructed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
73
diff
changeset
|
200 begin |
| 130 | 201 join M h f |
|
74
49e6eb3ef9c0
Kleisli Category constructed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
73
diff
changeset
|
202 ≈⟨⟩ |
|
49e6eb3ef9c0
Kleisli Category constructed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
73
diff
changeset
|
203 TMap μ c o ( FMap T h o f ) |
| 474 | 204 ≈⟨ cdr ( car ( fcong T h≈i )) ⟩ |
| 205 TMap μ c o ( FMap T i o f ) | |
| 206 ≈⟨ cdr ( cdr f≈g ) ⟩ | |
|
74
49e6eb3ef9c0
Kleisli Category constructed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
73
diff
changeset
|
207 TMap μ c o ( FMap T i o g ) |
|
49e6eb3ef9c0
Kleisli Category constructed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
73
diff
changeset
|
208 ≈⟨⟩ |
| 130 | 209 join M i g |
|
74
49e6eb3ef9c0
Kleisli Category constructed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
73
diff
changeset
|
210 ∎ |
|
49e6eb3ef9c0
Kleisli Category constructed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
73
diff
changeset
|
211 |
| 82 | 212 -- |
| 213 -- Hom in Kleisli Category | |
| 214 -- | |
|
74
49e6eb3ef9c0
Kleisli Category constructed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
73
diff
changeset
|
215 |
| 87 | 216 |
| 217 record KleisliHom { c₁ c₂ ℓ : Level} { A : Category c₁ c₂ ℓ } { T : Functor A A } (a : Obj A) (b : Obj A) | |
| 467 | 218 : Set c₂ where |
| 219 field | |
| 220 KMap : Hom A a ( FObj T b ) | |
| 221 | |
| 222 open KleisliHom | |
|
69
84a150c980ce
generalized distr and assco1
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
68
diff
changeset
|
223 |
| 467 | 224 -- we need this to make agda check stop |
| 300 | 225 KHom = λ (a b : Obj A) → KleisliHom {c₁} {c₂} {ℓ} {A} {T} a b |
| 87 | 226 |
|
72
cbc30519e961
stack overflow solved by moving implicit parameters to module parameters
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
71
diff
changeset
|
227 K-id : {a : Obj A} → KHom a a |
|
cbc30519e961
stack overflow solved by moving implicit parameters to module parameters
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
71
diff
changeset
|
228 K-id {a = a} = record { KMap = TMap η a } |
| 56 | 229 |
|
69
84a150c980ce
generalized distr and assco1
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
68
diff
changeset
|
230 open import Relation.Binary.Core |
| 56 | 231 |
| 300 | 232 _⋍_ : { a : Obj A } { b : Obj A } (f g : KHom a b ) → Set ℓ |
| 73 | 233 _⋍_ {a} {b} f g = A [ KMap f ≈ KMap g ] |
|
71
709c1bde54dc
Kleisli category problem written
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
70
diff
changeset
|
234 |
| 108 | 235 _*_ : { a b c : Obj A } → ( KHom b c) → ( KHom a b) → KHom a c |
| 130 | 236 _*_ {a} {b} {c} g f = record { KMap = join M {a} {b} {c} (KMap g) (KMap f) } |
| 70 | 237 |
|
72
cbc30519e961
stack overflow solved by moving implicit parameters to module parameters
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
71
diff
changeset
|
238 isKleisliCategory : IsCategory ( Obj A ) KHom _⋍_ _*_ K-id |
|
cbc30519e961
stack overflow solved by moving implicit parameters to module parameters
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
71
diff
changeset
|
239 isKleisliCategory = record { isEquivalence = isEquivalence |
|
71
709c1bde54dc
Kleisli category problem written
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
70
diff
changeset
|
240 ; identityL = KidL |
|
709c1bde54dc
Kleisli category problem written
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
70
diff
changeset
|
241 ; identityR = KidR |
|
709c1bde54dc
Kleisli category problem written
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
70
diff
changeset
|
242 ; o-resp-≈ = Ko-resp |
|
709c1bde54dc
Kleisli category problem written
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
70
diff
changeset
|
243 ; associative = Kassoc |
|
69
84a150c980ce
generalized distr and assco1
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
68
diff
changeset
|
244 } |
|
84a150c980ce
generalized distr and assco1
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
68
diff
changeset
|
245 where |
| 73 | 246 open ≈-Reasoning (A) |
| 300 | 247 isEquivalence : { a b : Obj A } → |
|
72
cbc30519e961
stack overflow solved by moving implicit parameters to module parameters
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
71
diff
changeset
|
248 IsEquivalence {_} {_} {KHom a b} _⋍_ |
| 82 | 249 isEquivalence {C} {D} = -- this is the same function as A's equivalence but has different types |
| 250 record { refl = refl-hom | |
| 251 ; sym = sym | |
| 252 ; trans = trans-hom | |
| 253 } | |
| 300 | 254 KidL : {C D : Obj A} → {f : KHom C D} → (K-id * f) ⋍ f |
| 73 | 255 KidL {_} {_} {f} = Lemma7 (KMap f) |
| 300 | 256 KidR : {C D : Obj A} → {f : KHom C D} → (f * K-id) ⋍ f |
| 73 | 257 KidR {_} {_} {f} = Lemma8 (KMap f) |
| 300 | 258 Ko-resp : {a b c : Obj A} → {f g : KHom a b } → {h i : KHom b c } → |
|
71
709c1bde54dc
Kleisli category problem written
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
70
diff
changeset
|
259 f ⋍ g → h ⋍ i → (h * f) ⋍ (i * g) |
|
74
49e6eb3ef9c0
Kleisli Category constructed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
73
diff
changeset
|
260 Ko-resp {a} {b} {c} {f} {g} {h} {i} eq-fg eq-hi = Lemma10 {a} {b} {c} (KMap f) (KMap g) (KMap h) (KMap i) eq-fg eq-hi |
| 300 | 261 Kassoc : {a b c d : Obj A} → {f : KHom c d } → {g : KHom b c } → {h : KHom a b } → |
|
71
709c1bde54dc
Kleisli category problem written
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
70
diff
changeset
|
262 (f * (g * h)) ⋍ ((f * g) * h) |
| 73 | 263 Kassoc {_} {_} {_} {_} {f} {g} {h} = Lemma9 (KMap f) (KMap g) (KMap h) |
| 3 | 264 |
| 78 | 265 KleisliCategory : Category c₁ c₂ ℓ |
| 75 | 266 KleisliCategory = |
| 267 record { Obj = Obj A | |
| 268 ; Hom = KHom | |
| 269 ; _o_ = _*_ | |
| 270 ; _≈_ = _⋍_ | |
| 271 ; Id = K-id | |
| 272 ; isCategory = isKleisliCategory | |
| 273 } | |
| 56 | 274 |
| 82 | 275 -- |
| 276 -- Resolution | |
| 277 -- T = U_T U_F | |
| 278 -- nat-ε | |
| 279 -- nat-η | |
| 280 -- | |
| 281 | |
| 300 | 282 ufmap : {a b : Obj A} (f : KHom a b ) → Hom A (FObj T a) (FObj T b) |
| 80 | 283 ufmap {a} {b} f = A [ TMap μ (b) o FMap T (KMap f) ] |
| 284 | |
| 75 | 285 U_T : Functor KleisliCategory A |
| 286 U_T = record { | |
| 287 FObj = FObj T | |
| 288 ; FMap = ufmap | |
| 289 ; isFunctor = record | |
| 290 { ≈-cong = ≈-cong | |
| 291 ; identity = identity | |
| 76 | 292 ; distr = distr1 |
| 75 | 293 } |
| 294 } where | |
| 295 identity : {a : Obj A} → A [ ufmap (K-id {a}) ≈ id1 A (FObj T a) ] | |
| 296 identity {a} = let open ≈-Reasoning (A) in | |
| 297 begin | |
| 298 TMap μ (a) o FMap T (TMap η a) | |
|
688
a5f2ca67e7c5
fix monad/adjunction definition
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
474
diff
changeset
|
299 ≈⟨ IsMonad.unity2 M ⟩ |
| 253 | 300 id (FObj T a) |
| 75 | 301 ∎ |
| 302 ≈-cong : {a b : Obj A} {f g : KHom a b} → A [ KMap f ≈ KMap g ] → A [ ufmap f ≈ ufmap g ] | |
| 303 ≈-cong {a} {b} {f} {g} f≈g = let open ≈-Reasoning (A) in | |
| 304 begin | |
| 305 TMap μ (b) o FMap T (KMap f) | |
| 306 ≈⟨ cdr (fcong T f≈g) ⟩ | |
| 307 TMap μ (b) o FMap T (KMap g) | |
| 308 ∎ | |
| 76 | 309 distr1 : {a b c : Obj A} {f : KHom a b} {g : KHom b c} → A [ ufmap (g * f) ≈ (A [ ufmap g o ufmap f ] )] |
| 310 distr1 {a} {b} {c} {f} {g} = let open ≈-Reasoning (A) in | |
| 75 | 311 begin |
| 312 ufmap (g * f) | |
| 76 | 313 ≈⟨⟩ |
| 314 ufmap {a} {c} ( record { KMap = TMap μ (c) o (FMap T (KMap g) o (KMap f)) } ) | |
| 315 ≈⟨⟩ | |
| 316 TMap μ (c) o FMap T ( TMap μ (c) o (FMap T (KMap g) o (KMap f))) | |
| 317 ≈⟨ cdr ( distr T) ⟩ | |
| 318 TMap μ (c) o (( FMap T ( TMap μ (c)) o FMap T (FMap T (KMap g) o (KMap f)))) | |
| 319 ≈⟨ assoc ⟩ | |
| 320 (TMap μ (c) o ( FMap T ( TMap μ (c)))) o FMap T (FMap T (KMap g) o (KMap f)) | |
|
688
a5f2ca67e7c5
fix monad/adjunction definition
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
474
diff
changeset
|
321 ≈⟨ car (sym (IsMonad.assoc M)) ⟩ |
| 76 | 322 (TMap μ (c) o ( TMap μ (FObj T c))) o FMap T (FMap T (KMap g) o (KMap f)) |
| 323 ≈⟨ sym assoc ⟩ | |
| 324 TMap μ (c) o (( TMap μ (FObj T c)) o FMap T (FMap T (KMap g) o (KMap f))) | |
| 325 ≈⟨ cdr (cdr (distr T)) ⟩ | |
| 326 TMap μ (c) o (( TMap μ (FObj T c)) o (FMap T (FMap T (KMap g)) o FMap T (KMap f))) | |
| 327 ≈⟨ cdr (assoc) ⟩ | |
| 328 TMap μ (c) o ((( TMap μ (FObj T c)) o (FMap T (FMap T (KMap g)))) o FMap T (KMap f)) | |
| 329 ≈⟨ sym (cdr (car (nat μ ))) ⟩ | |
| 330 TMap μ (c) o ((FMap T (KMap g ) o TMap μ (b)) o FMap T (KMap f )) | |
| 331 ≈⟨ cdr (sym assoc) ⟩ | |
| 332 TMap μ (c) o (FMap T (KMap g ) o ( TMap μ (b) o FMap T (KMap f ))) | |
| 333 ≈⟨ assoc ⟩ | |
| 334 ( TMap μ (c) o FMap T (KMap g ) ) o ( TMap μ (b) o FMap T (KMap f ) ) | |
| 335 ≈⟨⟩ | |
| 75 | 336 ufmap g o ufmap f |
| 337 ∎ | |
| 338 | |
| 339 | |
| 300 | 340 ffmap : {a b : Obj A} (f : Hom A a b) → KHom a b |
| 474 | 341 ffmap {a} {b} f = record { KMap = A [ TMap η b o f ] } |
| 75 | 342 |
| 343 F_T : Functor A KleisliCategory | |
| 344 F_T = record { | |
| 300 | 345 FObj = λ a → a |
| 75 | 346 ; FMap = ffmap |
| 347 ; isFunctor = record | |
| 348 { ≈-cong = ≈-cong | |
| 349 ; identity = identity | |
| 76 | 350 ; distr = distr1 |
| 75 | 351 } |
| 352 } where | |
| 353 identity : {a : Obj A} → A [ A [ TMap η a o id1 A a ] ≈ TMap η a ] | |
| 354 identity {a} = IsCategory.identityR ( Category.isCategory A) | |
| 82 | 355 -- Category.cod A f and Category.cod A g are actualy the same b, so we don't need cong-≈, just refl |
| 474 | 356 lemma1 : {b : Obj A} → A [ TMap η b ≈ TMap η b ] |
| 357 lemma1 = IsEquivalence.refl (IsCategory.isEquivalence ( Category.isCategory A )) | |
| 358 ≈-cong : {a b : Obj A} {f g : Hom A a b} → A [ f ≈ g ] → A [ A [ TMap η b o f ] ≈ A [ TMap η b o g ] ] | |
| 359 ≈-cong f≈g = (IsCategory.o-resp-≈ (Category.isCategory A)) f≈g lemma1 | |
| 76 | 360 distr1 : {a b c : Obj A} {f : Hom A a b} {g : Hom A b c} → |
| 75 | 361 ( ffmap (A [ g o f ]) ⋍ ( ffmap g * ffmap f ) ) |
| 77 | 362 distr1 {a} {b} {c} {f} {g} = let open ≈-Reasoning (A) in |
| 75 | 363 begin |
| 364 KMap (ffmap (A [ g o f ])) | |
| 77 | 365 ≈⟨⟩ |
| 366 TMap η (c) o (g o f) | |
| 367 ≈⟨ assoc ⟩ | |
| 368 (TMap η (c) o g) o f | |
| 369 ≈⟨ car (sym (nat η)) ⟩ | |
| 370 (FMap T g o TMap η (b)) o f | |
| 371 ≈⟨ sym idL ⟩ | |
| 253 | 372 id (FObj T c) o ((FMap T g o TMap η (b)) o f) |
|
688
a5f2ca67e7c5
fix monad/adjunction definition
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
474
diff
changeset
|
373 ≈⟨ sym (car (IsMonad.unity2 M)) ⟩ |
| 77 | 374 (TMap μ c o FMap T (TMap η c)) o ((FMap T g o TMap η (b)) o f) |
| 375 ≈⟨ sym assoc ⟩ | |
| 376 TMap μ c o ( FMap T (TMap η c) o ((FMap T g o TMap η (b)) o f) ) | |
| 377 ≈⟨ cdr (cdr (sym assoc)) ⟩ | |
| 378 TMap μ c o ( FMap T (TMap η c) o (FMap T g o (TMap η (b) o f))) | |
| 379 ≈⟨ cdr assoc ⟩ | |
| 380 TMap μ c o ( ( FMap T (TMap η c) o FMap T g ) o (TMap η (b) o f) ) | |
| 381 ≈⟨ sym (cdr ( car ( distr T ))) ⟩ | |
| 382 TMap μ c o ( ( FMap T (TMap η c o g)) o (TMap η (b) o f)) | |
| 383 ≈⟨ assoc ⟩ | |
| 384 (TMap μ c o ( FMap T (TMap η c o g))) o (TMap η (b) o f) | |
| 385 ≈⟨ assoc ⟩ | |
| 386 ((TMap μ c o (FMap T (TMap η c o g))) o TMap η b) o f | |
| 387 ≈⟨ sym assoc ⟩ | |
| 388 (TMap μ c o (FMap T (TMap η c o g))) o (TMap η b o f) | |
| 389 ≈⟨ sym assoc ⟩ | |
| 390 TMap μ c o ( (FMap T (TMap η c o g)) o (TMap η b o f) ) | |
| 391 ≈⟨⟩ | |
| 130 | 392 join M (TMap η c o g) (TMap η b o f) |
| 77 | 393 ≈⟨⟩ |
| 75 | 394 KMap ( ffmap g * ffmap f ) |
| 395 ∎ | |
| 396 | |
| 82 | 397 -- |
| 398 -- T = (U_T ○ F_T) | |
| 399 -- | |
| 400 | |
| 300 | 401 Lemma11-1 : ∀{a b : Obj A} → (f : Hom A a b ) → A [ FMap T f ≈ FMap (U_T ○ F_T) f ] |
| 79 | 402 Lemma11-1 {a} {b} f = let open ≈-Reasoning (A) in |
| 403 sym ( begin | |
| 404 FMap (U_T ○ F_T) f | |
| 405 ≈⟨⟩ | |
| 406 FMap U_T ( FMap F_T f ) | |
| 407 ≈⟨⟩ | |
| 408 TMap μ (b) o FMap T (KMap ( ffmap f ) ) | |
| 409 ≈⟨⟩ | |
| 410 TMap μ (b) o FMap T (TMap η (b) o f) | |
| 411 ≈⟨ cdr (distr T ) ⟩ | |
| 412 TMap μ (b) o ( FMap T (TMap η (b)) o FMap T f) | |
| 413 ≈⟨ assoc ⟩ | |
| 414 (TMap μ (b) o FMap T (TMap η (b))) o FMap T f | |
|
688
a5f2ca67e7c5
fix monad/adjunction definition
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
474
diff
changeset
|
415 ≈⟨ car (IsMonad.unity2 M) ⟩ |
| 253 | 416 id (FObj T b) o FMap T f |
| 79 | 417 ≈⟨ idL ⟩ |
| 418 FMap T f | |
| 419 ∎ ) | |
| 420 | |
| 82 | 421 -- construct ≃ |
| 422 | |
|
81
0404b2ba7db6
Resolution Adjoint proved.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
80
diff
changeset
|
423 Lemma11 : T ≃ (U_T ○ F_T) |
|
0404b2ba7db6
Resolution Adjoint proved.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
80
diff
changeset
|
424 Lemma11 f = Category.Cat.refl (Lemma11-1 f) |
| 78 | 425 |
| 82 | 426 -- |
| 427 -- natural transformations | |
| 428 -- | |
| 429 | |
| 78 | 430 nat-η : NTrans A A identityFunctor ( U_T ○ F_T ) |
| 467 | 431 nat-η = record { TMap = λ x → TMap η x ; isNTrans = record { commute = commute } } where |
| 432 commute : {a b : Obj A} {f : Hom A a b} | |
| 79 | 433 → A [ A [ ( FMap ( U_T ○ F_T ) f ) o ( TMap η a ) ] ≈ A [ (TMap η b ) o f ] ] |
| 467 | 434 commute {a} {b} {f} = let open ≈-Reasoning (A) in |
| 79 | 435 begin |
| 436 ( FMap ( U_T ○ F_T ) f ) o ( TMap η a ) | |
| 84 | 437 ≈⟨ sym (resp refl-hom (Lemma11-1 f)) ⟩ |
| 438 FMap T f o TMap η a | |
| 79 | 439 ≈⟨ nat η ⟩ |
| 84 | 440 TMap η b o f |
| 79 | 441 ∎ |
| 77 | 442 |
| 300 | 443 tmap-ε : (a : Obj A) → KHom (FObj T a) a |
| 78 | 444 tmap-ε a = record { KMap = id1 A (FObj T a) } |
| 445 | |
| 446 nat-ε : NTrans KleisliCategory KleisliCategory ( F_T ○ U_T ) identityFunctor | |
| 300 | 447 nat-ε = record { TMap = λ a → tmap-ε a; isNTrans = isNTrans1 } where |
| 130 | 448 commute1 : {a b : Obj A} {f : KHom a b} |
| 78 | 449 → (f * ( tmap-ε a ) ) ⋍ (( tmap-ε b ) * ( FMap (F_T ○ U_T) f ) ) |
| 130 | 450 commute1 {a} {b} {f} = let open ≈-Reasoning (A) in |
| 79 | 451 sym ( begin |
| 452 KMap (( tmap-ε b ) * ( FMap (F_T ○ U_T) f )) | |
| 80 | 453 ≈⟨⟩ |
| 253 | 454 TMap μ b o ( FMap T ( id (FObj T b) ) o ( KMap (FMap (F_T ○ U_T) f ) )) |
| 80 | 455 ≈⟨ cdr ( cdr ( |
| 456 begin | |
| 457 KMap (FMap (F_T ○ U_T) f ) | |
| 458 ≈⟨⟩ | |
| 459 KMap (FMap F_T (FMap U_T f)) | |
| 460 ≈⟨⟩ | |
| 461 TMap η (FObj T b) o (TMap μ (b) o FMap T (KMap f)) | |
| 462 ∎ | |
| 463 )) ⟩ | |
| 253 | 464 TMap μ b o ( FMap T ( id (FObj T b) ) o (TMap η (FObj T b) o (TMap μ (b) o FMap T (KMap f)))) |
| 80 | 465 ≈⟨ cdr (car (IsFunctor.identity (isFunctor T))) ⟩ |
| 253 | 466 TMap μ b o ( id (FObj T (FObj T b) ) o (TMap η (FObj T b) o (TMap μ (b) o FMap T (KMap f)))) |
| 80 | 467 ≈⟨ cdr idL ⟩ |
| 468 TMap μ b o (TMap η (FObj T b) o (TMap μ (b) o FMap T (KMap f))) | |
| 469 ≈⟨ assoc ⟩ | |
| 470 (TMap μ b o (TMap η (FObj T b))) o (TMap μ (b) o FMap T (KMap f)) | |
|
688
a5f2ca67e7c5
fix monad/adjunction definition
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
474
diff
changeset
|
471 ≈⟨ (car (IsMonad.unity1 M)) ⟩ |
| 253 | 472 id (FObj T b) o (TMap μ (b) o FMap T (KMap f)) |
| 80 | 473 ≈⟨ idL ⟩ |
| 474 TMap μ b o FMap T (KMap f) | |
| 475 ≈⟨ cdr (sym idR) ⟩ | |
| 253 | 476 TMap μ b o ( FMap T (KMap f) o id (FObj T a) ) |
| 80 | 477 ≈⟨⟩ |
| 79 | 478 KMap (f * ( tmap-ε a )) |
| 479 ∎ ) | |
| 300 | 480 isNTrans1 : IsNTrans KleisliCategory KleisliCategory ( F_T ○ U_T ) identityFunctor (λ a → tmap-ε a ) |
| 130 | 481 isNTrans1 = record { commute = commute1 } |
| 77 | 482 |
| 82 | 483 -- |
| 484 -- μ = U_T ε U_F | |
| 485 -- | |
| 300 | 486 tmap-μ : (a : Obj A) → Hom A (FObj ( U_T ○ F_T ) (FObj ( U_T ○ F_T ) a)) (FObj ( U_T ○ F_T ) a) |
| 95 | 487 tmap-μ a = FMap U_T ( TMap nat-ε ( FObj F_T a )) |
| 488 | |
| 489 nat-μ : NTrans A A (( U_T ○ F_T ) ○ ( U_T ○ F_T )) ( U_T ○ F_T ) | |
| 490 nat-μ = record { TMap = tmap-μ ; isNTrans = isNTrans1 } where | |
| 130 | 491 commute1 : {a b : Obj A} {f : Hom A a b} |
| 95 | 492 → A [ A [ (FMap (U_T ○ F_T) f) o ( tmap-μ a) ] ≈ A [ ( tmap-μ b ) o FMap (U_T ○ F_T) ( FMap (U_T ○ F_T) f) ] ] |
| 130 | 493 commute1 {a} {b} {f} = let open ≈-Reasoning (A) in |
| 95 | 494 sym ( begin |
| 495 ( tmap-μ b ) o FMap (U_T ○ F_T) ( FMap (U_T ○ F_T) f) | |
| 496 ≈⟨⟩ | |
| 497 ( FMap U_T ( TMap nat-ε ( FObj F_T b )) ) o FMap (U_T ○ F_T) ( FMap (U_T ○ F_T) f) | |
| 498 ≈⟨ sym ( distr U_T) ⟩ | |
| 499 FMap U_T ( KleisliCategory [ TMap nat-ε ( FObj F_T b ) o FMap F_T ( FMap (U_T ○ F_T) f) ] ) | |
| 500 ≈⟨ fcong U_T (sym (nat nat-ε)) ⟩ | |
| 501 FMap U_T ( KleisliCategory [ (FMap F_T f) o TMap nat-ε ( FObj F_T a ) ] ) | |
| 502 ≈⟨ distr U_T ⟩ | |
| 503 (FMap U_T (FMap F_T f)) o FMap U_T ( TMap nat-ε ( FObj F_T a )) | |
| 504 ≈⟨⟩ | |
| 505 (FMap (U_T ○ F_T) f) o ( tmap-μ a) | |
| 506 ∎ ) | |
| 507 isNTrans1 : IsNTrans A A (( U_T ○ F_T ) ○ ( U_T ○ F_T )) ( U_T ○ F_T ) tmap-μ | |
| 130 | 508 isNTrans1 = record { commute = commute1 } |
| 95 | 509 |
| 300 | 510 Lemma12 : {x : Obj A } → A [ TMap nat-μ x ≈ FMap U_T ( TMap nat-ε ( FObj F_T x ) ) ] |
| 80 | 511 Lemma12 {x} = let open ≈-Reasoning (A) in |
| 512 sym ( begin | |
| 513 FMap U_T ( TMap nat-ε ( FObj F_T x ) ) | |
| 514 ≈⟨⟩ | |
| 95 | 515 tmap-μ x |
| 516 ≈⟨⟩ | |
| 517 TMap nat-μ x | |
| 518 ∎ ) | |
| 519 | |
| 300 | 520 Lemma13 : {x : Obj A } → A [ TMap μ x ≈ FMap U_T ( TMap nat-ε ( FObj F_T x ) ) ] |
| 95 | 521 Lemma13 {x} = let open ≈-Reasoning (A) in |
| 522 sym ( begin | |
| 523 FMap U_T ( TMap nat-ε ( FObj F_T x ) ) | |
| 524 ≈⟨⟩ | |
| 253 | 525 TMap μ x o FMap T (id (FObj T x) ) |
| 80 | 526 ≈⟨ cdr (IsFunctor.identity (isFunctor T)) ⟩ |
| 253 | 527 TMap μ x o id (FObj T (FObj T x) ) |
| 80 | 528 ≈⟨ idR ⟩ |
| 529 TMap μ x | |
| 530 ∎ ) | |
| 78 | 531 |
|
688
a5f2ca67e7c5
fix monad/adjunction definition
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
474
diff
changeset
|
532 Adj_T : Adjunction A KleisliCategory |
| 84 | 533 Adj_T = record { |
|
688
a5f2ca67e7c5
fix monad/adjunction definition
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
474
diff
changeset
|
534 U = U_T ; |
|
a5f2ca67e7c5
fix monad/adjunction definition
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
474
diff
changeset
|
535 F = F_T ; |
|
a5f2ca67e7c5
fix monad/adjunction definition
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
474
diff
changeset
|
536 η = nat-η ; |
|
a5f2ca67e7c5
fix monad/adjunction definition
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
474
diff
changeset
|
537 ε = nat-ε ; |
| 80 | 538 isAdjunction = record { |
| 539 adjoint1 = adjoint1 ; | |
| 540 adjoint2 = adjoint2 | |
| 541 } | |
| 542 } where | |
| 543 adjoint1 : { b : Obj KleisliCategory } → | |
| 544 A [ A [ ( FMap U_T ( TMap nat-ε b)) o ( TMap nat-η ( FObj U_T b )) ] ≈ id1 A (FObj U_T b) ] | |
|
81
0404b2ba7db6
Resolution Adjoint proved.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
80
diff
changeset
|
545 adjoint1 {b} = let open ≈-Reasoning (A) in |
|
0404b2ba7db6
Resolution Adjoint proved.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
80
diff
changeset
|
546 begin |
|
0404b2ba7db6
Resolution Adjoint proved.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
80
diff
changeset
|
547 ( FMap U_T ( TMap nat-ε b)) o ( TMap nat-η ( FObj U_T b )) |
|
0404b2ba7db6
Resolution Adjoint proved.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
80
diff
changeset
|
548 ≈⟨⟩ |
| 253 | 549 (TMap μ (b) o FMap T (id (FObj T b ))) o ( TMap η ( FObj T b )) |
|
81
0404b2ba7db6
Resolution Adjoint proved.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
80
diff
changeset
|
550 ≈⟨ car ( cdr (IsFunctor.identity (isFunctor T))) ⟩ |
| 253 | 551 (TMap μ (b) o (id (FObj T (FObj T b )))) o ( TMap η ( FObj T b )) |
|
81
0404b2ba7db6
Resolution Adjoint proved.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
80
diff
changeset
|
552 ≈⟨ car idR ⟩ |
|
0404b2ba7db6
Resolution Adjoint proved.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
80
diff
changeset
|
553 TMap μ (b) o ( TMap η ( FObj T b )) |
|
688
a5f2ca67e7c5
fix monad/adjunction definition
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
474
diff
changeset
|
554 ≈⟨ IsMonad.unity1 M ⟩ |
| 253 | 555 id (FObj U_T b) |
|
81
0404b2ba7db6
Resolution Adjoint proved.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
80
diff
changeset
|
556 ∎ |
| 80 | 557 adjoint2 : {a : Obj A} → |
| 558 KleisliCategory [ KleisliCategory [ ( TMap nat-ε ( FObj F_T a )) o ( FMap F_T ( TMap nat-η a )) ] | |
| 87 | 559 ≈ id1 KleisliCategory (FObj F_T a) ] |
|
81
0404b2ba7db6
Resolution Adjoint proved.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
80
diff
changeset
|
560 adjoint2 {a} = let open ≈-Reasoning (A) in |
|
0404b2ba7db6
Resolution Adjoint proved.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
80
diff
changeset
|
561 begin |
|
0404b2ba7db6
Resolution Adjoint proved.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
80
diff
changeset
|
562 KMap (( TMap nat-ε ( FObj F_T a )) * ( FMap F_T ( TMap nat-η a )) ) |
|
0404b2ba7db6
Resolution Adjoint proved.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
80
diff
changeset
|
563 ≈⟨⟩ |
| 253 | 564 TMap μ a o (FMap T (id (FObj T a) ) o ((TMap η (FObj T a)) o (TMap η a))) |
|
81
0404b2ba7db6
Resolution Adjoint proved.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
80
diff
changeset
|
565 ≈⟨ cdr ( car ( IsFunctor.identity (isFunctor T))) ⟩ |
| 253 | 566 TMap μ a o ((id (FObj T (FObj T a) )) o ((TMap η (FObj T a)) o (TMap η a))) |
|
81
0404b2ba7db6
Resolution Adjoint proved.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
80
diff
changeset
|
567 ≈⟨ cdr ( idL ) ⟩ |
|
0404b2ba7db6
Resolution Adjoint proved.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
80
diff
changeset
|
568 TMap μ a o ((TMap η (FObj T a)) o (TMap η a)) |
|
0404b2ba7db6
Resolution Adjoint proved.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
80
diff
changeset
|
569 ≈⟨ assoc ⟩ |
|
0404b2ba7db6
Resolution Adjoint proved.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
80
diff
changeset
|
570 (TMap μ a o (TMap η (FObj T a))) o (TMap η a) |
|
688
a5f2ca67e7c5
fix monad/adjunction definition
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
474
diff
changeset
|
571 ≈⟨ car (IsMonad.unity1 M) ⟩ |
| 253 | 572 id (FObj T a) o (TMap η a) |
|
81
0404b2ba7db6
Resolution Adjoint proved.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
80
diff
changeset
|
573 ≈⟨ idL ⟩ |
|
0404b2ba7db6
Resolution Adjoint proved.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
80
diff
changeset
|
574 TMap η a |
|
0404b2ba7db6
Resolution Adjoint proved.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
80
diff
changeset
|
575 ≈⟨⟩ |
|
0404b2ba7db6
Resolution Adjoint proved.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
80
diff
changeset
|
576 TMap η (FObj F_T a) |
|
0404b2ba7db6
Resolution Adjoint proved.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
80
diff
changeset
|
577 ≈⟨⟩ |
|
0404b2ba7db6
Resolution Adjoint proved.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
80
diff
changeset
|
578 KMap (id1 KleisliCategory (FObj F_T a)) |
| 82 | 579 ∎ |
| 77 | 580 |
| 87 | 581 open MResolution |
| 84 | 582 |
|
688
a5f2ca67e7c5
fix monad/adjunction definition
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
474
diff
changeset
|
583 Resolution_T : MResolution A KleisliCategory ( record { T = T ; η = η ; μ = μ; isMonad = M } ) |
| 84 | 584 Resolution_T = record { |
|
688
a5f2ca67e7c5
fix monad/adjunction definition
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
474
diff
changeset
|
585 UR = U_T ; |
|
a5f2ca67e7c5
fix monad/adjunction definition
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
474
diff
changeset
|
586 FR = F_T ; |
|
a5f2ca67e7c5
fix monad/adjunction definition
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
474
diff
changeset
|
587 ηR = nat-η ; |
|
a5f2ca67e7c5
fix monad/adjunction definition
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
474
diff
changeset
|
588 εR = nat-ε ; |
|
a5f2ca67e7c5
fix monad/adjunction definition
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
474
diff
changeset
|
589 μR = nat-μ ; |
|
a5f2ca67e7c5
fix monad/adjunction definition
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
474
diff
changeset
|
590 Adj = Adjunction.isAdjunction Adj_T ; |
| 87 | 591 T=UF = Lemma11; |
| 592 μ=UεF = Lemma12 | |
| 84 | 593 } |
| 594 | |
|
97
2feec58bb02d
seprate comparison functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
96
diff
changeset
|
595 -- end |