# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1499311374 -32400
# Node ID 0d029674eb5921c5fb0a7cc7519677dc6589790b
# Parent  18431b63893b2c68f3ef483d9ebfb9ae9b04c259
on going ...

diff -r 18431b63893b -r 0d029674eb59 freyd2.agda
--- 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 
              ∎