# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1374668367 -32400
# Node ID c6f66c21230cf1022595eb97542b0140af50c19c
# Parent  83ff8d48fdca798507e0e9bc28a97150b7c7afa6
nat and functor comp

diff -r 83ff8d48fdca -r c6f66c21230c cat-utility.agda
--- a/cat-utility.agda	Wed Jul 24 20:47:28 2013 +0900
+++ b/cat-utility.agda	Wed Jul 24 21:19:27 2013 +0900
@@ -98,9 +98,9 @@
                (FMap F (TMap n b )) o  (FMap F (FMap G f))
             ∎
 
-Nat*Functor :  {c₁ c₂ ℓ c₁' c₂' ℓ' c₁'' c₂'' ℓ'' : Level} (A : Category c₁ c₂ ℓ) (B : Category c₁' c₂' ℓ') (C : Category c₁'' c₂'' ℓ'')
-    (F : Functor A B) -> { G H : Functor B C } -> ( n : NTrans B C G H ) -> NTrans A C (G ○  F) (H ○ F)
-Nat*Functor A B C F {G} {H} n = record {
+Nat*Functor :  {c₁ c₂ ℓ c₁' c₂' ℓ' c₁'' c₂'' ℓ'' : Level} (A : Category c₁ c₂ ℓ) {B : Category c₁' c₂' ℓ'} (C : Category c₁'' c₂'' ℓ'')
+    { G H : Functor B C } -> ( n : NTrans B C G H ) -> (F : Functor A B) -> NTrans A C (G ○  F) (H ○ F)
+Nat*Functor A {B} C {G} {H} n F = record {
        TMap  = \a -> TMap n (FObj F a)
        ; isNTrans = record {
             naturality = naturality
@@ -108,9 +108,7 @@
     } where
          naturality : {a b : Obj A} {f : Hom A a b} 
             → C [ C [ ( FMap H (FMap F f )) o  ( TMap n (FObj F a)) ]  ≈ C [ (TMap n (FObj F b )) o  (FMap G (FMap F f))  ] ]
-         naturality  {a} {b} {f}  = {!!}
-
-
+         naturality  {a} {b} {f}  =  IsNTrans.naturality ( isNTrans n) 
 
 record Kleisli  { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ )
                  ( T : Functor A A )
diff -r 83ff8d48fdca -r c6f66c21230c nat.agda
--- a/nat.agda	Wed Jul 24 20:47:28 2013 +0900
+++ b/nat.agda	Wed Jul 24 21:19:27 2013 +0900
@@ -271,4 +271,6 @@
                     unity1 = {!!};
                     unity2 = {!!}
               }
-      } 
+      } where
+         UεF : {!!}
+         UεF = Functor*Nat B A U ( Nat*Functor ? {?} ? ε F)