Mercurial > hg > Members > kono > Proof > category
annotate nat.agda @ 84:ee25f96ee8cc
record Resolution
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Sat, 27 Jul 2013 17:32:32 +0900 |
| parents | c3846bf83717 |
| children | 31e1dbbf8800 |
| 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 |
|
72
cbc30519e961
stack overflow solved by moving implicit parameters to module parameters
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
71
diff
changeset
|
213 record KHom (a : Obj A) (b : Obj A) |
| 78 | 214 : Set c₂ where |
| 70 | 215 field |
| 216 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
|
217 |
|
72
cbc30519e961
stack overflow solved by moving implicit parameters to module parameters
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
71
diff
changeset
|
218 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
|
219 K-id {a = a} = record { KMap = TMap η a } |
| 56 | 220 |
|
69
84a150c980ce
generalized distr and assco1
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
68
diff
changeset
|
221 open import Relation.Binary.Core |
| 73 | 222 open KHom |
| 56 | 223 |
|
74
49e6eb3ef9c0
Kleisli Category constructed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
73
diff
changeset
|
224 _⋍_ : { a : Obj A } { b : Obj A } (f g : KHom a b ) -> Set ℓ |
| 73 | 225 _⋍_ {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
|
226 |
|
72
cbc30519e961
stack overflow solved by moving implicit parameters to module parameters
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
71
diff
changeset
|
227 _*_ : { 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
|
228 ( 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
|
229 _*_ {a} {b} {c} g f = record { KMap = join K {a} {b} {c} (KMap g) (KMap f) } |
| 70 | 230 |
|
72
cbc30519e961
stack overflow solved by moving implicit parameters to module parameters
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
71
diff
changeset
|
231 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
|
232 isKleisliCategory = record { isEquivalence = isEquivalence |
|
71
709c1bde54dc
Kleisli category problem written
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
70
diff
changeset
|
233 ; identityL = KidL |
|
709c1bde54dc
Kleisli category problem written
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
70
diff
changeset
|
234 ; identityR = KidR |
|
709c1bde54dc
Kleisli category problem written
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
70
diff
changeset
|
235 ; o-resp-≈ = Ko-resp |
|
709c1bde54dc
Kleisli category problem written
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
70
diff
changeset
|
236 ; associative = Kassoc |
|
69
84a150c980ce
generalized distr and assco1
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
68
diff
changeset
|
237 } |
|
84a150c980ce
generalized distr and assco1
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
68
diff
changeset
|
238 where |
| 73 | 239 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
|
240 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
|
241 IsEquivalence {_} {_} {KHom a b} _⋍_ |
| 82 | 242 isEquivalence {C} {D} = -- this is the same function as A's equivalence but has different types |
| 243 record { refl = refl-hom | |
| 244 ; sym = sym | |
| 245 ; trans = trans-hom | |
| 246 } | |
|
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 KidL : {C D : Obj A} -> {f : KHom C D} → (K-id * f) ⋍ f |
| 73 | 248 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
|
249 KidR : {C D : Obj A} -> {f : KHom C D} → (f * K-id) ⋍ f |
| 73 | 250 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
|
251 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
|
252 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
|
253 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
|
254 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
|
255 (f * (g * h)) ⋍ ((f * g) * h) |
| 73 | 256 Kassoc {_} {_} {_} {_} {f} {g} {h} = Lemma9 (KMap f) (KMap g) (KMap h) |
| 3 | 257 |
| 78 | 258 KleisliCategory : Category c₁ c₂ ℓ |
| 75 | 259 KleisliCategory = |
| 260 record { Obj = Obj A | |
| 261 ; Hom = KHom | |
| 262 ; _o_ = _*_ | |
| 263 ; _≈_ = _⋍_ | |
| 264 ; Id = K-id | |
| 265 ; isCategory = isKleisliCategory | |
| 266 } | |
| 56 | 267 |
| 82 | 268 -- |
| 269 -- Resolution | |
| 270 -- T = U_T U_F | |
| 271 -- nat-ε | |
| 272 -- nat-η | |
| 273 -- | |
| 274 | |
| 80 | 275 ufmap : {a b : Obj A} (f : KHom a b ) -> Hom A (FObj T a) (FObj T b) |
| 276 ufmap {a} {b} f = A [ TMap μ (b) o FMap T (KMap f) ] | |
| 277 | |
| 75 | 278 U_T : Functor KleisliCategory A |
| 279 U_T = record { | |
| 280 FObj = FObj T | |
| 281 ; FMap = ufmap | |
| 282 ; isFunctor = record | |
| 283 { ≈-cong = ≈-cong | |
| 284 ; identity = identity | |
| 76 | 285 ; distr = distr1 |
| 75 | 286 } |
| 287 } where | |
| 288 identity : {a : Obj A} → A [ ufmap (K-id {a}) ≈ id1 A (FObj T a) ] | |
| 289 identity {a} = let open ≈-Reasoning (A) in | |
| 290 begin | |
| 291 TMap μ (a) o FMap T (TMap η a) | |
| 292 ≈⟨ IsMonad.unity2 (isMonad M) ⟩ | |
| 293 id1 A (FObj T a) | |
| 294 ∎ | |
| 295 ≈-cong : {a b : Obj A} {f g : KHom a b} → A [ KMap f ≈ KMap g ] → A [ ufmap f ≈ ufmap g ] | |
| 296 ≈-cong {a} {b} {f} {g} f≈g = let open ≈-Reasoning (A) in | |
| 297 begin | |
| 298 TMap μ (b) o FMap T (KMap f) | |
| 299 ≈⟨ cdr (fcong T f≈g) ⟩ | |
| 300 TMap μ (b) o FMap T (KMap g) | |
| 301 ∎ | |
| 76 | 302 distr1 : {a b c : Obj A} {f : KHom a b} {g : KHom b c} → A [ ufmap (g * f) ≈ (A [ ufmap g o ufmap f ] )] |
| 303 distr1 {a} {b} {c} {f} {g} = let open ≈-Reasoning (A) in | |
| 75 | 304 begin |
| 305 ufmap (g * f) | |
| 76 | 306 ≈⟨⟩ |
| 307 ufmap {a} {c} ( record { KMap = TMap μ (c) o (FMap T (KMap g) o (KMap f)) } ) | |
| 308 ≈⟨⟩ | |
| 309 TMap μ (c) o FMap T ( TMap μ (c) o (FMap T (KMap g) o (KMap f))) | |
| 310 ≈⟨ cdr ( distr T) ⟩ | |
| 311 TMap μ (c) o (( FMap T ( TMap μ (c)) o FMap T (FMap T (KMap g) o (KMap f)))) | |
| 312 ≈⟨ assoc ⟩ | |
| 313 (TMap μ (c) o ( FMap T ( TMap μ (c)))) o FMap T (FMap T (KMap g) o (KMap f)) | |
| 314 ≈⟨ car (sym (IsMonad.assoc (isMonad M))) ⟩ | |
| 315 (TMap μ (c) o ( TMap μ (FObj T c))) o FMap T (FMap T (KMap g) o (KMap f)) | |
| 316 ≈⟨ sym assoc ⟩ | |
| 317 TMap μ (c) o (( TMap μ (FObj T c)) o FMap T (FMap T (KMap g) o (KMap f))) | |
| 318 ≈⟨ cdr (cdr (distr T)) ⟩ | |
| 319 TMap μ (c) o (( TMap μ (FObj T c)) o (FMap T (FMap T (KMap g)) o FMap T (KMap f))) | |
| 320 ≈⟨ cdr (assoc) ⟩ | |
| 321 TMap μ (c) o ((( TMap μ (FObj T c)) o (FMap T (FMap T (KMap g)))) o FMap T (KMap f)) | |
| 322 ≈⟨ sym (cdr (car (nat μ ))) ⟩ | |
| 323 TMap μ (c) o ((FMap T (KMap g ) o TMap μ (b)) o FMap T (KMap f )) | |
| 324 ≈⟨ cdr (sym assoc) ⟩ | |
| 325 TMap μ (c) o (FMap T (KMap g ) o ( TMap μ (b) o FMap T (KMap f ))) | |
| 326 ≈⟨ assoc ⟩ | |
| 327 ( TMap μ (c) o FMap T (KMap g ) ) o ( TMap μ (b) o FMap T (KMap f ) ) | |
| 328 ≈⟨⟩ | |
| 75 | 329 ufmap g o ufmap f |
| 330 ∎ | |
| 331 | |
| 332 | |
| 333 ffmap : {a b : Obj A} (f : Hom A a b) -> KHom a b | |
| 334 ffmap f = record { KMap = A [ TMap η (Category.cod A f) o f ] } | |
| 335 | |
| 336 F_T : Functor A KleisliCategory | |
| 337 F_T = record { | |
| 338 FObj = \a -> a | |
| 339 ; FMap = ffmap | |
| 340 ; isFunctor = record | |
| 341 { ≈-cong = ≈-cong | |
| 342 ; identity = identity | |
| 76 | 343 ; distr = distr1 |
| 75 | 344 } |
| 345 } where | |
| 346 identity : {a : Obj A} → A [ A [ TMap η a o id1 A a ] ≈ TMap η a ] | |
| 347 identity {a} = IsCategory.identityR ( Category.isCategory A) | |
| 82 | 348 -- Category.cod A f and Category.cod A g are actualy the same b, so we don't need cong-≈, just refl |
| 75 | 349 lemma1 : {a b : Obj A} {f g : Hom A a b} → A [ f ≈ g ] → A [ TMap η b ≈ TMap η b ] |
| 350 lemma1 f≈g = IsEquivalence.refl (IsCategory.isEquivalence ( Category.isCategory A )) | |
| 351 ≈-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 ] ] | |
| 352 ≈-cong f≈g = (IsCategory.o-resp-≈ (Category.isCategory A)) f≈g ( lemma1 f≈g ) | |
| 76 | 353 distr1 : {a b c : Obj A} {f : Hom A a b} {g : Hom A b c} → |
| 75 | 354 ( ffmap (A [ g o f ]) ⋍ ( ffmap g * ffmap f ) ) |
| 77 | 355 distr1 {a} {b} {c} {f} {g} = let open ≈-Reasoning (A) in |
| 75 | 356 begin |
| 357 KMap (ffmap (A [ g o f ])) | |
| 77 | 358 ≈⟨⟩ |
| 359 TMap η (c) o (g o f) | |
| 360 ≈⟨ assoc ⟩ | |
| 361 (TMap η (c) o g) o f | |
| 362 ≈⟨ car (sym (nat η)) ⟩ | |
| 363 (FMap T g o TMap η (b)) o f | |
| 364 ≈⟨ sym idL ⟩ | |
| 365 id1 A (FObj T c) o ((FMap T g o TMap η (b)) o f) | |
| 366 ≈⟨ sym (car (IsMonad.unity2 (isMonad M))) ⟩ | |
| 367 (TMap μ c o FMap T (TMap η c)) o ((FMap T g o TMap η (b)) o f) | |
| 368 ≈⟨ sym assoc ⟩ | |
| 369 TMap μ c o ( FMap T (TMap η c) o ((FMap T g o TMap η (b)) o f) ) | |
| 370 ≈⟨ cdr (cdr (sym assoc)) ⟩ | |
| 371 TMap μ c o ( FMap T (TMap η c) o (FMap T g o (TMap η (b) o f))) | |
| 372 ≈⟨ cdr assoc ⟩ | |
| 373 TMap μ c o ( ( FMap T (TMap η c) o FMap T g ) o (TMap η (b) o f) ) | |
| 374 ≈⟨ sym (cdr ( car ( distr T ))) ⟩ | |
| 375 TMap μ c o ( ( FMap T (TMap η c o g)) o (TMap η (b) o f)) | |
| 376 ≈⟨ assoc ⟩ | |
| 377 (TMap μ c o ( FMap T (TMap η c o g))) o (TMap η (b) o f) | |
| 378 ≈⟨ assoc ⟩ | |
| 379 ((TMap μ c o (FMap T (TMap η c o g))) o TMap η b) o f | |
| 380 ≈⟨ sym assoc ⟩ | |
| 381 (TMap μ c o (FMap T (TMap η c o g))) o (TMap η b o f) | |
| 382 ≈⟨ sym assoc ⟩ | |
| 383 TMap μ c o ( (FMap T (TMap η c o g)) o (TMap η b o f) ) | |
| 384 ≈⟨⟩ | |
| 385 join K (TMap η c o g) (TMap η b o f) | |
| 386 ≈⟨⟩ | |
| 75 | 387 KMap ( ffmap g * ffmap f ) |
| 388 ∎ | |
| 389 | |
| 82 | 390 -- |
| 391 -- T = (U_T ○ F_T) | |
| 392 -- | |
| 393 | |
| 79 | 394 Lemma11-1 : ∀{a b : Obj A} -> (f : Hom A a b ) -> A [ FMap T f ≈ FMap (U_T ○ F_T) f ] |
| 395 Lemma11-1 {a} {b} f = let open ≈-Reasoning (A) in | |
| 396 sym ( begin | |
| 397 FMap (U_T ○ F_T) f | |
| 398 ≈⟨⟩ | |
| 399 FMap U_T ( FMap F_T f ) | |
| 400 ≈⟨⟩ | |
| 401 TMap μ (b) o FMap T (KMap ( ffmap f ) ) | |
| 402 ≈⟨⟩ | |
| 403 TMap μ (b) o FMap T (TMap η (b) o f) | |
| 404 ≈⟨ cdr (distr T ) ⟩ | |
| 405 TMap μ (b) o ( FMap T (TMap η (b)) o FMap T f) | |
| 406 ≈⟨ assoc ⟩ | |
| 407 (TMap μ (b) o FMap T (TMap η (b))) o FMap T f | |
| 408 ≈⟨ car (IsMonad.unity2 (isMonad M)) ⟩ | |
| 409 id1 A (FObj T b) o FMap T f | |
| 410 ≈⟨ idL ⟩ | |
| 411 FMap T f | |
| 412 ∎ ) | |
| 413 | |
| 82 | 414 -- construct ≃ |
| 415 | |
|
81
0404b2ba7db6
Resolution Adjoint proved.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
80
diff
changeset
|
416 Lemma11 : T ≃ (U_T ○ F_T) |
|
0404b2ba7db6
Resolution Adjoint proved.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
80
diff
changeset
|
417 Lemma11 f = Category.Cat.refl (Lemma11-1 f) |
| 78 | 418 |
| 82 | 419 -- |
| 420 -- natural transformations | |
| 421 -- | |
| 422 | |
| 78 | 423 nat-η : NTrans A A identityFunctor ( U_T ○ F_T ) |
| 424 nat-η = record { TMap = \x -> TMap η x ; isNTrans = isNTrans1 } where | |
| 79 | 425 naturality1 : {a b : Obj A} {f : Hom A a b} |
| 426 → A [ A [ ( FMap ( U_T ○ F_T ) f ) o ( TMap η a ) ] ≈ A [ (TMap η b ) o f ] ] | |
| 427 naturality1 {a} {b} {f} = let open ≈-Reasoning (A) in | |
| 428 begin | |
| 429 ( FMap ( U_T ○ F_T ) f ) o ( TMap η a ) | |
| 84 | 430 ≈⟨ sym (resp refl-hom (Lemma11-1 f)) ⟩ |
| 431 FMap T f o TMap η a | |
| 79 | 432 ≈⟨ nat η ⟩ |
| 84 | 433 TMap η b o f |
| 79 | 434 ∎ |
| 78 | 435 isNTrans1 : IsNTrans A A identityFunctor ( U_T ○ F_T ) (\a -> TMap η a) |
| 79 | 436 isNTrans1 = record { naturality = naturality1 } |
| 77 | 437 |
| 79 | 438 tmap-ε : (a : Obj A) -> KHom (FObj T a) a |
| 78 | 439 tmap-ε a = record { KMap = id1 A (FObj T a) } |
| 440 | |
| 441 nat-ε : NTrans KleisliCategory KleisliCategory ( F_T ○ U_T ) identityFunctor | |
| 442 nat-ε = record { TMap = \a -> tmap-ε a; isNTrans = isNTrans1 } where | |
| 79 | 443 naturality1 : {a b : Obj A} {f : KHom a b} |
| 78 | 444 → (f * ( tmap-ε a ) ) ⋍ (( tmap-ε b ) * ( FMap (F_T ○ U_T) f ) ) |
| 79 | 445 naturality1 {a} {b} {f} = let open ≈-Reasoning (A) in |
| 446 sym ( begin | |
| 447 KMap (( tmap-ε b ) * ( FMap (F_T ○ U_T) f )) | |
| 80 | 448 ≈⟨⟩ |
| 449 TMap μ b o ( FMap T ( id1 A (FObj T b) ) o ( KMap (FMap (F_T ○ U_T) f ) )) | |
| 450 ≈⟨ cdr ( cdr ( | |
| 451 begin | |
| 452 KMap (FMap (F_T ○ U_T) f ) | |
| 453 ≈⟨⟩ | |
| 454 KMap (FMap F_T (FMap U_T f)) | |
| 455 ≈⟨⟩ | |
| 456 TMap η (FObj T b) o (TMap μ (b) o FMap T (KMap f)) | |
| 457 ∎ | |
| 458 )) ⟩ | |
| 459 TMap μ b o ( FMap T ( id1 A (FObj T b) ) o (TMap η (FObj T b) o (TMap μ (b) o FMap T (KMap f)))) | |
| 460 ≈⟨ cdr (car (IsFunctor.identity (isFunctor T))) ⟩ | |
| 461 TMap μ b o ( id1 A (FObj T (FObj T b) ) o (TMap η (FObj T b) o (TMap μ (b) o FMap T (KMap f)))) | |
| 462 ≈⟨ cdr idL ⟩ | |
| 463 TMap μ b o (TMap η (FObj T b) o (TMap μ (b) o FMap T (KMap f))) | |
| 464 ≈⟨ assoc ⟩ | |
| 465 (TMap μ b o (TMap η (FObj T b))) o (TMap μ (b) o FMap T (KMap f)) | |
| 466 ≈⟨ (car (IsMonad.unity1 (isMonad M))) ⟩ | |
| 467 id1 A (FObj T b) o (TMap μ (b) o FMap T (KMap f)) | |
| 468 ≈⟨ idL ⟩ | |
| 469 TMap μ b o FMap T (KMap f) | |
| 470 ≈⟨ cdr (sym idR) ⟩ | |
| 471 TMap μ b o ( FMap T (KMap f) o id1 A (FObj T a) ) | |
| 472 ≈⟨⟩ | |
| 79 | 473 KMap (f * ( tmap-ε a )) |
| 474 ∎ ) | |
| 78 | 475 isNTrans1 : IsNTrans KleisliCategory KleisliCategory ( F_T ○ U_T ) identityFunctor (\a -> tmap-ε a ) |
| 79 | 476 isNTrans1 = record { naturality = naturality1 } |
| 77 | 477 |
| 82 | 478 -- |
| 479 -- μ = U_T ε U_F | |
| 480 -- | |
| 79 | 481 Lemma12 : {x : Obj A } -> A [ TMap μ x ≈ FMap U_T ( TMap nat-ε ( FObj F_T x ) ) ] |
| 80 | 482 Lemma12 {x} = let open ≈-Reasoning (A) in |
| 483 sym ( begin | |
| 484 FMap U_T ( TMap nat-ε ( FObj F_T x ) ) | |
| 485 ≈⟨⟩ | |
| 486 TMap μ x o FMap T (id1 A (FObj T x) ) | |
| 487 ≈⟨ cdr (IsFunctor.identity (isFunctor T)) ⟩ | |
| 488 TMap μ x o id1 A (FObj T (FObj T x) ) | |
| 489 ≈⟨ idR ⟩ | |
| 490 TMap μ x | |
| 491 ∎ ) | |
| 78 | 492 |
| 77 | 493 |
| 84 | 494 Adj_T : Adjunction A KleisliCategory U_T F_T nat-η nat-ε |
| 495 Adj_T = record { | |
| 80 | 496 isAdjunction = record { |
| 497 adjoint1 = adjoint1 ; | |
| 498 adjoint2 = adjoint2 | |
| 499 } | |
| 500 } where | |
| 501 adjoint1 : { b : Obj KleisliCategory } → | |
| 502 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
|
503 adjoint1 {b} = let open ≈-Reasoning (A) in |
|
0404b2ba7db6
Resolution Adjoint proved.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
80
diff
changeset
|
504 begin |
|
0404b2ba7db6
Resolution Adjoint proved.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
80
diff
changeset
|
505 ( 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
|
506 ≈⟨⟩ |
|
0404b2ba7db6
Resolution Adjoint proved.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
80
diff
changeset
|
507 (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
|
508 ≈⟨ car ( cdr (IsFunctor.identity (isFunctor T))) ⟩ |
|
0404b2ba7db6
Resolution Adjoint proved.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
80
diff
changeset
|
509 (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
|
510 ≈⟨ car idR ⟩ |
|
0404b2ba7db6
Resolution Adjoint proved.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
80
diff
changeset
|
511 TMap μ (b) o ( TMap η ( FObj T b )) |
|
0404b2ba7db6
Resolution Adjoint proved.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
80
diff
changeset
|
512 ≈⟨ IsMonad.unity1 (isMonad M) ⟩ |
|
0404b2ba7db6
Resolution Adjoint proved.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
80
diff
changeset
|
513 id1 A (FObj U_T b) |
|
0404b2ba7db6
Resolution Adjoint proved.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
80
diff
changeset
|
514 ∎ |
| 80 | 515 adjoint2 : {a : Obj A} → |
| 516 KleisliCategory [ KleisliCategory [ ( TMap nat-ε ( FObj F_T a )) o ( FMap F_T ( TMap nat-η a )) ] | |
| 517 ≈ id1 KleisliCategory (FObj F_T a) ] | |
|
81
0404b2ba7db6
Resolution Adjoint proved.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
80
diff
changeset
|
518 adjoint2 {a} = let open ≈-Reasoning (A) in |
|
0404b2ba7db6
Resolution Adjoint proved.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
80
diff
changeset
|
519 begin |
|
0404b2ba7db6
Resolution Adjoint proved.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
80
diff
changeset
|
520 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
|
521 ≈⟨⟩ |
|
0404b2ba7db6
Resolution Adjoint proved.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
80
diff
changeset
|
522 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
|
523 ≈⟨ cdr ( car ( IsFunctor.identity (isFunctor T))) ⟩ |
|
0404b2ba7db6
Resolution Adjoint proved.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
80
diff
changeset
|
524 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
|
525 ≈⟨ cdr ( idL ) ⟩ |
|
0404b2ba7db6
Resolution Adjoint proved.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
80
diff
changeset
|
526 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
|
527 ≈⟨ assoc ⟩ |
|
0404b2ba7db6
Resolution Adjoint proved.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
80
diff
changeset
|
528 (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
|
529 ≈⟨ car (IsMonad.unity1 (isMonad M)) ⟩ |
|
0404b2ba7db6
Resolution Adjoint proved.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
80
diff
changeset
|
530 id1 A (FObj T a) o (TMap η a) |
|
0404b2ba7db6
Resolution Adjoint proved.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
80
diff
changeset
|
531 ≈⟨ idL ⟩ |
|
0404b2ba7db6
Resolution Adjoint proved.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
80
diff
changeset
|
532 TMap η a |
|
0404b2ba7db6
Resolution Adjoint proved.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
80
diff
changeset
|
533 ≈⟨⟩ |
|
0404b2ba7db6
Resolution Adjoint proved.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
80
diff
changeset
|
534 TMap η (FObj F_T a) |
|
0404b2ba7db6
Resolution Adjoint proved.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
80
diff
changeset
|
535 ≈⟨⟩ |
|
0404b2ba7db6
Resolution Adjoint proved.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
80
diff
changeset
|
536 KMap (id1 KleisliCategory (FObj F_T a)) |
| 82 | 537 ∎ |
| 77 | 538 |
| 84 | 539 nat-μ : NTrans A A (( U_T ○ F_T ) ○ (U_T ○ F_T)) (U_T ○ F_T) |
| 540 nat-μ = {!!} | |
| 541 | |
| 542 M_T : Monad A ( U_T ○ F_T ) nat-η nat-μ | |
| 543 M_T = {!!} | |
| 544 | |
| 545 Resolution_T : Resolution A KleisliCategory M_T Adj_T | |
| 546 Resolution_T = record { | |
| 547 μ=UεF = {!!} | |
| 548 } | |
| 549 | |
| 75 | 550 |
| 83 | 551 module comparison-functor {c₁' c₂' ℓ' : Level} ( B : Category c₁ c₂ ℓ ) |
| 552 { U_K : Functor B A } { F_K : Functor A B } | |
| 553 { η_K : NTrans A A identityFunctor ( U_K ○ F_K ) } | |
| 554 { ε_K : NTrans B B ( F_K ○ U_K ) identityFunctor } | |
| 555 ( Adj : Adjunction A B U_K F_K η_K ε_K ) | |
| 556 where | |
| 75 | 557 |
| 84 | 558 kfmap : {!!} |
| 559 kfmap = {!!} | |
| 75 | 560 |
| 83 | 561 K_T : Functor KleisliCategory B |
| 562 K_T = record { | |
| 563 FObj = FObj F_K | |
| 564 ; FMap = kfmap | |
| 565 ; isFunctor = record | |
| 84 | 566 { ≈-cong = {!!} -- ≈-cong |
| 567 ; identity = {!!} -- identity | |
| 568 ; distr = {!!} -- distr1 | |
| 83 | 569 } |
| 84 | 570 } -- where |
| 571 -- identity : {a : Obj B} → B [ kfmap (K-id {a}) ≈ id1 B (FObj T a) ] | |
| 572 -- identity {a} = let open ≈-Reasoning (B) in | |
| 573 -- begin | |
| 574 -- ? | |
| 575 -- ≈⟨ ? ⟩ | |
| 576 -- ? | |
| 577 -- ∎ | |
| 578 -- ≈-cong : {a b : Obj B} {f g : KHom a b} → B [ KMap f ≈ KMap g ] → B [ kfmap f ≈ kfmap g ] | |
| 579 -- ≈-cong {a} {b} {f} {g} f≈g = let open ≈-Reasoning (B) in | |
| 580 -- begin | |
| 581 -- ? | |
| 582 -- ≈⟨ ? ⟩ | |
| 583 -- ? | |
| 584 -- ∎ | |
| 585 -- distr1 : {a b c : Obj B} {f : KHom a b} {g : KHom b c} → B [ kfmap (g * f) ≈ (B [ kfmap g o kfmap f ] )] | |
| 586 -- distr1 {a} {b} {c} {f} {g} = let open ≈-Reasoning (B) in | |
| 587 -- begin | |
| 588 -- ? | |
| 589 -- ≈⟨ ? ⟩ | |
| 590 -- ? | |
| 591 -- ∎ | |
| 75 | 592 |