Mercurial > hg > Members > kono > Proof > category
annotate nat.agda @ 71:709c1bde54dc
Kleisli category problem written
author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
---|---|
date | Fri, 26 Jul 2013 11:42:57 +0900 |
parents | fb3c48b375b3 |
children | cbc30519e961 |
rev | line source |
---|---|
0 | 1 module nat where |
2 | |
3 -- Monad | |
4 -- Category A | |
5 -- A = Category | |
22 | 6 -- Functor T : A → A |
0 | 7 --T(a) = t(a) |
8 --T(f) = tf(f) | |
9 | |
2 | 10 open import Category -- https://github.com/konn/category-agda |
0 | 11 open import Level |
56 | 12 --open import Category.HomReasoning |
13 open import HomReasoning | |
14 open import cat-utility | |
0 | 15 |
1 | 16 --T(g f) = T(g) T(f) |
17 | |
31 | 18 open Functor |
22 | 19 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 } |
20 → A [ ( FMap T (A [ g o f ] )) ≈ (A [ FMap T g o FMap T f ]) ] | |
21 Lemma1 = \t → IsFunctor.distr ( isFunctor t ) | |
0 | 22 |
23 | |
7 | 24 open NTrans |
1 | 25 Lemma2 : {c₁ c₂ l : Level} {A : Category c₁ c₂ l} {F G : Functor A A} |
22 | 26 → (μ : NTrans A A F G) → {a b : Obj A} { f : Hom A a b } |
30 | 27 → A [ A [ FMap G f o TMap μ a ] ≈ A [ TMap μ b o FMap F f ] ] |
22 | 28 Lemma2 = \n → IsNTrans.naturality ( isNTrans n ) |
0 | 29 |
30 open import Category.Cat | |
31 | |
22 | 32 -- η : 1_A → T |
33 -- μ : TT → T | |
0 | 34 -- μ(a)η(T(a)) = a |
35 -- μ(a)T(η(a)) = a | |
36 -- μ(a)(μ(T(a))) = μ(a)T(μ(a)) | |
37 | |
38 | |
2 | 39 open Monad |
40 Lemma3 : {c₁ c₂ ℓ : Level} {A : Category c₁ c₂ ℓ} | |
41 { T : Functor A A } | |
7 | 42 { η : NTrans A A identityFunctor T } |
43 { μ : NTrans A A (T ○ T) T } | |
22 | 44 { a : Obj A } → |
2 | 45 ( M : Monad A T η μ ) |
30 | 46 → A [ A [ TMap μ a o TMap μ ( FObj T a ) ] ≈ A [ TMap μ a o FMap T (TMap μ a) ] ] |
22 | 47 Lemma3 = \m → IsMonad.assoc ( isMonad m ) |
2 | 48 |
49 | |
50 Lemma4 : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) {a b : Obj A } { f : Hom A a b} | |
22 | 51 → A [ A [ Id {_} {_} {_} {A} b o f ] ≈ f ] |
52 Lemma4 = \a → IsCategory.identityL ( Category.isCategory a ) | |
0 | 53 |
3 | 54 Lemma5 : {c₁ c₂ ℓ : Level} {A : Category c₁ c₂ ℓ} |
55 { T : Functor A A } | |
7 | 56 { η : NTrans A A identityFunctor T } |
57 { μ : NTrans A A (T ○ T) T } | |
22 | 58 { a : Obj A } → |
3 | 59 ( M : Monad A T η μ ) |
30 | 60 → A [ A [ TMap μ a o TMap η ( FObj T a ) ] ≈ Id {_} {_} {_} {A} (FObj T a) ] |
22 | 61 Lemma5 = \m → IsMonad.unity1 ( isMonad m ) |
3 | 62 |
63 Lemma6 : {c₁ c₂ ℓ : Level} {A : Category c₁ c₂ ℓ} | |
64 { T : Functor A A } | |
7 | 65 { η : NTrans A A identityFunctor T } |
66 { μ : NTrans A A (T ○ T) T } | |
22 | 67 { a : Obj A } → |
3 | 68 ( M : Monad A T η μ ) |
30 | 69 → A [ A [ TMap μ a o (FMap T (TMap η a )) ] ≈ Id {_} {_} {_} {A} (FObj T a) ] |
22 | 70 Lemma6 = \m → IsMonad.unity2 ( isMonad m ) |
3 | 71 |
72 -- T = M x A | |
0 | 73 -- nat of η |
74 -- g ○ f = μ(c) T(g) f | |
75 -- η(b) ○ f = f | |
76 -- f ○ η(a) = f | |
22 | 77 -- h ○ (g ○ f) = (h ○ g) ○ f |
0 | 78 |
7 | 79 |
22 | 80 lemma12 : {c₁ c₂ ℓ : Level} (L : Category c₁ c₂ ℓ) { a b c : Obj L } → |
81 ( x : Hom L c a ) → ( y : Hom L b c ) → L [ L [ x o y ] ≈ L [ x o y ] ] | |
18 | 82 lemma12 L x y = |
83 let open ≈-Reasoning ( L ) in | |
84 begin L [ x o y ] ∎ | |
11 | 85 |
4 | 86 open Kleisli |
22 | 87 -- η(b) ○ f = f |
88 Lemma7 : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) → | |
56 | 89 { T : Functor A A } |
21 | 90 ( η : NTrans A A identityFunctor T ) |
7 | 91 { μ : NTrans A A (T ○ T) T } |
21 | 92 { a : Obj A } ( b : Obj A ) |
93 ( f : Hom A a ( FObj T b) ) | |
22 | 94 ( m : Monad A T η μ ) |
56 | 95 { k : Kleisli A T η μ m} |
68
829e0698f87f
join implicit parameter
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
66
diff
changeset
|
96 → A [ join k (TMap η b) f ≈ f ] |
56 | 97 Lemma7 c {T} η b f m {k} = |
21 | 98 let open ≈-Reasoning (c) |
99 μ = mu ( monad k ) | |
100 in | |
101 begin | |
68
829e0698f87f
join implicit parameter
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
66
diff
changeset
|
102 join k (TMap η b) f |
21 | 103 ≈⟨ refl-hom ⟩ |
30 | 104 c [ TMap μ b o c [ FMap T ((TMap η b)) o f ] ] |
21 | 105 ≈⟨ IsCategory.associative (Category.isCategory c) ⟩ |
30 | 106 c [ c [ TMap μ b o FMap T ((TMap η b)) ] o f ] |
28 | 107 ≈⟨ car ( IsMonad.unity2 ( isMonad ( monad k )) ) ⟩ |
22 | 108 c [ id (FObj T b) o f ] |
21 | 109 ≈⟨ IsCategory.identityL (Category.isCategory c) ⟩ |
110 f | |
111 ∎ | |
7 | 112 |
22 | 113 -- f ○ η(a) = f |
114 Lemma8 : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) | |
115 ( T : Functor A A ) | |
116 ( η : NTrans A A identityFunctor T ) | |
7 | 117 { μ : NTrans A A (T ○ T) T } |
22 | 118 ( a : Obj A ) ( b : Obj A ) |
119 ( f : Hom A a ( FObj T b) ) | |
120 ( m : Monad A T η μ ) | |
121 ( k : Kleisli A T η μ m) | |
68
829e0698f87f
join implicit parameter
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
66
diff
changeset
|
122 → A [ join k f (TMap η a) ≈ f ] |
22 | 123 Lemma8 c T η a b f m k = |
124 begin | |
68
829e0698f87f
join implicit parameter
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
66
diff
changeset
|
125 join k f (TMap η a) |
22 | 126 ≈⟨ refl-hom ⟩ |
30 | 127 c [ TMap μ b o c [ FMap T f o (TMap η a) ] ] |
66 | 128 ≈⟨ cdr ( nat η ) ⟩ |
30 | 129 c [ TMap μ b o c [ (TMap η ( FObj T b)) o f ] ] |
22 | 130 ≈⟨ IsCategory.associative (Category.isCategory c) ⟩ |
30 | 131 c [ c [ TMap μ b o (TMap η ( FObj T b)) ] o f ] |
28 | 132 ≈⟨ car ( IsMonad.unity1 ( isMonad ( monad k )) ) ⟩ |
22 | 133 c [ id (FObj T b) o f ] |
134 ≈⟨ IsCategory.identityL (Category.isCategory c) ⟩ | |
135 f | |
136 ∎ where | |
137 open ≈-Reasoning (c) | |
138 μ = mu ( monad k ) | |
5 | 139 |
22 | 140 -- h ○ (g ○ f) = (h ○ g) ○ f |
23 | 141 Lemma9 : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) |
56 | 142 { T : Functor A A } |
143 { η : NTrans A A identityFunctor T } | |
144 { μ : NTrans A A (T ○ T) T } | |
145 { a b c d : Obj A } | |
23 | 146 ( f : Hom A a ( FObj T b) ) |
147 ( g : Hom A b ( FObj T c) ) | |
148 ( h : Hom A c ( FObj T d) ) | |
149 ( m : Monad A T η μ ) | |
56 | 150 { k : Kleisli A T η μ m} |
68
829e0698f87f
join implicit parameter
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
66
diff
changeset
|
151 → A [ join k h (join k g f) ≈ join k ( join k h g) f ] |
56 | 152 Lemma9 A {T} {η} {μ} {a} {b} {c} {d} f g h m {k} = |
24 | 153 begin |
68
829e0698f87f
join implicit parameter
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
66
diff
changeset
|
154 join k h (join k g f) |
30 | 155 ≈⟨⟩ |
68
829e0698f87f
join implicit parameter
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
66
diff
changeset
|
156 join k h ( ( TMap μ c o ( FMap T g o f ) ) ) |
28 | 157 ≈⟨ refl-hom ⟩ |
30 | 158 ( TMap μ d o ( FMap T h o ( TMap μ c o ( FMap T g o f ) ) ) ) |
28 | 159 ≈⟨ cdr ( cdr ( assoc )) ⟩ |
30 | 160 ( TMap μ d o ( FMap T h o ( ( TMap μ c o FMap T g ) o f ) ) ) |
28 | 161 ≈⟨ assoc ⟩ --- ( f o ( g o h ) ) = ( ( f o g ) o h ) |
30 | 162 ( ( TMap μ d o FMap T h ) o ( (TMap μ c o FMap T g ) o f ) ) |
25 | 163 ≈⟨ assoc ⟩ |
30 | 164 ( ( ( TMap μ d o FMap T h ) o (TMap μ c o FMap T g ) ) o f ) |
28 | 165 ≈⟨ car (sym assoc) ⟩ |
30 | 166 ( ( TMap μ d o ( FMap T h o ( TMap μ c o FMap T g ) ) ) o f ) |
28 | 167 ≈⟨ car ( cdr (assoc) ) ⟩ |
30 | 168 ( ( TMap μ d o ( ( FMap T h o TMap μ c ) o FMap T g ) ) o f ) |
28 | 169 ≈⟨ car assoc ⟩ |
30 | 170 ( ( ( TMap μ d o ( FMap T h o TMap μ c ) ) o FMap T g ) o f ) |
28 | 171 ≈⟨ car (car ( cdr ( begin |
30 | 172 ( FMap T h o TMap μ c ) |
66 | 173 ≈⟨ nat μ ⟩ |
30 | 174 ( TMap μ (FObj T d) o FMap T (FMap T h) ) |
25 | 175 ∎ |
176 ))) ⟩ | |
30 | 177 ( ( ( TMap μ d o ( TMap μ ( FObj T d) o FMap T ( FMap T h ) ) ) o FMap T g ) o f ) |
28 | 178 ≈⟨ car (sym assoc) ⟩ |
30 | 179 ( ( TMap μ d o ( ( TMap μ ( FObj T d) o FMap T ( FMap T h ) ) o FMap T g ) ) o f ) |
28 | 180 ≈⟨ car ( cdr (sym assoc) ) ⟩ |
30 | 181 ( ( TMap μ d o ( TMap μ ( FObj T d) o ( FMap T ( FMap T h ) o FMap T g ) ) ) o f ) |
28 | 182 ≈⟨ car ( cdr (cdr (sym (distr T )))) ⟩ |
30 | 183 ( ( TMap μ d o ( TMap μ ( FObj T d) o FMap T ( ( FMap T h o g ) ) ) ) o f ) |
28 | 184 ≈⟨ car assoc ⟩ |
30 | 185 ( ( ( TMap μ d o TMap μ ( FObj T d) ) o FMap T ( ( FMap T h o g ) ) ) o f ) |
28 | 186 ≈⟨ car ( car ( |
27 | 187 begin |
30 | 188 ( TMap μ d o TMap μ (FObj T d) ) |
27 | 189 ≈⟨ IsMonad.assoc ( isMonad m) ⟩ |
30 | 190 ( TMap μ d o FMap T (TMap μ d) ) |
27 | 191 ∎ |
192 )) ⟩ | |
30 | 193 ( ( ( TMap μ d o FMap T ( TMap μ d) ) o FMap T ( ( FMap T h o g ) ) ) o f ) |
28 | 194 ≈⟨ car (sym assoc) ⟩ |
30 | 195 ( ( TMap μ d o ( FMap T ( TMap μ d ) o FMap T ( ( FMap T h o g ) ) ) ) o f ) |
24 | 196 ≈⟨ sym assoc ⟩ |
30 | 197 ( TMap μ d o ( ( FMap T ( TMap μ d ) o FMap T ( ( FMap T h o g ) ) ) o f ) ) |
28 | 198 ≈⟨ cdr ( car ( sym ( distr T ))) ⟩ |
30 | 199 ( TMap μ d o ( FMap T ( ( ( TMap μ d ) o ( FMap T h o g ) ) ) o f ) ) |
23 | 200 ≈⟨ refl-hom ⟩ |
68
829e0698f87f
join implicit parameter
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
66
diff
changeset
|
201 join k ( ( TMap μ d o ( FMap T h o g ) ) ) f |
23 | 202 ≈⟨ refl-hom ⟩ |
68
829e0698f87f
join implicit parameter
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
66
diff
changeset
|
203 join k ( join k h g) f |
24 | 204 ∎ where open ≈-Reasoning (A) |
3 | 205 |
70 | 206 KHom1 : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) → ( T : Functor A A ) (a : Obj A) → (b : Obj A) -> Set (c₂ ⊔ c₁) |
207 KHom1 = {!!} | |
208 | |
209 record KHom {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) ( T : Functor A A ) (a : Obj A) (b : Obj A) | |
210 : Set (suc (c₂ ⊔ c₁)) where | |
211 field | |
212 KMap : Hom A a ( FObj T b ) | |
69
84a150c980ce
generalized distr and assco1
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
68
diff
changeset
|
213 |
71
709c1bde54dc
Kleisli category problem written
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
70
diff
changeset
|
214 K-id : {c₁ c₂ ℓ : Level} {A : Category c₁ c₂ ℓ} { T : Functor A A } {η : NTrans A A identityFunctor T} {a : Obj A} → KHom A T a a |
709c1bde54dc
Kleisli category problem written
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
70
diff
changeset
|
215 K-id {_} {_} {_} {A} {T} {η} {a = a} = record { KMap = TMap η a } |
56 | 216 |
69
84a150c980ce
generalized distr and assco1
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
68
diff
changeset
|
217 open import Relation.Binary.Core |
56 | 218 |
71
709c1bde54dc
Kleisli category problem written
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
70
diff
changeset
|
219 _⋍_ : ∀{c₁ c₂ ℓ} {A : Category c₁ c₂ ℓ} { T : Functor A A } |
709c1bde54dc
Kleisli category problem written
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
70
diff
changeset
|
220 { a : Obj A } { b : Obj A } (f g : KHom A T a b ) -> Set (suc ((c₂ ⊔ c₁) ⊔ ℓ)) |
709c1bde54dc
Kleisli category problem written
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
70
diff
changeset
|
221 _⋍_ = {!!} |
709c1bde54dc
Kleisli category problem written
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
70
diff
changeset
|
222 |
709c1bde54dc
Kleisli category problem written
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
70
diff
changeset
|
223 |
709c1bde54dc
Kleisli category problem written
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
70
diff
changeset
|
224 _*_ : { c₁ c₂ ℓ : Level} { A : Category c₁ c₂ ℓ } |
709c1bde54dc
Kleisli category problem written
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
70
diff
changeset
|
225 { T : Functor A A } |
709c1bde54dc
Kleisli category problem written
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
70
diff
changeset
|
226 { η : NTrans A A identityFunctor T } |
709c1bde54dc
Kleisli category problem written
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
70
diff
changeset
|
227 { μ : NTrans A A (T ○ T) T } |
709c1bde54dc
Kleisli category problem written
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
70
diff
changeset
|
228 { M : Monad A T η μ } → |
709c1bde54dc
Kleisli category problem written
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
70
diff
changeset
|
229 { K : Kleisli A T η μ M } → |
709c1bde54dc
Kleisli category problem written
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
70
diff
changeset
|
230 { a b : Obj A } → { c : Obj A } → |
709c1bde54dc
Kleisli category problem written
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
70
diff
changeset
|
231 ( Hom A b ( FObj T c )) → ( Hom A a ( FObj T b)) → Hom A a ( FObj T c ) |
709c1bde54dc
Kleisli category problem written
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
70
diff
changeset
|
232 _*_ {_} {_} {_} {_} {_} {_} {_} {_} {K} {a} {b} {c} g f = join K {a} {b} {c} g f |
70 | 233 |
69
84a150c980ce
generalized distr and assco1
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
68
diff
changeset
|
234 isKleisliCategory : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) |
84a150c980ce
generalized distr and assco1
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
68
diff
changeset
|
235 { T : Functor A A } |
84a150c980ce
generalized distr and assco1
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
68
diff
changeset
|
236 { η : NTrans A A identityFunctor T } |
84a150c980ce
generalized distr and assco1
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
68
diff
changeset
|
237 { μ : NTrans A A (T ○ T) T } |
84a150c980ce
generalized distr and assco1
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
68
diff
changeset
|
238 ( m : Monad A T η μ ) |
84a150c980ce
generalized distr and assco1
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
68
diff
changeset
|
239 { k : Kleisli A T η μ m} → |
71
709c1bde54dc
Kleisli category problem written
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
70
diff
changeset
|
240 IsCategory ( Obj A ) ( KHom A T ) _⋍_ _*_ K-id |
709c1bde54dc
Kleisli category problem written
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
70
diff
changeset
|
241 isKleisliCategory A {T} {η} m = record { isEquivalence = isEquivalence A T |
709c1bde54dc
Kleisli category problem written
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
70
diff
changeset
|
242 ; identityL = KidL |
709c1bde54dc
Kleisli category problem written
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
70
diff
changeset
|
243 ; identityR = KidR |
709c1bde54dc
Kleisli category problem written
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
70
diff
changeset
|
244 ; o-resp-≈ = Ko-resp |
709c1bde54dc
Kleisli category problem written
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
70
diff
changeset
|
245 ; associative = Kassoc |
69
84a150c980ce
generalized distr and assco1
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
68
diff
changeset
|
246 } |
84a150c980ce
generalized distr and assco1
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
68
diff
changeset
|
247 where |
71
709c1bde54dc
Kleisli category problem written
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
70
diff
changeset
|
248 isEquivalence : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) → ( T : Functor A A ) -> { a b : Obj A } -> |
709c1bde54dc
Kleisli category problem written
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
70
diff
changeset
|
249 IsEquivalence {_} {_} {KHom A T a b} _⋍_ |
709c1bde54dc
Kleisli category problem written
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
70
diff
changeset
|
250 isEquivalence A T {C} {D} = |
709c1bde54dc
Kleisli category problem written
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
70
diff
changeset
|
251 record { refl = λ {F} → ⋍-refl {F} |
709c1bde54dc
Kleisli category problem written
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
70
diff
changeset
|
252 ; sym = λ {F} {G} → ⋍-sym {F} {G} |
709c1bde54dc
Kleisli category problem written
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
70
diff
changeset
|
253 ; trans = λ {F} {G} {H} → ⋍-trans {F} {G} {H} |
709c1bde54dc
Kleisli category problem written
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
70
diff
changeset
|
254 } where |
709c1bde54dc
Kleisli category problem written
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
70
diff
changeset
|
255 ⋍-refl : {F : KHom A T C D} → F ⋍ F |
709c1bde54dc
Kleisli category problem written
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
70
diff
changeset
|
256 ⋍-refl = {!!} |
709c1bde54dc
Kleisli category problem written
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
70
diff
changeset
|
257 ⋍-sym : {F G : KHom A T C D} → F ⋍ G → G ⋍ F |
709c1bde54dc
Kleisli category problem written
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
70
diff
changeset
|
258 ⋍-sym = {!!} |
709c1bde54dc
Kleisli category problem written
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
70
diff
changeset
|
259 ⋍-trans : {F G H : KHom A T C D} → F ⋍ G → G ⋍ H → F ⋍ H |
709c1bde54dc
Kleisli category problem written
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
70
diff
changeset
|
260 ⋍-trans = {!!} |
709c1bde54dc
Kleisli category problem written
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
70
diff
changeset
|
261 KidL : {c₁ c₂ ℓ : Level} { A : Category c₁ c₂ ℓ} { T : Functor A A } |
69
84a150c980ce
generalized distr and assco1
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
68
diff
changeset
|
262 { η : NTrans A A identityFunctor T } |
71
709c1bde54dc
Kleisli category problem written
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
70
diff
changeset
|
263 { μ : NTrans A A (T ○ T) T } { m : Monad A T η μ } → {C D : Obj A} -> {f : KHom A T C D} → (K-id * f) ⋍ f |
69
84a150c980ce
generalized distr and assco1
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
68
diff
changeset
|
264 KidL = {!!} |
71
709c1bde54dc
Kleisli category problem written
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
70
diff
changeset
|
265 KidR : {c₁ c₂ ℓ : Level} { A : Category c₁ c₂ ℓ} { T : Functor A A } |
709c1bde54dc
Kleisli category problem written
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
70
diff
changeset
|
266 { η : NTrans A A identityFunctor T } |
709c1bde54dc
Kleisli category problem written
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
70
diff
changeset
|
267 { μ : NTrans A A (T ○ T) T } { m : Monad A T η μ } → {C D : Obj A} -> {f : KHom A T C D} → (f * K-id) ⋍ f |
69
84a150c980ce
generalized distr and assco1
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
68
diff
changeset
|
268 KidR = {!!} |
71
709c1bde54dc
Kleisli category problem written
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
70
diff
changeset
|
269 Ko-resp : {c₁ c₂ ℓ : Level} { A : Category c₁ c₂ ℓ} { T : Functor A A } |
709c1bde54dc
Kleisli category problem written
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
70
diff
changeset
|
270 { η : NTrans A A identityFunctor T } |
709c1bde54dc
Kleisli category problem written
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
70
diff
changeset
|
271 { μ : NTrans A A (T ○ T) T } { m : Monad A T η μ } → {a b c : Obj A} -> {f g : KHom A T a b } → {h i : KHom A T b c } → |
709c1bde54dc
Kleisli category problem written
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
70
diff
changeset
|
272 f ⋍ g → h ⋍ i → (h * f) ⋍ (i * g) |
69
84a150c980ce
generalized distr and assco1
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
68
diff
changeset
|
273 Ko-resp = {!!} |
71
709c1bde54dc
Kleisli category problem written
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
70
diff
changeset
|
274 Kassoc : {c₁ c₂ ℓ : Level} { A : Category c₁ c₂ ℓ} { T : Functor A A } |
709c1bde54dc
Kleisli category problem written
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
70
diff
changeset
|
275 { η : NTrans A A identityFunctor T } |
709c1bde54dc
Kleisli category problem written
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
70
diff
changeset
|
276 { μ : NTrans A A (T ○ T) T } { m : Monad A T η μ } → {a b c : Obj A} -> {f g : KHom A T a b } → {h i : KHom A T b c } → |
709c1bde54dc
Kleisli category problem written
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
70
diff
changeset
|
277 (f * (g * h)) ⋍ ((f * g) * h) |
69
84a150c980ce
generalized distr and assco1
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
68
diff
changeset
|
278 Kassoc = {!!} |
3 | 279 |
280 -- Kleisli : | |
281 -- Kleisli = record { Hom = | |
282 -- ; Hom = _⟶_ | |
283 -- ; Id = IdProd | |
284 -- ; _o_ = _∘_ | |
285 -- ; _≈_ = _≈_ | |
286 -- ; isCategory = record { isEquivalence = record { refl = λ {φ} → ≈-refl {φ = φ} | |
287 -- ; sym = λ {φ ψ} → ≈-symm {φ = φ} {ψ} | |
288 -- ; trans = λ {φ ψ σ} → ≈-trans {φ = φ} {ψ} {σ} | |
289 -- } | |
290 -- ; identityL = identityL | |
291 -- ; identityR = identityR | |
292 -- ; o-resp-≈ = o-resp-≈ | |
293 -- ; associative = associative | |
294 -- } | |
295 -- } | |
56 | 296 |
63 | 297 ---- |
298 -- | |
299 -- Adjunction to Monad | |
300 -- | |
301 ---- | |
56 | 302 |
63 | 303 open Adjunction |
58 | 304 |
305 UεF : {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} (A : Category c₁ c₂ ℓ) (B : Category c₁' c₂' ℓ') | |
306 ( U : Functor B A ) | |
307 ( F : Functor A B ) | |
308 ( ε : NTrans B B ( F ○ U ) identityFunctor ) → NTrans A A (( U ○ F ) ○ ( U ○ F )) ( U ○ F ) | |
63 | 309 UεF A B U F ε = lemma11 ( |
310 Functor*Nat A {B} A U {( F ○ U) ○ F} {identityFunctor ○ F} ( Nat*Functor A {B} B { F ○ U} {identityFunctor} ε F) ) where | |
311 lemma11 : NTrans A A ( U ○ ((F ○ U) ○ F )) ( U ○ (identityFunctor ○ F) ) | |
66 | 312 → NTrans A A (( U ○ F ) ○ ( U ○ F )) ( U ○ F ) |
63 | 313 lemma11 n = record { TMap = \a → TMap n a; isNTrans = record { naturality = IsNTrans.naturality ( isNTrans n ) }} |
58 | 314 |
56 | 315 Adj2Monad : {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} (A : Category c₁ c₂ ℓ) (B : Category c₁' c₂' ℓ') |
316 { U : Functor B A } | |
317 { F : Functor A B } | |
318 { η : NTrans A A identityFunctor ( U ○ F ) } | |
319 { ε : NTrans B B ( F ○ U ) identityFunctor } → | |
58 | 320 Adjunction A B U F η ε → Monad A (U ○ F) η (UεF A B U F ε) |
56 | 321 Adj2Monad A B {U} {F} {η} {ε} adj = record { |
322 isMonad = record { | |
60 | 323 assoc = assoc1; |
324 unity1 = unity1; | |
325 unity2 = unity2 | |
56 | 326 } |
60 | 327 } where |
328 T : Functor A A | |
329 T = U ○ F | |
330 μ : NTrans A A ( T ○ T ) T | |
331 μ = UεF A B U F ε | |
63 | 332 lemma-assoc1 : {a b : Obj B} → ( f : Hom B a b) → |
333 B [ B [ f o TMap ε a ] ≈ B [ TMap ε b o FMap F (FMap U f ) ] ] | |
334 lemma-assoc1 f = IsNTrans.naturality ( isNTrans ε ) | |
60 | 335 assoc1 : {a : Obj A} → A [ A [ TMap μ a o TMap μ ( FObj T a ) ] ≈ A [ TMap μ a o FMap T (TMap μ a) ] ] |
62 | 336 assoc1 {a} = let open ≈-Reasoning (A) in |
337 begin | |
338 TMap μ a o TMap μ ( FObj T a ) | |
339 ≈⟨⟩ | |
340 (FMap U (TMap ε ( FObj F a ))) o (FMap U (TMap ε ( FObj F ( FObj U (FObj F a ))))) | |
66 | 341 ≈⟨ sym (distr U) ⟩ |
62 | 342 FMap U (B [ TMap ε ( FObj F a ) o TMap ε ( FObj F ( FObj U (FObj F a ))) ] ) |
63 | 343 ≈⟨ (IsFunctor.≈-cong (isFunctor U)) (lemma-assoc1 ( TMap ε (FObj F a ))) ⟩ |
62 | 344 FMap U (B [ (TMap ε ( FObj F a )) o FMap F (FMap U (TMap ε ( FObj F a ))) ] ) |
66 | 345 ≈⟨ distr U ⟩ |
62 | 346 (FMap U (TMap ε ( FObj F a ))) o FMap U (FMap F (FMap U (TMap ε ( FObj F a )))) |
347 ≈⟨⟩ | |
348 TMap μ a o FMap T (TMap μ a) | |
349 ∎ | |
60 | 350 unity1 : {a : Obj A} → A [ A [ TMap μ a o TMap η ( FObj T a ) ] ≈ Id {_} {_} {_} {A} (FObj T a) ] |
61 | 351 unity1 {a} = let open ≈-Reasoning (A) in |
352 begin | |
353 TMap μ a o TMap η ( FObj T a ) | |
354 ≈⟨⟩ | |
355 (FMap U (TMap ε ( FObj F a ))) o TMap η ( FObj U ( FObj F a )) | |
356 ≈⟨ IsAdjunction.adjoint1 ( isAdjunction adj ) ⟩ | |
357 id (FObj U ( FObj F a )) | |
358 ≈⟨⟩ | |
359 id (FObj T a) | |
360 ∎ | |
60 | 361 unity2 : {a : Obj A} → A [ A [ TMap μ a o (FMap T (TMap η a ))] ≈ Id {_} {_} {_} {A} (FObj T a) ] |
362 unity2 {a} = let open ≈-Reasoning (A) in | |
363 begin | |
364 TMap μ a o (FMap T (TMap η a )) | |
365 ≈⟨⟩ | |
366 (FMap U (TMap ε ( FObj F a ))) o (FMap U ( FMap F (TMap η a ))) | |
66 | 367 ≈⟨ sym (distr U ) ⟩ |
60 | 368 FMap U ( B [ (TMap ε ( FObj F a )) o ( FMap F (TMap η a )) ]) |
369 ≈⟨ (IsFunctor.≈-cong (isFunctor U)) (IsAdjunction.adjoint2 ( isAdjunction adj )) ⟩ | |
370 FMap U ( id1 B (FObj F a) ) | |
371 ≈⟨ IsFunctor.identity ( isFunctor U ) ⟩ | |
372 id (FObj T a) | |
373 ∎ |