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