Mercurial > hg > Members > kono > Proof > category

changeset 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
files freyd2.agda
diffstat 1 files changed, 27 insertions(+), 2 deletions(-) [+]
line wrap: on
line diff
--- a/freyd2.agda	Thu Jul 06 09:54:56 2017 +0900
+++ b/freyd2.agda	Thu Jul 06 12:22:54 2017 +0900
@@ -492,6 +492,31 @@
    nat-ε  = record {
          TMap = λ x → arrow ( solution (id1 B (FObj U x)))
          ; isNTrans = record { commute = comm1 } } where
+        lemma-nat1 : {a b : Obj A} {f : Hom A a b} →
+           B [ B [ FMap U (A [ FMap (identityFunctor {_} {_} {_} {A}) f o arrow (initial (In (FObj U a))
+                  (record { obj = a ; hom = id1 B (FObj U a) })) ] ) o tmap-η (FObj U a) ]
+           ≈ B [ FMap U f o id1 B (FObj U a) ] ]
+        lemma-nat1 {a} {b} {f} = let open ≈-Reasoning B in begin
+                FMap U (A [ FMap (identityFunctor {_} {_} {_} {A}) f o arrow (initial (In (FObj U a))
+                  (record { obj = a ; hom = id1 B (FObj U a) })) ] ) o tmap-η (FObj U a) 
+             ≈⟨ car (distr U) ⟩
+                 ( FMap U (FMap (identityFunctor {_} {_} {_} {A}) f) o FMap U (arrow (initial (In (FObj U a))
+                    (record { obj = a ; hom = id1 B (FObj U a) })))) o (tmap-η (FObj U a))
+             ≈⟨ {!!} ⟩
+                FMap U f 
+             ≈↑⟨ idR ⟩
+                FMap U f o id1 B (FObj U a) 
+             ∎  
+        lemma-nat2 : {a b : Obj A} {f : Hom A a b} →
+             B [ B [ FMap U (A [ arrow (initial (In (FObj U b))
+          (record { obj = b ; hom = id1 B (FObj U b) })) o FMap (F ○ U) f ] ) o tmap-η (FObj U a) ]
+           ≈ B [ FMap U f o id1 B (FObj U a) ] ]
+        lemma-nat2 {a} {b} {f} = let open ≈-Reasoning B in begin
+                 FMap U (A [ arrow (initial (In (FObj U b))
+                  (record { obj = b ; hom = id1 B (FObj U b) })) o FMap (F ○ U) f ] ) o tmap-η (FObj U a) 
+             ≈⟨ {!!} ⟩
+                 FMap U f o id1 B (FObj U a) 
+             ∎  
         comm1 : {a b : Obj A} {f : Hom A a b} →
                 A [ A [ FMap (identityFunctor {_} {_} {_} {A}) f o
                     arrow (initial (In (FObj U a)) (record { obj = a ; hom = id1 B (FObj U a) })) ]
@@ -499,9 +524,9 @@
         comm1 {a} {b} {f} = let open ≈-Reasoning A in begin
                FMap (identityFunctor {_} {_} {_} {A}) f o
                     arrow (initial (In (FObj U a)) (record { obj = a ; hom = id1 B (FObj U a) })) 
-             ≈↑⟨ unique {!!} ⟩
+             ≈↑⟨ unique lemma-nat1 ⟩
                arrow (initial (In (FObj U a)) (record { obj = b ; hom = B [ FMap U f o id1 B (FObj U a) ] })) 
-             ≈⟨ unique {!!} ⟩
+             ≈⟨ unique lemma-nat2 ⟩
                arrow (initial (In (FObj U b)) (record { obj = b ; hom = id1 B (FObj U b) })) o FMap (F ○ U) f 
              ∎