Mercurial > hg > Members > kono > Proof > category

comparison nat.agda @ 76:6c6c3dd8ef12

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
U done
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Fri, 26 Jul 2013 20:54:41 +0900
parents 8e665152c306
children 528c7e27af91
comparison
equal deleted inserted replaced
75:8e665152c306 76:6c6c3dd8ef12
268 FObj = FObj T 268 FObj = FObj T
269 ; FMap = ufmap 269 ; FMap = ufmap
270 ; isFunctor = record 270 ; isFunctor = record
271 { ≈-cong = ≈-cong 271 { ≈-cong = ≈-cong
272 ; identity = identity 272 ; identity = identity
273 ; distr = distr 273 ; distr = distr1
274 } 274 }
275 } where 275 } where
276 ufmap : {a b : Obj A} (f : KHom a b ) -> Hom A (FObj T a) (FObj T b) 276 ufmap : {a b : Obj A} (f : KHom a b ) -> Hom A (FObj T a) (FObj T b)
277 ufmap {a} {b} f = A [ TMap μ (b) o FMap T (KMap f) ] 277 ufmap {a} {b} f = A [ TMap μ (b) o FMap T (KMap f) ]
278 identity : {a : Obj A} → A [ ufmap (K-id {a}) ≈ id1 A (FObj T a) ] 278 identity : {a : Obj A} → A [ ufmap (K-id {a}) ≈ id1 A (FObj T a) ]
287 begin 287 begin
288 TMap μ (b) o FMap T (KMap f) 288 TMap μ (b) o FMap T (KMap f)
289 ≈⟨ cdr (fcong T f≈g) ⟩ 289 ≈⟨ cdr (fcong T f≈g) ⟩
290 TMap μ (b) o FMap T (KMap g) 290 TMap μ (b) o FMap T (KMap g)
291 ∎ 291 ∎
292 distr : {a b c : Obj A} {f : KHom a b} {g : KHom b c} → A [ ufmap (g * f) ≈ (A [ ufmap g o ufmap f ] )] 292 distr1 : {a b c : Obj A} {f : KHom a b} {g : KHom b c} → A [ ufmap (g * f) ≈ (A [ ufmap g o ufmap f ] )]
293 distr {_} {_} {c} {f} {g} = let open ≈-Reasoning (A) in 293 distr1 {a} {b} {c} {f} {g} = let open ≈-Reasoning (A) in
294 begin 294 begin
295 ufmap (g * f) 295 ufmap (g * f)
296 -- ≈⟨⟩ 296 ≈⟨⟩
297 -- TMap μ (FObj T c) o FMap T ( (TMap μ (c) o FMap T (KMap g)) o (KMap f)) 297 ufmap {a} {c} ( record { KMap = TMap μ (c) o (FMap T (KMap g) o (KMap f)) } )
298 ≈⟨ {!!} ⟩ 298 ≈⟨⟩
299 TMap μ (c) o FMap T ( TMap μ (c) o (FMap T (KMap g) o (KMap f)))
300 ≈⟨ cdr ( distr T) ⟩
301 TMap μ (c) o (( FMap T ( TMap μ (c)) o FMap T (FMap T (KMap g) o (KMap f))))
302 ≈⟨ assoc ⟩
303 (TMap μ (c) o ( FMap T ( TMap μ (c)))) o FMap T (FMap T (KMap g) o (KMap f))
304 ≈⟨ car (sym (IsMonad.assoc (isMonad M))) ⟩
305 (TMap μ (c) o ( TMap μ (FObj T c))) o FMap T (FMap T (KMap g) o (KMap f))
306 ≈⟨ sym assoc ⟩
307 TMap μ (c) o (( TMap μ (FObj T c)) o FMap T (FMap T (KMap g) o (KMap f)))
308 ≈⟨ cdr (cdr (distr T)) ⟩
309 TMap μ (c) o (( TMap μ (FObj T c)) o (FMap T (FMap T (KMap g)) o FMap T (KMap f)))
310 ≈⟨ cdr (assoc) ⟩
311 TMap μ (c) o ((( TMap μ (FObj T c)) o (FMap T (FMap T (KMap g)))) o FMap T (KMap f))
312 ≈⟨ sym (cdr (car (nat μ ))) ⟩
313 TMap μ (c) o ((FMap T (KMap g ) o TMap μ (b)) o FMap T (KMap f ))
314 ≈⟨ cdr (sym assoc) ⟩
315 TMap μ (c) o (FMap T (KMap g ) o ( TMap μ (b) o FMap T (KMap f )))
316 ≈⟨ assoc ⟩
317 ( TMap μ (c) o FMap T (KMap g ) ) o ( TMap μ (b) o FMap T (KMap f ) )
318 ≈⟨⟩
299 ufmap g o ufmap f 319 ufmap g o ufmap f
300 ∎ 320 ∎
301 321
302 322
303 ffmap : {a b : Obj A} (f : Hom A a b) -> KHom a b 323 ffmap : {a b : Obj A} (f : Hom A a b) -> KHom a b
308 FObj = \a -> a 328 FObj = \a -> a
309 ; FMap = ffmap 329 ; FMap = ffmap
310 ; isFunctor = record 330 ; isFunctor = record
311 { ≈-cong = ≈-cong 331 { ≈-cong = ≈-cong
312 ; identity = identity 332 ; identity = identity
313 ; distr = distr 333 ; distr = distr1
314 } 334 }
315 } where 335 } where
316 identity : {a : Obj A} → A [ A [ TMap η a o id1 A a ] ≈ TMap η a ] 336 identity : {a : Obj A} → A [ A [ TMap η a o id1 A a ] ≈ TMap η a ]
317 identity {a} = IsCategory.identityR ( Category.isCategory A) 337 identity {a} = IsCategory.identityR ( Category.isCategory A)
318 lemma1 : {a b : Obj A} {f g : Hom A a b} → A [ f ≈ g ] → A [ TMap η b ≈ TMap η b ] 338 lemma1 : {a b : Obj A} {f g : Hom A a b} → A [ f ≈ g ] → A [ TMap η b ≈ TMap η b ]
319 lemma1 f≈g = IsEquivalence.refl (IsCategory.isEquivalence ( Category.isCategory A )) 339 lemma1 f≈g = IsEquivalence.refl (IsCategory.isEquivalence ( Category.isCategory A ))
320 ≈-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 ] ] 340 ≈-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 ] ]
321 ≈-cong f≈g = (IsCategory.o-resp-≈ (Category.isCategory A)) f≈g ( lemma1 f≈g ) 341 ≈-cong f≈g = (IsCategory.o-resp-≈ (Category.isCategory A)) f≈g ( lemma1 f≈g )
322 distr : {a b c : Obj A} {f : Hom A a b} {g : Hom A b c} → 342 distr1 : {a b c : Obj A} {f : Hom A a b} {g : Hom A b c} →
323 ( ffmap (A [ g o f ]) ⋍ ( ffmap g * ffmap f ) ) 343 ( ffmap (A [ g o f ]) ⋍ ( ffmap g * ffmap f ) )
324 distr {_} {_} {_} {f} {g} = let open ≈-Reasoning (A) in 344 distr1 {_} {_} {_} {f} {g} = let open ≈-Reasoning (A) in
325 begin 345 begin
326 KMap (ffmap (A [ g o f ])) 346 KMap (ffmap (A [ g o f ]))
327 ≈⟨ {!!} ⟩ 347 ≈⟨ {!!} ⟩
328 KMap ( ffmap g * ffmap f ) 348 KMap ( ffmap g * ffmap f )
329 ∎ 349 ∎