Mercurial > hg > Members > kono > Proof > category

comparison freyd2.agda @ 657:0d029674eb59

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 Thu, 06 Jul 2017 12:22:54 +0900
parents 18431b63893b
children 9242298cffa8
comparison
equal deleted inserted replaced
656:18431b63893b 657:0d029674eb59
490 490
491 nat-ε : NTrans A A (F ○ U) identityFunctor 491 nat-ε : NTrans A A (F ○ U) identityFunctor
492 nat-ε = record { 492 nat-ε = record {
493 TMap = λ x → arrow ( solution (id1 B (FObj U x))) 493 TMap = λ x → arrow ( solution (id1 B (FObj U x)))
494 ; isNTrans = record { commute = comm1 } } where 494 ; isNTrans = record { commute = comm1 } } where
495 lemma-nat1 : {a b : Obj A} {f : Hom A a b} →
496 B [ B [ FMap U (A [ FMap (identityFunctor {_} {_} {_} {A}) f o arrow (initial (In (FObj U a))
497 (record { obj = a ; hom = id1 B (FObj U a) })) ] ) o tmap-η (FObj U a) ]
498 ≈ B [ FMap U f o id1 B (FObj U a) ] ]
499 lemma-nat1 {a} {b} {f} = let open ≈-Reasoning B in begin
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)
502 ≈⟨ car (distr U) ⟩
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))
505 ≈⟨ {!!} ⟩
506 FMap U f
507 ≈↑⟨ idR ⟩
508 FMap U f o id1 B (FObj U a)
509 ∎
510 lemma-nat2 : {a b : Obj A} {f : Hom A a b} →
511 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) ]
513 ≈ B [ FMap U f o id1 B (FObj U a) ] ]
514 lemma-nat2 {a} {b} {f} = let open ≈-Reasoning B in begin
515 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)
517 ≈⟨ {!!} ⟩
518 FMap U f o id1 B (FObj U a)
519 ∎
495 comm1 : {a b : Obj A} {f : Hom A a b} → 520 comm1 : {a b : Obj A} {f : Hom A a b} →
496 A [ A [ FMap (identityFunctor {_} {_} {_} {A}) f o 521 A [ A [ FMap (identityFunctor {_} {_} {_} {A}) f o
497 arrow (initial (In (FObj U a)) (record { obj = a ; hom = id1 B (FObj U a) })) ] 522 arrow (initial (In (FObj U a)) (record { obj = a ; hom = id1 B (FObj U a) })) ]
498 ≈ A [ arrow (initial (In (FObj U b)) (record { obj = b ; hom = id1 B (FObj U b) })) o FMap (F ○ U) f ] ] 523 ≈ A [ arrow (initial (In (FObj U b)) (record { obj = b ; hom = id1 B (FObj U b) })) o FMap (F ○ U) f ] ]
499 comm1 {a} {b} {f} = let open ≈-Reasoning A in begin 524 comm1 {a} {b} {f} = let open ≈-Reasoning A in begin
500 FMap (identityFunctor {_} {_} {_} {A}) f o 525 FMap (identityFunctor {_} {_} {_} {A}) f o
501 arrow (initial (In (FObj U a)) (record { obj = a ; hom = id1 B (FObj U a) })) 526 arrow (initial (In (FObj U a)) (record { obj = a ; hom = id1 B (FObj U a) }))
502 ≈↑⟨ unique {!!} ⟩ 527 ≈↑⟨ unique lemma-nat1 ⟩
503 arrow (initial (In (FObj U a)) (record { obj = b ; hom = B [ FMap U f o id1 B (FObj U a) ] })) 528 arrow (initial (In (FObj U a)) (record { obj = b ; hom = B [ FMap U f o id1 B (FObj U a) ] }))
504 ≈⟨ unique {!!} ⟩ 529 ≈⟨ unique lemma-nat2 ⟩
505 arrow (initial (In (FObj U b)) (record { obj = b ; hom = id1 B (FObj U b) })) o FMap (F ○ U) f 530 arrow (initial (In (FObj U b)) (record { obj = b ; hom = id1 B (FObj U b) })) o FMap (F ○ U) f
506 ∎ 531 ∎
507 532
508 nat-η : NTrans B B identityFunctor (U ○ F) 533 nat-η : NTrans B B identityFunctor (U ○ F)
509 nat-η = record { TMap = λ y → tmap-η y ; isNTrans = record { commute = comm1 } } where 534 nat-η = record { TMap = λ y → tmap-η y ; isNTrans = record { commute = comm1 } } where