--- a/yoneda.agda	Fri Aug 30 21:46:18 2013 +0900
+++ b/yoneda.agda	Sat Aug 31 01:23:50 2013 +0900
@@ -171,6 +171,7 @@
              identity =  identity
              ; distr = distr1
              ; ≈-cong = ≈-cong
+
         } 
   } where
         ≈-cong : {a b : Obj A} {f g : Hom A a b} → A [ f ≈ g ] → SetsAop [ y-nat f ≈ y-nat g ]
@@ -274,5 +275,32 @@
                 TMap ha   
              ∎ 
 
+-- Yoneda's Lemma
+--    full and faithfull
+--    that is FMapp Yoneda is injective and surjective
 
+--  λ b g → (A Category.o f₁) g
+YondaLemma1 : {a a' : Obj A } {f : FObj (FObj YonedaFunctor a) a' } → SetsAop [ F2Nat {a'} {FObj YonedaFunctor a} f ≈ FMap YonedaFunctor f ]
+YondaLemma1 {a} {a'} {f} = refl
 
+--  F2Nat is bijection so FMap YonedaFunctor also ( using functional extensionality )
+
+--  Full embedding requires injective on Object, that is
+--     FObj YonedaFunctor a   ≡ FObj YonedaFunctor b → a  ≡ b
+
+dom-equivalence : {a b : Obj A} → {f g : Hom A a b} → A [ f ≈ g ] → Category.dom A f ≡ Category.dom A g
+dom-equivalence eq = refl
+
+equive-elm : ∀{n} {a b : Set n} → (f : a ) → a ≡ b → b
+equive-elm f refl  = f
+
+equive-arrow : {a b : Obj A } → (f : Hom A a b ) → Hom A a b  ≡ Hom A a a →　Hom A a a
+equive-arrow f eq  = equive-elm f eq
+
+-- equive-hom : {a b : Obj A } → {f : Hom A a b } → Hom A a b  ≡ Hom A a a → a ≡ b 
+-- equive-hom  {a} {b} {f} eq  = {!!}
+
+-- YondaLemma2 : {a b : Obj A }  → (λ x → FObj (FObj YonedaFunctor a) x)  ≡ (λ x → FObj (FObj YonedaFunctor b  ) x)  →  
+--        {f : Hom A a b } → a ≡ b 
+-- YondaLemma2 {a} {b} eq  {f}  = {!!} eq
+