--- a/yoneda.agda	Thu Aug 29 16:07:45 2013 +0900
+++ b/yoneda.agda	Fri Aug 30 15:28:57 2013 +0900
@@ -192,7 +192,7 @@
              ∎
           ) )  )
         distr1 : {a b c : Obj A} {f : Hom A a b} {g : Hom A b c} → SetsAop [ y-nat (A [ g o f ]) ≈ SetsAop [ y-nat g o y-nat f ] ]
-        distr1 {a} {b} {c} {f} {g} = let open ≈-Reasoning (A) in -- (λ x g₁ → (A [  (A [ g o f]  o g₁ ]) ≡ (λ x x₁ → A [  g o A [ f o x₁ ] ] )
+        distr1 {a} {b} {c} {f} {g} = let open ≈-Reasoning (A) in -- (λ x g₁ → (A [  (A [ g o f]  o g₁ ]))) ≡ (λ x x₁ → A [  g o A [ f o x₁ ] ] )
            extensionality1 ( λ x → extensionality (
              λ h →  ≈-≡  ( begin
                 A [ A [ g o f ]  o h ]
@@ -207,16 +207,19 @@
 --  F : A → Sets  ∈ Obj SetsAop
 --
 --  F(a) ⇔ Nat(h_a,F)
---
+--      x ∈ F(a) , (g : Hom A b a)  → ( FMap F g ) x
 ------
 
-F2Natmap :  {a : Obj A} → {F : Obj SetsAop} → (x : Obj (Category.op A)) → Hom Sets (FObj (CF {a}) x) (FObj F x)
-F2Natmap = {!!}
+F2Natmap :  {a : Obj A} → {F : Obj SetsAop} → {x : FObj F a} → (b : Obj (Category.op A)) → Hom Sets (FObj (CF {a}) b) (FObj F b)
+F2Natmap {a} {F} {x} b = λ ( g : Hom A b a ) → ( FMap F g ) x
 
 F2Nat : {a : Obj A} → {F : Obj SetsAop} →  FObj F a  → Hom SetsAop (CF {a}) F
-F2Nat {a} {F} x = record { TMap = F2Natmap {a} {F} ; isNTrans = isNTrans1 {a} } where
-   isNTrans1 : {a : Obj A } → IsNTrans (Category.op A) (Sets {c₂}) (CF {a}) F (F2Natmap {a} {F})
-   isNTrans1 {a} = record { commute = {!!}  }
+F2Nat {a} {F} x = record { TMap = F2Natmap {a} {F} {x} ; isNTrans = isNTrans1 } where
+   commute : {a₁ b : Obj (Category.op A)} {f : Hom (Category.op A) a₁ b} → 
+        Sets [ Sets [ FMap F f o F2Natmap {a} {F} {x} a₁ ] ≈ Sets [ F2Natmap {a} {F} {x} b o FMap CF f ] ]
+   commute {a₁} {b} {f} =  extensionality ( λ (g : Hom A a₁ a ) →　?  )
+   isNTrans1 : IsNTrans (Category.op A) (Sets {c₂}) (CF {a}) F (F2Natmap {a} {F})
+   isNTrans1 = record { commute = λ {a₁ b f}  →  commute {a₁} {b} {f} } 
 
 
 Nat2F : {a : Obj A} → {F : Obj SetsAop} →  Hom SetsAop (CF {a}) F  → FObj F a