Mercurial > hg > Members > kono > Proof > category
annotate nat.agda @ 96:85425bd12835
fix
author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
---|---|
date | Mon, 29 Jul 2013 14:47:57 +0900 |
parents | 4be27d290ea2 |
children | 2feec58bb02d |
rev | line source |
---|---|
82 | 1 -- -- -- -- -- -- -- -- |
2 -- Monad to Kelisli Category | |
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 |
cbc30519e961
stack overflow solved by moving implicit parameters to module parameters
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
71
diff
changeset
|
23 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
|
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 } |
cbc30519e961
stack overflow solved by moving implicit parameters to module parameters
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
71
diff
changeset
|
27 { 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
|
28 { 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
|
29 |
0 | 30 |
1 | 31 --T(g f) = T(g) T(f) |
32 | |
31 | 33 open Functor |
22 | 34 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 } |
35 → A [ ( FMap T (A [ g o f ] )) ≈ (A [ FMap T g o FMap T f ]) ] | |
36 Lemma1 = \t → IsFunctor.distr ( isFunctor t ) | |
0 | 37 |
38 | |
7 | 39 open NTrans |
1 | 40 Lemma2 : {c₁ c₂ l : Level} {A : Category c₁ c₂ l} {F G : Functor A A} |
22 | 41 → (μ : NTrans A A F G) → {a b : Obj A} { f : Hom A a b } |
30 | 42 → A [ A [ FMap G f o TMap μ a ] ≈ A [ TMap μ b o FMap F f ] ] |
22 | 43 Lemma2 = \n → IsNTrans.naturality ( isNTrans n ) |
0 | 44 |
82 | 45 -- Laws of Monad |
46 -- | |
22 | 47 -- η : 1_A → T |
48 -- μ : TT → T | |
82 | 49 -- μ(a)η(T(a)) = a -- unity law 1 |
50 -- μ(a)T(η(a)) = a -- unity law 2 | |
51 -- μ(a)(μ(T(a))) = μ(a)T(μ(a)) -- association law | |
0 | 52 |
53 | |
2 | 54 open Monad |
55 Lemma3 : {c₁ c₂ ℓ : Level} {A : Category c₁ c₂ ℓ} | |
56 { T : Functor A A } | |
7 | 57 { η : NTrans A A identityFunctor T } |
58 { μ : NTrans A A (T ○ T) T } | |
22 | 59 { a : Obj A } → |
2 | 60 ( M : Monad A T η μ ) |
30 | 61 → A [ A [ TMap μ a o TMap μ ( FObj T a ) ] ≈ A [ TMap μ a o FMap T (TMap μ a) ] ] |
22 | 62 Lemma3 = \m → IsMonad.assoc ( isMonad m ) |
2 | 63 |
64 | |
65 Lemma4 : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) {a b : Obj A } { f : Hom A a b} | |
22 | 66 → A [ A [ Id {_} {_} {_} {A} b o f ] ≈ f ] |
67 Lemma4 = \a → IsCategory.identityL ( Category.isCategory a ) | |
0 | 68 |
3 | 69 Lemma5 : {c₁ c₂ ℓ : Level} {A : Category c₁ c₂ ℓ} |
70 { T : Functor A A } | |
7 | 71 { η : NTrans A A identityFunctor T } |
72 { μ : NTrans A A (T ○ T) T } | |
22 | 73 { a : Obj A } → |
3 | 74 ( M : Monad A T η μ ) |
30 | 75 → A [ A [ TMap μ a o TMap η ( FObj T a ) ] ≈ Id {_} {_} {_} {A} (FObj T a) ] |
22 | 76 Lemma5 = \m → IsMonad.unity1 ( isMonad m ) |
3 | 77 |
78 Lemma6 : {c₁ c₂ ℓ : Level} {A : Category c₁ c₂ ℓ} | |
79 { T : Functor A A } | |
7 | 80 { η : NTrans A A identityFunctor T } |
81 { μ : NTrans A A (T ○ T) T } | |
22 | 82 { a : Obj A } → |
3 | 83 ( M : Monad A T η μ ) |
30 | 84 → A [ A [ TMap μ a o (FMap T (TMap η a )) ] ≈ Id {_} {_} {_} {A} (FObj T a) ] |
22 | 85 Lemma6 = \m → IsMonad.unity2 ( isMonad m ) |
3 | 86 |
82 | 87 -- Laws of Kleisli Category |
88 -- | |
0 | 89 -- nat of η |
82 | 90 -- g ○ f = μ(c) T(g) f -- join definition |
91 -- η(b) ○ f = f -- left id (Lemma7) | |
92 -- f ○ η(a) = f -- right id (Lemma8) | |
93 -- h ○ (g ○ f) = (h ○ g) ○ f -- assocation law (Lemma9) | |
11 | 94 |
4 | 95 open Kleisli |
22 | 96 -- η(b) ○ f = f |
73 | 97 Lemma7 : { a : Obj A } { b : Obj A } ( f : Hom A a ( FObj T b) ) |
98 → A [ join K (TMap η b) f ≈ f ] | |
99 Lemma7 {_} {b} f = | |
100 let open ≈-Reasoning (A) in | |
21 | 101 begin |
73 | 102 join K (TMap η b) f |
21 | 103 ≈⟨ refl-hom ⟩ |
73 | 104 A [ TMap μ b o A [ FMap T ((TMap η b)) o f ] ] |
105 ≈⟨ IsCategory.associative (Category.isCategory A) ⟩ | |
106 A [ A [ TMap μ b o FMap T ((TMap η b)) ] o f ] | |
107 ≈⟨ car ( IsMonad.unity2 ( isMonad ( monad K )) ) ⟩ | |
108 A [ id (FObj T b) o f ] | |
109 ≈⟨ IsCategory.identityL (Category.isCategory A) ⟩ | |
21 | 110 f |
111 ∎ | |
7 | 112 |
22 | 113 -- f ○ η(a) = f |
73 | 114 Lemma8 : { a : Obj A } { b : Obj A } |
22 | 115 ( 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
|
116 → A [ join K f (TMap η a) ≈ f ] |
73 | 117 Lemma8 {a} {b} f = |
22 | 118 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
|
119 join K f (TMap η a) |
22 | 120 ≈⟨ 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
|
121 A [ TMap μ b o A [ FMap T f o (TMap η a) ] ] |
66 | 122 ≈⟨ 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
|
123 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
|
124 ≈⟨ 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
|
125 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
|
126 ≈⟨ 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
|
127 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
|
128 ≈⟨ IsCategory.identityL (Category.isCategory A) ⟩ |
22 | 129 f |
130 ∎ 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
|
131 open ≈-Reasoning (A) |
5 | 132 |
22 | 133 -- 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
|
134 Lemma9 : { a b c d : Obj A } |
73 | 135 ( h : Hom A c ( FObj T d) ) |
23 | 136 ( g : Hom A b ( FObj T c) ) |
73 | 137 ( 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
|
138 → A [ join K h (join K g f) ≈ join K ( join K h g) f ] |
73 | 139 Lemma9 {a} {b} {c} {d} h g f = |
24 | 140 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
|
141 join K h (join K g f) |
30 | 142 ≈⟨⟩ |
72
cbc30519e961
stack overflow solved by moving implicit parameters to module parameters
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
71
diff
changeset
|
143 join K h ( ( TMap μ c o ( FMap T g o f ) ) ) |
28 | 144 ≈⟨ refl-hom ⟩ |
30 | 145 ( TMap μ d o ( FMap T h o ( TMap μ c o ( FMap T g o f ) ) ) ) |
28 | 146 ≈⟨ cdr ( cdr ( assoc )) ⟩ |
30 | 147 ( TMap μ d o ( FMap T h o ( ( TMap μ c o FMap T g ) o f ) ) ) |
28 | 148 ≈⟨ assoc ⟩ --- ( f o ( g o h ) ) = ( ( f o g ) o h ) |
30 | 149 ( ( TMap μ d o FMap T h ) o ( (TMap μ c o FMap T g ) o f ) ) |
25 | 150 ≈⟨ assoc ⟩ |
30 | 151 ( ( ( TMap μ d o FMap T h ) o (TMap μ c o FMap T g ) ) o f ) |
28 | 152 ≈⟨ car (sym assoc) ⟩ |
30 | 153 ( ( TMap μ d o ( FMap T h o ( TMap μ c o FMap T g ) ) ) o f ) |
28 | 154 ≈⟨ car ( cdr (assoc) ) ⟩ |
30 | 155 ( ( TMap μ d o ( ( FMap T h o TMap μ c ) o FMap T g ) ) o f ) |
28 | 156 ≈⟨ car assoc ⟩ |
30 | 157 ( ( ( TMap μ d o ( FMap T h o TMap μ c ) ) o FMap T g ) o f ) |
28 | 158 ≈⟨ car (car ( cdr ( begin |
30 | 159 ( FMap T h o TMap μ c ) |
66 | 160 ≈⟨ nat μ ⟩ |
30 | 161 ( TMap μ (FObj T d) o FMap T (FMap T h) ) |
25 | 162 ∎ |
163 ))) ⟩ | |
30 | 164 ( ( ( TMap μ d o ( TMap μ ( FObj T d) o FMap T ( FMap T h ) ) ) o FMap T g ) o f ) |
28 | 165 ≈⟨ car (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 (sym assoc) ) ⟩ |
30 | 168 ( ( TMap μ d o ( TMap μ ( FObj T d) o ( FMap T ( FMap T h ) o FMap T g ) ) ) o f ) |
28 | 169 ≈⟨ car ( cdr (cdr (sym (distr T )))) ⟩ |
30 | 170 ( ( TMap μ d o ( TMap μ ( FObj T d) o FMap T ( ( FMap T h o g ) ) ) ) o f ) |
28 | 171 ≈⟨ car assoc ⟩ |
30 | 172 ( ( ( TMap μ d o TMap μ ( FObj T d) ) o FMap T ( ( FMap T h o g ) ) ) o f ) |
28 | 173 ≈⟨ car ( car ( |
27 | 174 begin |
30 | 175 ( 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
|
176 ≈⟨ IsMonad.assoc ( isMonad M) ⟩ |
30 | 177 ( TMap μ d o FMap T (TMap μ d) ) |
27 | 178 ∎ |
179 )) ⟩ | |
30 | 180 ( ( ( TMap μ d o FMap T ( TMap μ d) ) o FMap T ( ( FMap T h o g ) ) ) o f ) |
28 | 181 ≈⟨ car (sym assoc) ⟩ |
30 | 182 ( ( TMap μ d o ( FMap T ( TMap μ d ) o FMap T ( ( FMap T h o g ) ) ) ) o f ) |
24 | 183 ≈⟨ sym assoc ⟩ |
30 | 184 ( TMap μ d o ( ( FMap T ( TMap μ d ) o FMap T ( ( FMap T h o g ) ) ) o f ) ) |
28 | 185 ≈⟨ cdr ( car ( sym ( distr T ))) ⟩ |
30 | 186 ( TMap μ d o ( FMap T ( ( ( TMap μ d ) o ( FMap T h o g ) ) ) o 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 ( ( TMap μ d o ( FMap T h o g ) ) ) f |
23 | 189 ≈⟨ 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
|
190 join K ( join K h g) f |
24 | 191 ∎ where open ≈-Reasoning (A) |
3 | 192 |
82 | 193 -- |
194 -- o-resp in Kleisli Category ( for Functor definitions ) | |
195 -- | |
74
49e6eb3ef9c0
Kleisli Category constructed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
73
diff
changeset
|
196 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
|
197 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
|
198 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
|
199 begin |
49e6eb3ef9c0
Kleisli Category constructed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
73
diff
changeset
|
200 join K h f |
49e6eb3ef9c0
Kleisli Category constructed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
73
diff
changeset
|
201 ≈⟨⟩ |
49e6eb3ef9c0
Kleisli Category constructed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
73
diff
changeset
|
202 TMap μ c o ( FMap T h o f ) |
49e6eb3ef9c0
Kleisli Category constructed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
73
diff
changeset
|
203 ≈⟨ 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
|
204 TMap μ c o ( FMap T i o g ) |
49e6eb3ef9c0
Kleisli Category constructed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
73
diff
changeset
|
205 ≈⟨⟩ |
49e6eb3ef9c0
Kleisli Category constructed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
73
diff
changeset
|
206 join K i g |
49e6eb3ef9c0
Kleisli Category constructed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
73
diff
changeset
|
207 ∎ |
49e6eb3ef9c0
Kleisli Category constructed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
73
diff
changeset
|
208 |
82 | 209 -- |
210 -- Hom in Kleisli Category | |
211 -- | |
74
49e6eb3ef9c0
Kleisli Category constructed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
73
diff
changeset
|
212 |
87 | 213 |
214 record KleisliHom { c₁ c₂ ℓ : Level} { A : Category c₁ c₂ ℓ } { T : Functor A A } (a : Obj A) (b : Obj A) | |
78 | 215 : Set c₂ where |
70 | 216 field |
217 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
|
218 |
88 | 219 open KleisliHom |
220 KHom = \(a b : Obj A) -> KleisliHom {c₁} {c₂} {ℓ} {A} {T} a b | |
87 | 221 |
72
cbc30519e961
stack overflow solved by moving implicit parameters to module parameters
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
71
diff
changeset
|
222 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
|
223 K-id {a = a} = record { KMap = TMap η a } |
56 | 224 |
69
84a150c980ce
generalized distr and assco1
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
68
diff
changeset
|
225 open import Relation.Binary.Core |
56 | 226 |
74
49e6eb3ef9c0
Kleisli Category constructed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
73
diff
changeset
|
227 _⋍_ : { a : Obj A } { b : Obj A } (f g : KHom a b ) -> Set ℓ |
73 | 228 _⋍_ {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
|
229 |
72
cbc30519e961
stack overflow solved by moving implicit parameters to module parameters
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
71
diff
changeset
|
230 _*_ : { 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
|
231 ( 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
|
232 _*_ {a} {b} {c} g f = record { KMap = join K {a} {b} {c} (KMap g) (KMap f) } |
70 | 233 |
72
cbc30519e961
stack overflow solved by moving implicit parameters to module parameters
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
71
diff
changeset
|
234 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
|
235 isKleisliCategory = record { isEquivalence = isEquivalence |
71
709c1bde54dc
Kleisli category problem written
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
70
diff
changeset
|
236 ; identityL = KidL |
709c1bde54dc
Kleisli category problem written
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
70
diff
changeset
|
237 ; identityR = KidR |
709c1bde54dc
Kleisli category problem written
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
70
diff
changeset
|
238 ; o-resp-≈ = Ko-resp |
709c1bde54dc
Kleisli category problem written
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
70
diff
changeset
|
239 ; associative = Kassoc |
69
84a150c980ce
generalized distr and assco1
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
68
diff
changeset
|
240 } |
84a150c980ce
generalized distr and assco1
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
68
diff
changeset
|
241 where |
73 | 242 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
|
243 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
|
244 IsEquivalence {_} {_} {KHom a b} _⋍_ |
82 | 245 isEquivalence {C} {D} = -- this is the same function as A's equivalence but has different types |
246 record { refl = refl-hom | |
247 ; sym = sym | |
248 ; trans = trans-hom | |
249 } | |
72
cbc30519e961
stack overflow solved by moving implicit parameters to module parameters
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
71
diff
changeset
|
250 KidL : {C D : Obj A} -> {f : KHom C D} → (K-id * f) ⋍ f |
73 | 251 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
|
252 KidR : {C D : Obj A} -> {f : KHom C D} → (f * K-id) ⋍ f |
73 | 253 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
|
254 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
|
255 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
|
256 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
|
257 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
|
258 (f * (g * h)) ⋍ ((f * g) * h) |
73 | 259 Kassoc {_} {_} {_} {_} {f} {g} {h} = Lemma9 (KMap f) (KMap g) (KMap h) |
3 | 260 |
78 | 261 KleisliCategory : Category c₁ c₂ ℓ |
75 | 262 KleisliCategory = |
263 record { Obj = Obj A | |
264 ; Hom = KHom | |
265 ; _o_ = _*_ | |
266 ; _≈_ = _⋍_ | |
267 ; Id = K-id | |
268 ; isCategory = isKleisliCategory | |
269 } | |
56 | 270 |
82 | 271 -- |
272 -- Resolution | |
273 -- T = U_T U_F | |
274 -- nat-ε | |
275 -- nat-η | |
276 -- | |
277 | |
80 | 278 ufmap : {a b : Obj A} (f : KHom a b ) -> Hom A (FObj T a) (FObj T b) |
279 ufmap {a} {b} f = A [ TMap μ (b) o FMap T (KMap f) ] | |
280 | |
75 | 281 U_T : Functor KleisliCategory A |
282 U_T = record { | |
283 FObj = FObj T | |
284 ; FMap = ufmap | |
285 ; isFunctor = record | |
286 { ≈-cong = ≈-cong | |
287 ; identity = identity | |
76 | 288 ; distr = distr1 |
75 | 289 } |
290 } where | |
291 identity : {a : Obj A} → A [ ufmap (K-id {a}) ≈ id1 A (FObj T a) ] | |
292 identity {a} = let open ≈-Reasoning (A) in | |
293 begin | |
294 TMap μ (a) o FMap T (TMap η a) | |
295 ≈⟨ IsMonad.unity2 (isMonad M) ⟩ | |
296 id1 A (FObj T a) | |
297 ∎ | |
298 ≈-cong : {a b : Obj A} {f g : KHom a b} → A [ KMap f ≈ KMap g ] → A [ ufmap f ≈ ufmap g ] | |
299 ≈-cong {a} {b} {f} {g} f≈g = let open ≈-Reasoning (A) in | |
300 begin | |
301 TMap μ (b) o FMap T (KMap f) | |
302 ≈⟨ cdr (fcong T f≈g) ⟩ | |
303 TMap μ (b) o FMap T (KMap g) | |
304 ∎ | |
76 | 305 distr1 : {a b c : Obj A} {f : KHom a b} {g : KHom b c} → A [ ufmap (g * f) ≈ (A [ ufmap g o ufmap f ] )] |
306 distr1 {a} {b} {c} {f} {g} = let open ≈-Reasoning (A) in | |
75 | 307 begin |
308 ufmap (g * f) | |
76 | 309 ≈⟨⟩ |
310 ufmap {a} {c} ( record { KMap = TMap μ (c) o (FMap T (KMap g) o (KMap f)) } ) | |
311 ≈⟨⟩ | |
312 TMap μ (c) o FMap T ( TMap μ (c) o (FMap T (KMap g) o (KMap f))) | |
313 ≈⟨ cdr ( distr T) ⟩ | |
314 TMap μ (c) o (( FMap T ( TMap μ (c)) o FMap T (FMap T (KMap g) o (KMap f)))) | |
315 ≈⟨ assoc ⟩ | |
316 (TMap μ (c) o ( FMap T ( TMap μ (c)))) o FMap T (FMap T (KMap g) o (KMap f)) | |
317 ≈⟨ car (sym (IsMonad.assoc (isMonad M))) ⟩ | |
318 (TMap μ (c) o ( TMap μ (FObj T c))) o FMap T (FMap T (KMap g) o (KMap f)) | |
319 ≈⟨ sym assoc ⟩ | |
320 TMap μ (c) o (( TMap μ (FObj T c)) o FMap T (FMap T (KMap g) o (KMap f))) | |
321 ≈⟨ cdr (cdr (distr T)) ⟩ | |
322 TMap μ (c) o (( TMap μ (FObj T c)) o (FMap T (FMap T (KMap g)) o FMap T (KMap f))) | |
323 ≈⟨ cdr (assoc) ⟩ | |
324 TMap μ (c) o ((( TMap μ (FObj T c)) o (FMap T (FMap T (KMap g)))) o FMap T (KMap f)) | |
325 ≈⟨ sym (cdr (car (nat μ ))) ⟩ | |
326 TMap μ (c) o ((FMap T (KMap g ) o TMap μ (b)) o FMap T (KMap f )) | |
327 ≈⟨ cdr (sym assoc) ⟩ | |
328 TMap μ (c) o (FMap T (KMap g ) o ( TMap μ (b) o FMap T (KMap f ))) | |
329 ≈⟨ assoc ⟩ | |
330 ( TMap μ (c) o FMap T (KMap g ) ) o ( TMap μ (b) o FMap T (KMap f ) ) | |
331 ≈⟨⟩ | |
75 | 332 ufmap g o ufmap f |
333 ∎ | |
334 | |
335 | |
336 ffmap : {a b : Obj A} (f : Hom A a b) -> KHom a b | |
337 ffmap f = record { KMap = A [ TMap η (Category.cod A f) o f ] } | |
338 | |
339 F_T : Functor A KleisliCategory | |
340 F_T = record { | |
341 FObj = \a -> a | |
342 ; FMap = ffmap | |
343 ; isFunctor = record | |
344 { ≈-cong = ≈-cong | |
345 ; identity = identity | |
76 | 346 ; distr = distr1 |
75 | 347 } |
348 } where | |
349 identity : {a : Obj A} → A [ A [ TMap η a o id1 A a ] ≈ TMap η a ] | |
350 identity {a} = IsCategory.identityR ( Category.isCategory A) | |
82 | 351 -- Category.cod A f and Category.cod A g are actualy the same b, so we don't need cong-≈, just refl |
75 | 352 lemma1 : {a b : Obj A} {f g : Hom A a b} → A [ f ≈ g ] → A [ TMap η b ≈ TMap η b ] |
353 lemma1 f≈g = IsEquivalence.refl (IsCategory.isEquivalence ( Category.isCategory A )) | |
354 ≈-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 ] ] | |
355 ≈-cong f≈g = (IsCategory.o-resp-≈ (Category.isCategory A)) f≈g ( lemma1 f≈g ) | |
76 | 356 distr1 : {a b c : Obj A} {f : Hom A a b} {g : Hom A b c} → |
75 | 357 ( ffmap (A [ g o f ]) ⋍ ( ffmap g * ffmap f ) ) |
77 | 358 distr1 {a} {b} {c} {f} {g} = let open ≈-Reasoning (A) in |
75 | 359 begin |
360 KMap (ffmap (A [ g o f ])) | |
77 | 361 ≈⟨⟩ |
362 TMap η (c) o (g o f) | |
363 ≈⟨ assoc ⟩ | |
364 (TMap η (c) o g) o f | |
365 ≈⟨ car (sym (nat η)) ⟩ | |
366 (FMap T g o TMap η (b)) o f | |
367 ≈⟨ sym idL ⟩ | |
368 id1 A (FObj T c) o ((FMap T g o TMap η (b)) o f) | |
369 ≈⟨ sym (car (IsMonad.unity2 (isMonad M))) ⟩ | |
370 (TMap μ c o FMap T (TMap η c)) o ((FMap T g o TMap η (b)) o f) | |
371 ≈⟨ sym assoc ⟩ | |
372 TMap μ c o ( FMap T (TMap η c) o ((FMap T g o TMap η (b)) o f) ) | |
373 ≈⟨ cdr (cdr (sym assoc)) ⟩ | |
374 TMap μ c o ( FMap T (TMap η c) o (FMap T g o (TMap η (b) o f))) | |
375 ≈⟨ cdr assoc ⟩ | |
376 TMap μ c o ( ( FMap T (TMap η c) o FMap T g ) o (TMap η (b) o f) ) | |
377 ≈⟨ sym (cdr ( car ( distr T ))) ⟩ | |
378 TMap μ c o ( ( FMap T (TMap η c o g)) o (TMap η (b) o f)) | |
379 ≈⟨ assoc ⟩ | |
380 (TMap μ c o ( FMap T (TMap η c o g))) o (TMap η (b) o f) | |
381 ≈⟨ assoc ⟩ | |
382 ((TMap μ c o (FMap T (TMap η c o g))) o TMap η b) o f | |
383 ≈⟨ sym assoc ⟩ | |
384 (TMap μ c o (FMap T (TMap η c o g))) o (TMap η b o f) | |
385 ≈⟨ sym assoc ⟩ | |
386 TMap μ c o ( (FMap T (TMap η c o g)) o (TMap η b o f) ) | |
387 ≈⟨⟩ | |
388 join K (TMap η c o g) (TMap η b o f) | |
389 ≈⟨⟩ | |
75 | 390 KMap ( ffmap g * ffmap f ) |
391 ∎ | |
392 | |
82 | 393 -- |
394 -- T = (U_T ○ F_T) | |
395 -- | |
396 | |
79 | 397 Lemma11-1 : ∀{a b : Obj A} -> (f : Hom A a b ) -> A [ FMap T f ≈ FMap (U_T ○ F_T) f ] |
398 Lemma11-1 {a} {b} f = let open ≈-Reasoning (A) in | |
399 sym ( begin | |
400 FMap (U_T ○ F_T) f | |
401 ≈⟨⟩ | |
402 FMap U_T ( FMap F_T f ) | |
403 ≈⟨⟩ | |
404 TMap μ (b) o FMap T (KMap ( ffmap f ) ) | |
405 ≈⟨⟩ | |
406 TMap μ (b) o FMap T (TMap η (b) o f) | |
407 ≈⟨ cdr (distr T ) ⟩ | |
408 TMap μ (b) o ( FMap T (TMap η (b)) o FMap T f) | |
409 ≈⟨ assoc ⟩ | |
410 (TMap μ (b) o FMap T (TMap η (b))) o FMap T f | |
411 ≈⟨ car (IsMonad.unity2 (isMonad M)) ⟩ | |
412 id1 A (FObj T b) o FMap T f | |
413 ≈⟨ idL ⟩ | |
414 FMap T f | |
415 ∎ ) | |
416 | |
82 | 417 -- construct ≃ |
418 | |
81
0404b2ba7db6
Resolution Adjoint proved.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
80
diff
changeset
|
419 Lemma11 : T ≃ (U_T ○ F_T) |
0404b2ba7db6
Resolution Adjoint proved.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
80
diff
changeset
|
420 Lemma11 f = Category.Cat.refl (Lemma11-1 f) |
78 | 421 |
82 | 422 -- |
423 -- natural transformations | |
424 -- | |
425 | |
78 | 426 nat-η : NTrans A A identityFunctor ( U_T ○ F_T ) |
427 nat-η = record { TMap = \x -> TMap η x ; isNTrans = isNTrans1 } where | |
79 | 428 naturality1 : {a b : Obj A} {f : Hom A a b} |
429 → A [ A [ ( FMap ( U_T ○ F_T ) f ) o ( TMap η a ) ] ≈ A [ (TMap η b ) o f ] ] | |
430 naturality1 {a} {b} {f} = let open ≈-Reasoning (A) in | |
431 begin | |
432 ( FMap ( U_T ○ F_T ) f ) o ( TMap η a ) | |
84 | 433 ≈⟨ sym (resp refl-hom (Lemma11-1 f)) ⟩ |
434 FMap T f o TMap η a | |
79 | 435 ≈⟨ nat η ⟩ |
84 | 436 TMap η b o f |
79 | 437 ∎ |
78 | 438 isNTrans1 : IsNTrans A A identityFunctor ( U_T ○ F_T ) (\a -> TMap η a) |
79 | 439 isNTrans1 = record { naturality = naturality1 } |
77 | 440 |
79 | 441 tmap-ε : (a : Obj A) -> KHom (FObj T a) a |
78 | 442 tmap-ε a = record { KMap = id1 A (FObj T a) } |
443 | |
444 nat-ε : NTrans KleisliCategory KleisliCategory ( F_T ○ U_T ) identityFunctor | |
445 nat-ε = record { TMap = \a -> tmap-ε a; isNTrans = isNTrans1 } where | |
79 | 446 naturality1 : {a b : Obj A} {f : KHom a b} |
78 | 447 → (f * ( tmap-ε a ) ) ⋍ (( tmap-ε b ) * ( FMap (F_T ○ U_T) f ) ) |
79 | 448 naturality1 {a} {b} {f} = let open ≈-Reasoning (A) in |
449 sym ( begin | |
450 KMap (( tmap-ε b ) * ( FMap (F_T ○ U_T) f )) | |
80 | 451 ≈⟨⟩ |
452 TMap μ b o ( FMap T ( id1 A (FObj T b) ) o ( KMap (FMap (F_T ○ U_T) f ) )) | |
453 ≈⟨ cdr ( cdr ( | |
454 begin | |
455 KMap (FMap (F_T ○ U_T) f ) | |
456 ≈⟨⟩ | |
457 KMap (FMap F_T (FMap U_T f)) | |
458 ≈⟨⟩ | |
459 TMap η (FObj T b) o (TMap μ (b) o FMap T (KMap f)) | |
460 ∎ | |
461 )) ⟩ | |
462 TMap μ b o ( FMap T ( id1 A (FObj T b) ) o (TMap η (FObj T b) o (TMap μ (b) o FMap T (KMap f)))) | |
463 ≈⟨ cdr (car (IsFunctor.identity (isFunctor T))) ⟩ | |
464 TMap μ b o ( id1 A (FObj T (FObj T b) ) o (TMap η (FObj T b) o (TMap μ (b) o FMap T (KMap f)))) | |
465 ≈⟨ cdr idL ⟩ | |
466 TMap μ b o (TMap η (FObj T b) o (TMap μ (b) o FMap T (KMap f))) | |
467 ≈⟨ assoc ⟩ | |
468 (TMap μ b o (TMap η (FObj T b))) o (TMap μ (b) o FMap T (KMap f)) | |
469 ≈⟨ (car (IsMonad.unity1 (isMonad M))) ⟩ | |
470 id1 A (FObj T b) o (TMap μ (b) o FMap T (KMap f)) | |
471 ≈⟨ idL ⟩ | |
472 TMap μ b o FMap T (KMap f) | |
473 ≈⟨ cdr (sym idR) ⟩ | |
474 TMap μ b o ( FMap T (KMap f) o id1 A (FObj T a) ) | |
475 ≈⟨⟩ | |
79 | 476 KMap (f * ( tmap-ε a )) |
477 ∎ ) | |
78 | 478 isNTrans1 : IsNTrans KleisliCategory KleisliCategory ( F_T ○ U_T ) identityFunctor (\a -> tmap-ε a ) |
79 | 479 isNTrans1 = record { naturality = naturality1 } |
77 | 480 |
82 | 481 -- |
482 -- μ = U_T ε U_F | |
483 -- | |
95 | 484 tmap-μ : (a : Obj A) -> Hom A (FObj ( U_T ○ F_T ) (FObj ( U_T ○ F_T ) a)) (FObj ( U_T ○ F_T ) a) |
485 tmap-μ a = FMap U_T ( TMap nat-ε ( FObj F_T a )) | |
486 | |
487 nat-μ : NTrans A A (( U_T ○ F_T ) ○ ( U_T ○ F_T )) ( U_T ○ F_T ) | |
488 nat-μ = record { TMap = tmap-μ ; isNTrans = isNTrans1 } where | |
489 naturality1 : {a b : Obj A} {f : Hom A a b} | |
490 → 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) ] ] | |
491 naturality1 {a} {b} {f} = let open ≈-Reasoning (A) in | |
492 sym ( begin | |
493 ( tmap-μ b ) o FMap (U_T ○ F_T) ( FMap (U_T ○ F_T) f) | |
494 ≈⟨⟩ | |
495 ( FMap U_T ( TMap nat-ε ( FObj F_T b )) ) o FMap (U_T ○ F_T) ( FMap (U_T ○ F_T) f) | |
496 ≈⟨ sym ( distr U_T) ⟩ | |
497 FMap U_T ( KleisliCategory [ TMap nat-ε ( FObj F_T b ) o FMap F_T ( FMap (U_T ○ F_T) f) ] ) | |
498 ≈⟨ fcong U_T (sym (nat nat-ε)) ⟩ | |
499 FMap U_T ( KleisliCategory [ (FMap F_T f) o TMap nat-ε ( FObj F_T a ) ] ) | |
500 ≈⟨ distr U_T ⟩ | |
501 (FMap U_T (FMap F_T f)) o FMap U_T ( TMap nat-ε ( FObj F_T a )) | |
502 ≈⟨⟩ | |
503 (FMap (U_T ○ F_T) f) o ( tmap-μ a) | |
504 ∎ ) | |
505 isNTrans1 : IsNTrans A A (( U_T ○ F_T ) ○ ( U_T ○ F_T )) ( U_T ○ F_T ) tmap-μ | |
506 isNTrans1 = record { naturality = naturality1 } | |
507 | |
508 Lemma12 : {x : Obj A } -> A [ TMap nat-μ x ≈ FMap U_T ( TMap nat-ε ( FObj F_T x ) ) ] | |
80 | 509 Lemma12 {x} = let open ≈-Reasoning (A) in |
510 sym ( begin | |
511 FMap U_T ( TMap nat-ε ( FObj F_T x ) ) | |
512 ≈⟨⟩ | |
95 | 513 tmap-μ x |
514 ≈⟨⟩ | |
515 TMap nat-μ x | |
516 ∎ ) | |
517 | |
518 Lemma13 : {x : Obj A } -> A [ TMap μ x ≈ FMap U_T ( TMap nat-ε ( FObj F_T x ) ) ] | |
519 Lemma13 {x} = let open ≈-Reasoning (A) in | |
520 sym ( begin | |
521 FMap U_T ( TMap nat-ε ( FObj F_T x ) ) | |
522 ≈⟨⟩ | |
80 | 523 TMap μ x o FMap T (id1 A (FObj T x) ) |
524 ≈⟨ cdr (IsFunctor.identity (isFunctor T)) ⟩ | |
525 TMap μ x o id1 A (FObj T (FObj T x) ) | |
526 ≈⟨ idR ⟩ | |
527 TMap μ x | |
528 ∎ ) | |
78 | 529 |
84 | 530 Adj_T : Adjunction A KleisliCategory U_T F_T nat-η nat-ε |
531 Adj_T = record { | |
80 | 532 isAdjunction = record { |
533 adjoint1 = adjoint1 ; | |
534 adjoint2 = adjoint2 | |
535 } | |
536 } where | |
537 adjoint1 : { b : Obj KleisliCategory } → | |
538 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
|
539 adjoint1 {b} = let open ≈-Reasoning (A) in |
0404b2ba7db6
Resolution Adjoint proved.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
80
diff
changeset
|
540 begin |
0404b2ba7db6
Resolution Adjoint proved.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
80
diff
changeset
|
541 ( 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
|
542 ≈⟨⟩ |
0404b2ba7db6
Resolution Adjoint proved.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
80
diff
changeset
|
543 (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
|
544 ≈⟨ car ( cdr (IsFunctor.identity (isFunctor T))) ⟩ |
0404b2ba7db6
Resolution Adjoint proved.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
80
diff
changeset
|
545 (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
|
546 ≈⟨ car idR ⟩ |
0404b2ba7db6
Resolution Adjoint proved.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
80
diff
changeset
|
547 TMap μ (b) o ( TMap η ( FObj T b )) |
0404b2ba7db6
Resolution Adjoint proved.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
80
diff
changeset
|
548 ≈⟨ IsMonad.unity1 (isMonad M) ⟩ |
0404b2ba7db6
Resolution Adjoint proved.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
80
diff
changeset
|
549 id1 A (FObj U_T b) |
0404b2ba7db6
Resolution Adjoint proved.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
80
diff
changeset
|
550 ∎ |
80 | 551 adjoint2 : {a : Obj A} → |
552 KleisliCategory [ KleisliCategory [ ( TMap nat-ε ( FObj F_T a )) o ( FMap F_T ( TMap nat-η a )) ] | |
87 | 553 ≈ id1 KleisliCategory (FObj F_T a) ] |
81
0404b2ba7db6
Resolution Adjoint proved.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
80
diff
changeset
|
554 adjoint2 {a} = let open ≈-Reasoning (A) in |
0404b2ba7db6
Resolution Adjoint proved.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
80
diff
changeset
|
555 begin |
0404b2ba7db6
Resolution Adjoint proved.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
80
diff
changeset
|
556 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
|
557 ≈⟨⟩ |
0404b2ba7db6
Resolution Adjoint proved.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
80
diff
changeset
|
558 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
|
559 ≈⟨ cdr ( car ( IsFunctor.identity (isFunctor T))) ⟩ |
0404b2ba7db6
Resolution Adjoint proved.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
80
diff
changeset
|
560 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
|
561 ≈⟨ cdr ( idL ) ⟩ |
0404b2ba7db6
Resolution Adjoint proved.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
80
diff
changeset
|
562 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
|
563 ≈⟨ assoc ⟩ |
0404b2ba7db6
Resolution Adjoint proved.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
80
diff
changeset
|
564 (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
|
565 ≈⟨ car (IsMonad.unity1 (isMonad M)) ⟩ |
0404b2ba7db6
Resolution Adjoint proved.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
80
diff
changeset
|
566 id1 A (FObj T a) o (TMap η a) |
0404b2ba7db6
Resolution Adjoint proved.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
80
diff
changeset
|
567 ≈⟨ idL ⟩ |
0404b2ba7db6
Resolution Adjoint proved.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
80
diff
changeset
|
568 TMap η a |
0404b2ba7db6
Resolution Adjoint proved.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
80
diff
changeset
|
569 ≈⟨⟩ |
0404b2ba7db6
Resolution Adjoint proved.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
80
diff
changeset
|
570 TMap η (FObj F_T a) |
0404b2ba7db6
Resolution Adjoint proved.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
80
diff
changeset
|
571 ≈⟨⟩ |
0404b2ba7db6
Resolution Adjoint proved.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
80
diff
changeset
|
572 KMap (id1 KleisliCategory (FObj F_T a)) |
82 | 573 ∎ |
77 | 574 |
87 | 575 open MResolution |
84 | 576 |
95 | 577 Resolution_T : MResolution A KleisliCategory T U_T F_T {nat-η} {nat-ε} {nat-μ} Adj_T |
84 | 578 Resolution_T = record { |
87 | 579 T=UF = Lemma11; |
580 μ=UεF = Lemma12 | |
84 | 581 } |
582 | |
75 | 583 |
87 | 584 module comparison-functor {c₁' c₂' ℓ' : Level} ( B : Category c₁' c₂' ℓ' ) |
83 | 585 { U_K : Functor B A } { F_K : Functor A B } |
586 { η_K : NTrans A A identityFunctor ( U_K ○ F_K ) } | |
587 { ε_K : NTrans B B ( F_K ○ U_K ) identityFunctor } | |
85 | 588 { μ_K : NTrans A A (( U_K ○ F_K ) ○ ( U_K ○ F_K )) ( U_K ○ F_K ) } |
87 | 589 ( K : Monad A (U_K ○ F_K) η_K μ_K ) |
85 | 590 ( AdjK : Adjunction A B U_K F_K η_K ε_K ) |
94
4fa718e4fd77
Comparison Functor constructed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
93
diff
changeset
|
591 ( RK : MResolution A B T U_K F_K {η_K} {ε_K} {μ_K} AdjK ) |
83 | 592 where |
89 | 593 open Category.Cat.[_]_~_ |
75 | 594 |
89 | 595 ≃-sym : {c₁ c₂ ℓ : Level} { C : Category c₁ c₂ ℓ } {c₁' c₂' ℓ' : Level} { D : Category c₁' c₂' ℓ' } |
596 {F G : Functor C D} → F ≃ G → G ≃ F | |
94
4fa718e4fd77
Comparison Functor constructed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
93
diff
changeset
|
597 ≃-sym {_} {_} {_} {C} {_} {_} {_} {D} {F} {G} F≃G f = helper (F≃G f) |
89 | 598 where |
599 helper : ∀{a b c d} {f : Hom D a b} {g : Hom D c d} → [ D ] f ~ g → [ D ] g ~ f | |
600 helper (Category.Cat.refl Ff≈Gf) = | |
601 Category.Cat.refl {C = D} (IsEquivalence.sym (IsCategory.isEquivalence (Category.isCategory D)) Ff≈Gf) | |
602 | |
94
4fa718e4fd77
Comparison Functor constructed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
93
diff
changeset
|
603 -- to T=UF constraints happy |
4fa718e4fd77
Comparison Functor constructed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
93
diff
changeset
|
604 hoge : {c₁ c₂ ℓ : Level} { C : Category c₁ c₂ ℓ } {c₁' c₂' ℓ' : Level} { D : Category c₁' c₂' ℓ' } |
4fa718e4fd77
Comparison Functor constructed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
93
diff
changeset
|
605 {F G : Functor C D} → F ≃ G → F ≃ G |
4fa718e4fd77
Comparison Functor constructed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
93
diff
changeset
|
606 hoge {_} {_} {_} {C} {_} {_} {_} {D} {F} {G} F≃G f = helper (F≃G f) |
4fa718e4fd77
Comparison Functor constructed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
93
diff
changeset
|
607 where |
4fa718e4fd77
Comparison Functor constructed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
93
diff
changeset
|
608 helper : ∀{a b c d} {f : Hom D a b} {g : Hom D c d} → [ D ] f ~ g → [ D ] f ~ g |
4fa718e4fd77
Comparison Functor constructed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
93
diff
changeset
|
609 helper (Category.Cat.refl Ff≈Gf) = Category.Cat.refl Ff≈Gf |
4fa718e4fd77
Comparison Functor constructed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
93
diff
changeset
|
610 |
87 | 611 RHom = \(a b : Obj A) -> KleisliHom {c₁} {c₂} {ℓ} {A} { U_K ○ F_K } a b |
96 | 612 TtoK : (a b : Obj A) -> (KHom a b) -> {g h : Hom A (FObj T b) (FObj ( U_K ○ F_K) b) } -> |
94
4fa718e4fd77
Comparison Functor constructed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
93
diff
changeset
|
613 ([ A ] g ~ h) -> Hom A a (FObj ( U_K ○ F_K ) b) |
96 | 614 TtoK _ _ f {g} (Category.Cat.refl _) = A [ g o (KMap f) ] |
88 | 615 RMap : {a b : Obj A} -> (f : KHom a b) -> Hom A a (FObj ( U_K ○ F_K ) b) |
96 | 616 RMap {a} {b} f = TtoK a b f {_} {_} ((hoge (T=UF RK)) (id1 A b)) |
89 | 617 |
96 | 618 KtoT : (a b : Obj A) -> (RHom a b) -> {g h : Hom A (FObj ( U_K ○ F_K ) b) (FObj T b) } -> |
94
4fa718e4fd77
Comparison Functor constructed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
93
diff
changeset
|
619 ([ A ] g ~ h) -> Hom A a (FObj T b) |
96 | 620 KtoT _ _ f {g} {h} (Category.Cat.refl eq) = A [ g o (KMap f) ] |
89 | 621 RKMap : {a b : Obj A} -> (f : RHom a b) -> Hom A a (FObj T b) |
96 | 622 RKMap {a} {b} f = KtoT a b f {_} {_} (( ≃-sym (T=UF RK)) (id1 A b)) |
88 | 623 |
93 | 624 RMap-cong : {a b : Obj A} {f g : KHom a b} -> A [ KMap f ≈ KMap g ] -> A [ RMap f ≈ RMap g ] |
94
4fa718e4fd77
Comparison Functor constructed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
93
diff
changeset
|
625 RMap-cong {a} {b} {f} {g} eq = helper a b f g eq ((hoge (T=UF RK))( id1 A b )) |
93 | 626 where |
627 open ≈-Reasoning (A) | |
628 helper : (a b : Obj A) (f g : KHom a b) -> A [ KMap f ≈ KMap g ] -> | |
629 {conv : Hom A (FObj T b) (FObj ( U_K ○ F_K ) b) } -> ([ A ] conv ~ conv) -> A [ RMap f ≈ RMap g ] | |
94
4fa718e4fd77
Comparison Functor constructed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
93
diff
changeset
|
630 helper _ _ _ _ eq (Category.Cat.refl _) = |
4fa718e4fd77
Comparison Functor constructed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
93
diff
changeset
|
631 (Category.IsCategory.o-resp-≈ (Category.isCategory A)) eq refl-hom |
93 | 632 |
88 | 633 kfmap : {a b : Obj A} (f : KHom a b) -> Hom B (FObj F_K a) (FObj F_K b) |
634 kfmap {_} {b} f = B [ TMap ε_K (FObj F_K b) o FMap F_K (RMap f) ] | |
75 | 635 |
92 | 636 open Adjunction |
83 | 637 K_T : Functor KleisliCategory B |
638 K_T = record { | |
639 FObj = FObj F_K | |
88 | 640 ; FMap = kfmap |
83 | 641 ; isFunctor = record |
92 | 642 { ≈-cong = ≈-cong |
643 ; identity = identity | |
93 | 644 ; distr = distr1 |
83 | 645 } |
92 | 646 } where |
647 identity : {a : Obj A} → B [ kfmap (K-id {a}) ≈ id1 B (FObj F_K a) ] | |
648 identity {a} = let open ≈-Reasoning (B) in | |
649 begin | |
650 kfmap (K-id {a}) | |
651 ≈⟨⟩ | |
652 TMap ε_K (FObj F_K a) o FMap F_K (RMap (K-id {a})) | |
653 ≈⟨⟩ | |
654 TMap ε_K (FObj F_K a) o FMap F_K (TMap η_K a) | |
655 ≈⟨ IsAdjunction.adjoint2 (isAdjunction AdjK) ⟩ | |
656 id1 B (FObj F_K a) | |
657 ∎ | |
658 ≈-cong : {a b : Obj A} -> {f g : KHom a b} → A [ KMap f ≈ KMap g ] → B [ kfmap f ≈ kfmap g ] | |
93 | 659 ≈-cong {a} {b} {f} {g} f≈g = let open ≈-Reasoning (B) in |
660 begin | |
661 kfmap f | |
662 ≈⟨⟩ | |
663 TMap ε_K (FObj F_K b) o FMap F_K (RMap f) | |
664 ≈⟨ cdr ( fcong F_K (RMap-cong f≈g)) ⟩ | |
665 TMap ε_K (FObj F_K b) o FMap F_K (RMap g) | |
666 ≈⟨⟩ | |
667 kfmap g | |
668 ∎ | |
669 distr1 : {a b c : Obj A} {f : KHom a b} {g : KHom b c} → B [ kfmap (g * f) ≈ (B [ kfmap g o kfmap f ] )] | |
670 distr1 {a} {b} {c} {f} {g} = let open ≈-Reasoning (B) in | |
671 begin | |
672 kfmap (g * f) | |
673 ≈⟨⟩ | |
674 TMap ε_K (FObj F_K c) o FMap F_K (RMap (g * f)) | |
675 ≈⟨⟩ | |
94
4fa718e4fd77
Comparison Functor constructed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
93
diff
changeset
|
676 TMap ε_K (FObj F_K c) o FMap F_K (A [ TMap μ_K c o A [ FMap ( U_K ○ F_K ) (RMap g) o RMap f ] ] ) |
4fa718e4fd77
Comparison Functor constructed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
93
diff
changeset
|
677 ≈⟨ cdr ( distr F_K ) ⟩ |
4fa718e4fd77
Comparison Functor constructed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
93
diff
changeset
|
678 TMap ε_K (FObj F_K c) o ( FMap F_K (TMap μ_K c) o ( FMap F_K (A [ FMap ( U_K ○ F_K ) (RMap g) o RMap f ]))) |
4fa718e4fd77
Comparison Functor constructed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
93
diff
changeset
|
679 ≈⟨ cdr (cdr ( distr F_K )) ⟩ |
4fa718e4fd77
Comparison Functor constructed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
93
diff
changeset
|
680 TMap ε_K (FObj F_K c) o ( FMap F_K (TMap μ_K c) o (( FMap F_K (FMap ( U_K ○ F_K ) (RMap g))) o (FMap F_K (RMap f)))) |
4fa718e4fd77
Comparison Functor constructed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
93
diff
changeset
|
681 ≈⟨ cdr assoc ⟩ |
4fa718e4fd77
Comparison Functor constructed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
93
diff
changeset
|
682 TMap ε_K (FObj F_K c) o ((( FMap F_K (TMap μ_K c) o ( FMap F_K (FMap (U_K ○ F_K) (RMap g))))) o (FMap F_K (RMap f))) |
4fa718e4fd77
Comparison Functor constructed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
93
diff
changeset
|
683 ≈⟨ cdr (car (car ( fcong F_K ( μ=UεF RK )))) ⟩ |
4fa718e4fd77
Comparison Functor constructed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
93
diff
changeset
|
684 TMap ε_K (FObj F_K c) o (( FMap F_K ( FMap U_K ( TMap ε_K ( FObj F_K c ) )) o |
4fa718e4fd77
Comparison Functor constructed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
93
diff
changeset
|
685 ( FMap F_K (FMap (U_K ○ F_K) (RMap g)))) o (FMap F_K (RMap f))) |
4fa718e4fd77
Comparison Functor constructed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
93
diff
changeset
|
686 ≈⟨ sym (cdr assoc) ⟩ |
4fa718e4fd77
Comparison Functor constructed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
93
diff
changeset
|
687 TMap ε_K (FObj F_K c) o (( FMap F_K ( FMap U_K ( TMap ε_K ( FObj F_K c ) ))) o |
4fa718e4fd77
Comparison Functor constructed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
93
diff
changeset
|
688 (( FMap F_K (FMap (U_K ○ F_K) (RMap g))) o (FMap F_K (RMap f)))) |
4fa718e4fd77
Comparison Functor constructed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
93
diff
changeset
|
689 ≈⟨ assoc ⟩ |
4fa718e4fd77
Comparison Functor constructed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
93
diff
changeset
|
690 (TMap ε_K (FObj F_K c) o ( FMap F_K ( FMap U_K ( TMap ε_K ( FObj F_K c ) )))) o |
4fa718e4fd77
Comparison Functor constructed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
93
diff
changeset
|
691 (( FMap F_K (FMap (U_K ○ F_K) (RMap g))) o (FMap F_K (RMap f))) |
4fa718e4fd77
Comparison Functor constructed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
93
diff
changeset
|
692 ≈⟨ car (sym (nat ε_K)) ⟩ |
4fa718e4fd77
Comparison Functor constructed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
93
diff
changeset
|
693 (TMap ε_K (FObj F_K c) o ( TMap ε_K (FObj (F_K ○ U_K) (FObj F_K c)))) o |
4fa718e4fd77
Comparison Functor constructed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
93
diff
changeset
|
694 (( FMap F_K (FMap (U_K ○ F_K) (RMap g))) o (FMap F_K (RMap f))) |
4fa718e4fd77
Comparison Functor constructed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
93
diff
changeset
|
695 ≈⟨ sym assoc ⟩ |
4fa718e4fd77
Comparison Functor constructed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
93
diff
changeset
|
696 TMap ε_K (FObj F_K c) o (( TMap ε_K (FObj (F_K ○ U_K) (FObj F_K c))) o |
4fa718e4fd77
Comparison Functor constructed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
93
diff
changeset
|
697 ((( FMap F_K (FMap (U_K ○ F_K) (RMap g)))) o (FMap F_K (RMap f)))) |
4fa718e4fd77
Comparison Functor constructed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
93
diff
changeset
|
698 ≈⟨ cdr assoc ⟩ |
4fa718e4fd77
Comparison Functor constructed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
93
diff
changeset
|
699 TMap ε_K (FObj F_K c) o ((( TMap ε_K (FObj (F_K ○ U_K) (FObj F_K c))) o |
4fa718e4fd77
Comparison Functor constructed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
93
diff
changeset
|
700 (( FMap F_K (FMap (U_K ○ F_K) (RMap g))))) o (FMap F_K (RMap f))) |
4fa718e4fd77
Comparison Functor constructed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
93
diff
changeset
|
701 ≈⟨ cdr ( car ( |
4fa718e4fd77
Comparison Functor constructed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
93
diff
changeset
|
702 begin |
4fa718e4fd77
Comparison Functor constructed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
93
diff
changeset
|
703 TMap ε_K (FObj (F_K ○ U_K) (FObj F_K c)) o ((FMap F_K (FMap (U_K ○ F_K) (RMap g)))) |
4fa718e4fd77
Comparison Functor constructed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
93
diff
changeset
|
704 ≈⟨⟩ |
4fa718e4fd77
Comparison Functor constructed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
93
diff
changeset
|
705 TMap ε_K (FObj (F_K ○ U_K) (FObj F_K c)) o (FMap (F_K ○ U_K) (FMap F_K (RMap g))) |
4fa718e4fd77
Comparison Functor constructed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
93
diff
changeset
|
706 ≈⟨ sym (nat ε_K) ⟩ |
4fa718e4fd77
Comparison Functor constructed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
93
diff
changeset
|
707 ( FMap F_K (RMap g)) o (TMap ε_K (FObj F_K b)) |
4fa718e4fd77
Comparison Functor constructed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
93
diff
changeset
|
708 ∎ |
4fa718e4fd77
Comparison Functor constructed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
93
diff
changeset
|
709 )) ⟩ |
4fa718e4fd77
Comparison Functor constructed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
93
diff
changeset
|
710 TMap ε_K (FObj F_K c) o ((( FMap F_K (RMap g)) o (TMap ε_K (FObj F_K b))) o FMap F_K (RMap f)) |
4fa718e4fd77
Comparison Functor constructed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
93
diff
changeset
|
711 ≈⟨ cdr (sym assoc) ⟩ |
4fa718e4fd77
Comparison Functor constructed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
93
diff
changeset
|
712 TMap ε_K (FObj F_K c) o (( FMap F_K (RMap g)) o (TMap ε_K (FObj F_K b) o FMap F_K (RMap f))) |
4fa718e4fd77
Comparison Functor constructed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
93
diff
changeset
|
713 ≈⟨ assoc ⟩ |
4fa718e4fd77
Comparison Functor constructed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
93
diff
changeset
|
714 (TMap ε_K (FObj F_K c) o FMap F_K (RMap g)) o (TMap ε_K (FObj F_K b) o FMap F_K (RMap f)) |
4fa718e4fd77
Comparison Functor constructed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
93
diff
changeset
|
715 ≈⟨⟩ |
93 | 716 kfmap g o kfmap f |
717 ∎ | |
75 | 718 |