Mercurial > hg > Members > kono > Proof > category

comparison freyd2.agda @ 658:9242298cffa8

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
adjoint functor theorem done
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Thu, 06 Jul 2017 13:50:45 +0900
parents 0d029674eb59
children 372205f40ab0
comparison
equal deleted inserted replaced
657:0d029674eb59 658:9242298cffa8
500 FMap U (A [ FMap (identityFunctor {_} {_} {_} {A}) f o arrow (initial (In (FObj U a)) 500 FMap U (A [ FMap (identityFunctor {_} {_} {_} {A}) f o arrow (initial (In (FObj U a))
501 (record { obj = a ; hom = id1 B (FObj U a) })) ] ) o tmap-η (FObj U a) 501 (record { obj = a ; hom = id1 B (FObj U a) })) ] ) o tmap-η (FObj U a)
502 ≈⟨ car (distr U) ⟩ 502 ≈⟨ car (distr U) ⟩
503 ( FMap U (FMap (identityFunctor {_} {_} {_} {A}) f) o FMap U (arrow (initial (In (FObj U a)) 503 ( FMap U (FMap (identityFunctor {_} {_} {_} {A}) f) o FMap U (arrow (initial (In (FObj U a))
504 (record { obj = a ; hom = id1 B (FObj U a) })))) o (tmap-η (FObj U a)) 504 (record { obj = a ; hom = id1 B (FObj U a) })))) o (tmap-η (FObj U a))
505 ≈⟨ {!!} ⟩ 505 ≈↑⟨ assoc ⟩
506 FMap U f 506 FMap U (FMap (identityFunctor {_} {_} {_} {A}) f) o (FMap U (arrow (initial (In (FObj U a))
507 ≈↑⟨ idR ⟩ 507 (record { obj = a ; hom = id1 B (FObj U a) }))) o tmap-η (FObj U a) )
508 ≈⟨ cdr ( univ (id1 B (FObj U a))) ⟩
509 FMap U (FMap (identityFunctor {_} {_} {_} {A}) f) o id1 B (FObj U a)
510 ≈⟨⟩
508 FMap U f o id1 B (FObj U a) 511 FMap U f o id1 B (FObj U a)
509 ∎ 512 ∎
510 lemma-nat2 : {a b : Obj A} {f : Hom A a b} → 513 lemma-nat2 : {a b : Obj A} {f : Hom A a b} →
511 B [ B [ FMap U (A [ arrow (initial (In (FObj U b)) 514 B [ B [ FMap U (A [ arrow (initial (In (FObj U b))
512 (record { obj = b ; hom = id1 B (FObj U b) })) o FMap (F ○ U) f ] ) o tmap-η (FObj U a) ] 515 (record { obj = b ; hom = id1 B (FObj U b) })) o FMap (F ○ U) f ] ) o tmap-η (FObj U a) ]
513 ≈ B [ FMap U f o id1 B (FObj U a) ] ] 516 ≈ B [ FMap U f o id1 B (FObj U a) ] ]
514 lemma-nat2 {a} {b} {f} = let open ≈-Reasoning B in begin 517 lemma-nat2 {a} {b} {f} = let open ≈-Reasoning B in begin
515 FMap U (A [ arrow (initial (In (FObj U b)) 518 FMap U (A [ arrow (initial (In (FObj U b))
516 (record { obj = b ; hom = id1 B (FObj U b) })) o FMap (F ○ U) f ] ) o tmap-η (FObj U a) 519 (record { obj = b ; hom = id1 B (FObj U b) })) o FMap (F ○ U) f ] ) o tmap-η (FObj U a)
517 ≈⟨ {!!} ⟩ 520 ≈⟨ car (distr U) ⟩
521 ( FMap U (arrow (initial (In (FObj U b)) (record { obj = b ; hom = id1 B (FObj U b) })))
522 o FMap U ( FMap (F ○ U) f )) o tmap-η (FObj U a)
523 ≈↑⟨ assoc ⟩
524 FMap U (arrow (initial (In (FObj U b)) (record { obj = b ; hom = id1 B (FObj U b) })))
525 o ( FMap U ( FMap (F ○ U) f ) o tmap-η (FObj U a) )
526 ≈⟨ cdr ( univ ( tmap-η (FObj U b) o FMap U f ) ) ⟩
527 FMap U (arrow (initial (In (FObj U b)) (record { obj = b ; hom = id1 B (FObj U b) })))
528 o ( tmap-η (FObj U b) o FMap U f )
529 ≈⟨ assoc ⟩
530 ( FMap U (arrow (initial (In (FObj U b)) (record { obj = b ; hom = id1 B (FObj U b) })))
531 o tmap-η (FObj U b) ) o FMap U f
532 ≈⟨ car (univ (id1 B (FObj U b))) ⟩
533 id1 B (FObj U b) o FMap U f
534 ≈⟨ idL ⟩
535 FMap U f
536 ≈↑⟨ idR ⟩
518 FMap U f o id1 B (FObj U a) 537 FMap U f o id1 B (FObj U a)
519 ∎ 538 ∎
520 comm1 : {a b : Obj A} {f : Hom A a b} → 539 comm1 : {a b : Obj A} {f : Hom A a b} →
521 A [ A [ FMap (identityFunctor {_} {_} {_} {A}) f o 540 A [ A [ FMap (identityFunctor {_} {_} {_} {A}) f o
522 arrow (initial (In (FObj U a)) (record { obj = a ; hom = id1 B (FObj U a) })) ] 541 arrow (initial (In (FObj U a)) (record { obj = a ; hom = id1 B (FObj U a) })) ]
549 FisLeftAdjoint = record { isAdjunction = record { 568 FisLeftAdjoint = record { isAdjunction = record {
550 adjoint1 = adjoint1 569 adjoint1 = adjoint1
551 ; adjoint2 = adjoint2 570 ; adjoint2 = adjoint2
552 } } where 571 } } where
553 adjoint1 : {b : Obj A} → B [ B [ FMap U (TMap nat-ε b) o TMap nat-η (FObj U b) ] ≈ id1 B (FObj U b) ] 572 adjoint1 : {b : Obj A} → B [ B [ FMap U (TMap nat-ε b) o TMap nat-η (FObj U b) ] ≈ id1 B (FObj U b) ]
554 adjoint1 = {!!} 573 adjoint1 {b} = let open ≈-Reasoning B in begin
574 FMap U (TMap nat-ε b) o TMap nat-η (FObj U b)
575 ≈⟨ univ (id1 B (FObj U b)) ⟩
576 id1 B (FObj U b)
577 ∎
578 adj2comm1 : {a : Obj B} → B [ B [ FMap U (A [ TMap nat-ε (FObj F a) o FMap F (TMap nat-η a) ]) o
579 tmap-η (FObj (identityFunctor {_} {_} {_} {B}) a) ] ≈ tmap-η a ]
580 adj2comm1 {a} = let open ≈-Reasoning B in begin
581 FMap U (A [ TMap nat-ε (FObj F a) o FMap F (TMap nat-η a) ]) o tmap-η a
582 ≈⟨ car (distr U) ⟩
583 (FMap U (TMap nat-ε (FObj F a)) o FMap U (FMap F (TMap nat-η a) )) o tmap-η a
584 ≈↑⟨ assoc ⟩
585 FMap U (TMap nat-ε (FObj F a)) o (FMap U (FMap F (TMap nat-η a) ) o tmap-η a )
586 ≈⟨ cdr ( univ (tmap-η (FObj U (obj (i a))) o tmap-η a )) ⟩
587 FMap U (TMap nat-ε (FObj F a)) o (tmap-η (FObj U (obj (i a))) o tmap-η a )
588 ≈⟨ assoc ⟩
589 ( FMap U (TMap nat-ε (FObj F a)) o tmap-η (FObj U (obj (i a)))) o tmap-η a
590 ≈⟨ car (univ (id1 B (FObj U (FObj F a)))) ⟩
591 id1 B (FObj U (FObj F a)) o tmap-η a
592 ≈⟨ idL ⟩
593 tmap-η a
594 ∎
595 adj2comm2 : {a : Obj B} → B [ B [ FMap U (id1 A (FObj F a)) o tmap-η a ] ≈ tmap-η a ]
596 adj2comm2 {a} = let open ≈-Reasoning B in begin
597 FMap U (id1 A (FObj F a)) o tmap-η a
598 ≈⟨ car (IsFunctor.identity (isFunctor U)) ⟩
599 id1 B (FObj U (obj (i a))) o tmap-η a
600 ≈⟨ idL ⟩
601 tmap-η a
602 ∎
555 adjoint2 : {a : Obj B} → A [ A [ TMap nat-ε (FObj F a) o FMap F (TMap nat-η a) ] ≈ id1 A (FObj F a) ] 603 adjoint2 : {a : Obj B} → A [ A [ TMap nat-ε (FObj F a) o FMap F (TMap nat-η a) ] ≈ id1 A (FObj F a) ]
556 adjoint2 = {!!} 604 adjoint2 {a} = let open ≈-Reasoning A in begin
605 TMap nat-ε (FObj F a) o FMap F (TMap nat-η a)
606 ≈↑⟨ unique adj2comm1 ⟩
607 arrow (solution ( tmap-η a ) )
608 ≈⟨ unique adj2comm2 ⟩
609 id1 A (FObj F a)
610 ∎