--- a/yoneda.agda	Sun Sep 01 15:21:53 2013 +0900
+++ b/yoneda.agda	Sun Sep 01 16:14:08 2013 +0900
@@ -298,37 +298,20 @@
 
 --  F2Nat is bijection so FMap YonedaFunctor also ( using functional extensionality )
 
---  Full embedding of Yoneda Functor requires injective on Object, that is
+--  Full embedding of Yoneda Functor requires injective on Object, 
+--
+-- But we cannot prove like this
 --     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
-
--- dom-equivalence1 : {a b : Obj A} → {f : Hom A a a} -> {g : Hom A a b} → A [ f ≈ g ] → Category.dom A f ≡ Category.dom A g
--- dom-equivalence1 eq = ?
-
-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
+--     YondaLemma2 : {a b x : Obj A }  → (FObj (FObj YonedaFunctor a) x)  ≡ (FObj (FObj YonedaFunctor b  ) x)  →     
+--         a ≡ b 
+--     YondaLemma2 {a} {b} eq  = {!!}
+--
+-- Instead we prove 
+--     inv ( FObj YonedaFunctor a )  ≡ a
 
--- 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  = {!!}
-
-inv :  {a x : Obj A} ( f : FObj (FObj YonedaFunctor a) x ) →  Obj A
-inv {a} {x} f =  Category.cod A f
+inv :  {a x : Obj A} ( f : FObj (FObj YonedaFunctor a) x)  →  Obj A
+inv {a} f =  Category.cod A f
 
---YondaLemma2 : {a b : Obj A }  → (λ x → FObj (FObj YonedaFunctor a) x)  ≡ (λ x → FObj (FObj YonedaFunctor b  ) x)  →     
---         a ≡ b 
---YondaLemma2 {a} {b} eq  = ≡-cong inv ?
-
-inv-yobj :  {a x : Obj A} →  Hom A a x → Obj A
-inv-yobj {a} {x} _ = a
-
-YonedaLemma21 :  (a x : Obj A) { f : ( FObj (FObj YonedaFunctor a) x) } →  Category.cod A f  ≡ a
+YonedaLemma21 :  (a x : Obj A) { f : ( FObj (FObj YonedaFunctor a) x) } →  inv f  ≡ a
 YonedaLemma21 a x {f} = refl
 
----    f ≡  g     f x  ≡ g x
-
--- I cannot prove this, please help.