# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1377859600 -32400
# Node ID 3271d2d04b17b293dadc9b4b67030ea592dc2712
# Parent  4e6f080f01073f34db40f9759746d5ebd08ffb1a
F2Nat→Nat2F done

diff -r 4e6f080f0107 -r 3271d2d04b17 yoneda.agda
--- a/yoneda.agda	Fri Aug 30 16:49:28 2013 +0900
+++ b/yoneda.agda	Fri Aug 30 19:46:40 2013 +0900
@@ -239,8 +239,33 @@
 Nat2F {a} {F} ha =  ( TMap ha a ) (id1 A a)
 
 F2Nat→Nat2F : {a : Obj A } → {F : Obj SetsAop} → (fa : FObj F a) →  Nat2F {a} {F} (F2Nat {a} {F} fa) ≡ fa 
-F2Nat→Nat2F  = {!!}
+-- FMap F (Category.Category.Id A) fa ≡ fa
+F2Nat→Nat2F {a} {F} fa = let open ≈-Reasoning (Sets) in cong ( λ f → f fa ) (
+             begin
+               ( FMap F (id1 A _ )) 
+             ≈⟨ IsFunctor.identity (isFunctor F)    ⟩
+                id1 Sets (FObj F a)
+             ∎ )
+
+open  import  Relation.Binary.PropositionalEquality
+
+postulate extensionality2 : Relation.Binary.PropositionalEquality.Extensionality  c₁ c₂ 
+postulate extensionality3 : Relation.Binary.PropositionalEquality.Extensionality  c₂ c₂
 
 Nat2F→F2Nat : {a : Obj A } → {F : Obj SetsAop} → (ha : Hom SetsAop (CF {a}) F) →  SetsAop [ F2Nat {a} {F} (Nat2F {a} {F} ha) ≈ ha ]
-Nat2F→F2Nat = {!!}
+-- (λ b g → FMap F g (TMap ha a (Category.Category.Id A))) ≡ TMap ha
+Nat2F→F2Nat {a} {F} ha = let open ≡-Reasoning in
+             begin
+                ( λ (b : Obj A ) → λ (g : Hom A b a ) → FMap F g (TMap ha a (Category.Category.Id A))  )
+             ≡⟨ extensionality2 ( λ b → extensionality3 (λ g → lemma1 {a} {F} ha b g )) ⟩
+                TMap ha   
+             ∎ where
+               lemma1 :  {a : Obj A } → {F : Obj SetsAop} → (ha : Hom SetsAop (CF {a}) F) →  (b : Obj A ) → (g : Hom A b a ) → 
+                            FMap F g (TMap ha a (Category.Category.Id A)) ≡  TMap ha b g
+               lemma1 {a} {F} ha b g =  ?
 
+--     F :  op A → Sets
+--     ha : NTrans (op A) Sets (CF {a}) F
+--                FMap (CF {a}) g  o TMap ha a ≈   TMap ha b  o FMap F g
+
+