Mercurial > hg > Members > kono > Proof > category

comparison nat.agda @ 95:4be27d290ea2

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
nat-μ
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Mon, 29 Jul 2013 14:08:45 +0900
parents 4fa718e4fd77
children 85425bd12835
comparison
equal deleted inserted replaced
94:4fa718e4fd77 95:4be27d290ea2
479 isNTrans1 = record { naturality = naturality1 } 479 isNTrans1 = record { naturality = naturality1 }
480 480
481 -- 481 --
482 -- μ = U_T ε U_F 482 -- μ = U_T ε U_F
483 -- 483 --
484 Lemma12 : {x : Obj A } -> A [ TMap μ x ≈ FMap U_T ( TMap nat-ε ( FObj F_T x ) ) ] 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 ) ) ]
485 Lemma12 {x} = let open ≈-Reasoning (A) in 509 Lemma12 {x} = let open ≈-Reasoning (A) in
510 sym ( begin
511 FMap U_T ( TMap nat-ε ( FObj F_T x ) )
512 ≈⟨⟩
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
486 sym ( begin 520 sym ( begin
487 FMap U_T ( TMap nat-ε ( FObj F_T x ) ) 521 FMap U_T ( TMap nat-ε ( FObj F_T x ) )
488 ≈⟨⟩ 522 ≈⟨⟩
489 TMap μ x o FMap T (id1 A (FObj T x) ) 523 TMap μ x o FMap T (id1 A (FObj T x) )
490 ≈⟨ cdr (IsFunctor.identity (isFunctor T)) ⟩ 524 ≈⟨ cdr (IsFunctor.identity (isFunctor T)) ⟩
491 TMap μ x o id1 A (FObj T (FObj T x) ) 525 TMap μ x o id1 A (FObj T (FObj T x) )
492 ≈⟨ idR ⟩ 526 ≈⟨ idR ⟩
493 TMap μ x 527 TMap μ x
494 ∎ ) 528 ∎ )
495
496 529
497 Adj_T : Adjunction A KleisliCategory U_T F_T nat-η nat-ε 530 Adj_T : Adjunction A KleisliCategory U_T F_T nat-η nat-ε
498 Adj_T = record { 531 Adj_T = record {
499 isAdjunction = record { 532 isAdjunction = record {
500 adjoint1 = adjoint1 ; 533 adjoint1 = adjoint1 ;
539 KMap (id1 KleisliCategory (FObj F_T a)) 572 KMap (id1 KleisliCategory (FObj F_T a))
540 ∎ 573 ∎
541 574
542 open MResolution 575 open MResolution
543 576
544 Resolution_T : MResolution A KleisliCategory T U_T F_T Adj_T 577 Resolution_T : MResolution A KleisliCategory T U_T F_T {nat-η} {nat-ε} {nat-μ} Adj_T
545 Resolution_T = record { 578 Resolution_T = record {
546 T=UF = Lemma11; 579 T=UF = Lemma11;
547 μ=UεF = Lemma12 580 μ=UεF = Lemma12
548 } 581 }
549 582