Mercurial > hg > Members > kono > Proof > category

comparison nat.agda @ 73:b75b5792bd81

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
on going
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Fri, 26 Jul 2013 15:52:24 +0900
parents cbc30519e961
children 49e6eb3ef9c0
comparison
equal deleted inserted replaced
72:cbc30519e961 73:b75b5792bd81
90 let open ≈-Reasoning ( L ) in 90 let open ≈-Reasoning ( L ) in
91 begin L [ x o y ] ∎ 91 begin L [ x o y ] ∎
92 92
93 open Kleisli 93 open Kleisli
94 -- η(b) ○ f = f 94 -- η(b) ○ f = f
95 Lemma7 : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) → 95 Lemma7 : { a : Obj A } { b : Obj A } ( f : Hom A a ( FObj T b) )
96 { T : Functor A A } 96 → A [ join K (TMap η b) f ≈ f ]
97 ( η : NTrans A A identityFunctor T ) 97 Lemma7 {_} {b} f =
98 { μ : NTrans A A (T ○ T) T } 98 let open ≈-Reasoning (A) in
99 { a : Obj A } ( b : Obj A )
100 ( f : Hom A a ( FObj T b) )
101 ( m : Monad A T η μ )
102 { k : Kleisli A T η μ m}
103 → A [ join k (TMap η b) f ≈ f ]
104 Lemma7 c {T} η b f m {k} =
105 let open ≈-Reasoning (c)
106 μ = mu ( monad k )
107 in
108 begin 99 begin
109 join k (TMap η b) f 100 join K (TMap η b) f
110 ≈⟨ refl-hom ⟩ 101 ≈⟨ refl-hom ⟩
111 c [ TMap μ b o c [ FMap T ((TMap η b)) o f ] ] 102 A [ TMap μ b o A [ FMap T ((TMap η b)) o f ] ]
112 ≈⟨ IsCategory.associative (Category.isCategory c) ⟩ 103 ≈⟨ IsCategory.associative (Category.isCategory A) ⟩
113 c [ c [ TMap μ b o FMap T ((TMap η b)) ] o f ] 104 A [ A [ TMap μ b o FMap T ((TMap η b)) ] o f ]
114 ≈⟨ car ( IsMonad.unity2 ( isMonad ( monad k )) ) ⟩ 105 ≈⟨ car ( IsMonad.unity2 ( isMonad ( monad K )) ) ⟩
115 c [ id (FObj T b) o f ] 106 A [ id (FObj T b) o f ]
116 ≈⟨ IsCategory.identityL (Category.isCategory c) ⟩ 107 ≈⟨ IsCategory.identityL (Category.isCategory A) ⟩
117 f 108 f
118 ∎ 109 ∎
119 110
120 -- f ○ η(a) = f 111 -- f ○ η(a) = f
121 Lemma8 : ( a : Obj A ) ( b : Obj A ) 112 Lemma8 : { a : Obj A } { b : Obj A }
122 ( f : Hom A a ( FObj T b) ) 113 ( f : Hom A a ( FObj T b) )
123 → A [ join K f (TMap η a) ≈ f ] 114 → A [ join K f (TMap η a) ≈ f ]
124 Lemma8 a b f = 115 Lemma8 {a} {b} f =
125 begin 116 begin
126 join K f (TMap η a) 117 join K f (TMap η a)
127 ≈⟨ refl-hom ⟩ 118 ≈⟨ refl-hom ⟩
128 A [ TMap μ b o A [ FMap T f o (TMap η a) ] ] 119 A [ TMap μ b o A [ FMap T f o (TMap η a) ] ]
129 ≈⟨ cdr ( nat η ) ⟩ 120 ≈⟨ cdr ( nat η ) ⟩
137 ∎ where 128 ∎ where
138 open ≈-Reasoning (A) 129 open ≈-Reasoning (A)
139 130
140 -- h ○ (g ○ f) = (h ○ g) ○ f 131 -- h ○ (g ○ f) = (h ○ g) ○ f
141 Lemma9 : { a b c d : Obj A } 132 Lemma9 : { a b c d : Obj A }
133 ( h : Hom A c ( FObj T d) )
134 ( g : Hom A b ( FObj T c) )
142 ( f : Hom A a ( FObj T b) ) 135 ( f : Hom A a ( FObj T b) )
143 ( g : Hom A b ( FObj T c) )
144 ( h : Hom A c ( FObj T d) )
145 → A [ join K h (join K g f) ≈ join K ( join K h g) f ] 136 → A [ join K h (join K g f) ≈ join K ( join K h g) f ]
146 Lemma9 {a} {b} {c} {d} f g h = 137 Lemma9 {a} {b} {c} {d} h g f =
147 begin 138 begin
148 join K h (join K g f) 139 join K h (join K g f)
149 ≈⟨⟩ 140 ≈⟨⟩
150 join K h ( ( TMap μ c o ( FMap T g o f ) ) ) 141 join K h ( ( TMap μ c o ( FMap T g o f ) ) )
151 ≈⟨ refl-hom ⟩ 142 ≈⟨ refl-hom ⟩
195 join K ( ( TMap μ d o ( FMap T h o g ) ) ) f 186 join K ( ( TMap μ d o ( FMap T h o g ) ) ) f
196 ≈⟨ refl-hom ⟩ 187 ≈⟨ refl-hom ⟩
197 join K ( join K h g) f 188 join K ( join K h g) f
198 ∎ where open ≈-Reasoning (A) 189 ∎ where open ≈-Reasoning (A)
199 190
200 KHom1 : (a : Obj A) → (b : Obj A) -> Set (c₂ ⊔ c₁)
201 KHom1 = {!!}
202
203 record KHom (a : Obj A) (b : Obj A) 191 record KHom (a : Obj A) (b : Obj A)
204 : Set (suc (c₂ ⊔ c₁)) where 192 : Set (suc (c₂ ⊔ c₁)) where
205 field 193 field
206 KMap : Hom A a ( FObj T b ) 194 KMap : Hom A a ( FObj T b )
207 195
208 K-id : {a : Obj A} → KHom a a 196 K-id : {a : Obj A} → KHom a a
209 K-id {a = a} = record { KMap = TMap η a } 197 K-id {a = a} = record { KMap = TMap η a }
210 198
211 open import Relation.Binary.Core 199 open import Relation.Binary.Core
212
213 _⋍_ :
214 { a : Obj A } { b : Obj A } (f g : KHom a b ) -> Set (suc ((c₂ ⊔ c₁) ⊔ ℓ))
215 _⋍_ = {!!}
216
217 open KHom 200 open KHom
201
202 _⋍_ : { a : Obj A } { b : Obj A } (f g : KHom a b ) -> Set ℓ -- (suc ((c₂ ⊔ c₁) ⊔ ℓ))
203 _⋍_ {a} {b} f g = A [ KMap f ≈ KMap g ]
218 204
219 _*_ : { a b : Obj A } → { c : Obj A } → 205 _*_ : { a b : Obj A } → { c : Obj A } →
220 ( KHom b c) → ( KHom a b) → KHom a c 206 ( KHom b c) → ( KHom a b) → KHom a c
221 _*_ {a} {b} {c} g f = record { KMap = join K {a} {b} {c} (KMap g) (KMap f) } 207 _*_ {a} {b} {c} g f = record { KMap = join K {a} {b} {c} (KMap g) (KMap f) }
222 208
226 ; identityR = KidR 212 ; identityR = KidR
227 ; o-resp-≈ = Ko-resp 213 ; o-resp-≈ = Ko-resp
228 ; associative = Kassoc 214 ; associative = Kassoc
229 } 215 }
230 where 216 where
217 open ≈-Reasoning (A)
231 isEquivalence : { a b : Obj A } -> 218 isEquivalence : { a b : Obj A } ->
232 IsEquivalence {_} {_} {KHom a b} _⋍_ 219 IsEquivalence {_} {_} {KHom a b} _⋍_
233 isEquivalence {C} {D} = 220 isEquivalence {C} {D} =
234 record { refl = λ {F} → ⋍-refl {F} 221 record { refl = λ {F} → ⋍-refl {F}
235 ; sym = λ {F} {G} → ⋍-sym {F} {G} 222 ; sym = λ {F} {G} → ⋍-sym {F} {G}
236 ; trans = λ {F} {G} {H} → ⋍-trans {F} {G} {H} 223 ; trans = λ {F} {G} {H} → ⋍-trans {F} {G} {H}
237 } where 224 } where
238 ⋍-refl : {F : KHom C D} → F ⋍ F 225 ⋍-refl : {F : KHom C D} → F ⋍ F
239 ⋍-refl = {!!} 226 ⋍-refl = refl-hom
240 ⋍-sym : {F G : KHom C D} → F ⋍ G → G ⋍ F 227 ⋍-sym : {F G : KHom C D} → F ⋍ G → G ⋍ F
241 ⋍-sym = {!!} 228 ⋍-sym = sym
242 ⋍-trans : {F G H : KHom C D} → F ⋍ G → G ⋍ H → F ⋍ H 229 ⋍-trans : {F G H : KHom C D} → F ⋍ G → G ⋍ H → F ⋍ H
243 ⋍-trans = {!!} 230 ⋍-trans = trans-hom
244 KidL : {C D : Obj A} -> {f : KHom C D} → (K-id * f) ⋍ f 231 KidL : {C D : Obj A} -> {f : KHom C D} → (K-id * f) ⋍ f
245 KidL = {!!} 232 KidL {_} {_} {f} = Lemma7 (KMap f)
246 KidR : {C D : Obj A} -> {f : KHom C D} → (f * K-id) ⋍ f 233 KidR : {C D : Obj A} -> {f : KHom C D} → (f * K-id) ⋍ f
247 KidR = {!!} 234 KidR {_} {_} {f} = Lemma8 (KMap f)
248 Ko-resp : {a b c : Obj A} -> {f g : KHom a b } → {h i : KHom b c } → 235 Ko-resp : {a b c : Obj A} -> {f g : KHom a b } → {h i : KHom b c } →
249 f ⋍ g → h ⋍ i → (h * f) ⋍ (i * g) 236 f ⋍ g → h ⋍ i → (h * f) ⋍ (i * g)
250 Ko-resp = {!!} 237 Ko-resp = {!!}
251 Kassoc : {a b c d : Obj A} -> {f : KHom c d } → {g : KHom b c } → {h : KHom a b } → 238 Kassoc : {a b c d : Obj A} -> {f : KHom c d } → {g : KHom b c } → {h : KHom a b } →
252 (f * (g * h)) ⋍ ((f * g) * h) 239 (f * (g * h)) ⋍ ((f * g) * h)
253 Kassoc = {!!} 240 Kassoc {_} {_} {_} {_} {f} {g} {h} = Lemma9 (KMap f) (KMap g) (KMap h)
254 241
255 242