--- a/src/yoneda.agda	Tue Mar 09 13:24:20 2021 +0900
+++ b/src/yoneda.agda	Tue Mar 09 14:18:06 2021 +0900
@@ -322,18 +322,20 @@
 f-u = f-unique
 
 -- faithful (injective )
-Yoneda-injective : {a b : Obj A } → {x y : Obj SetsAop} → (g h : Hom SetsAop y (FObj YonedaFunctor a))  (f : Hom A a b )
-    → SetsAop [ SetsAop [ FMap YonedaFunctor f o g ] ≈ SetsAop [ FMap YonedaFunctor f o h ] ]
-    → SetsAop [  g ≈ h ]
+Yoneda-injective : {a b b'  : Obj A } → {x y : Obj SetsAop} → (g h : Hom A b b' )  (f : Hom A a b )
+    → SetsAop [ FMap YonedaFunctor g  ≈  FMap YonedaFunctor h ]
+    → A [  g ≈ h ]
 Yoneda-injective {a} {b} {x} {y} g h f yg=yh = begin
-             TMap g _ ≈⟨ {!!}  ⟩
-             TMap h _ ∎  where
-     open ≈-Reasoning Sets
-     hoge : (x₁ : Obj A) → FObj y x₁ -- Hom Sets (FObj y x₁) (FObj (FObj YonedaFunctor a) x₁)
-     hoge x₁ = Nat2F {x₁} {y} {!!}
-     ylem11 : {x : Obj A}  (z : FObj y x) → A [ f  o TMap g _ z ] ≡ A [ f o TMap h _ z ]
-     ylem11  z = (cong (λ k → k z ) yg=yh )
+             g  ≈↑⟨ idR  ⟩
+             Nat2F (FMap YonedaFunctor g)  ≈⟨ ylem11 yg=yh ⟩ 
+             Nat2F (FMap YonedaFunctor h)  ≈⟨ idR ⟩
+             h  ∎  where
+     ylem11 : SetsAop [ FMap YonedaFunctor g  ≈  FMap YonedaFunctor h ] → A [ Nat2F (FMap YonedaFunctor g) ≈ Nat2F (FMap YonedaFunctor h) ]
+     ylem11 yg=yh with  yg=yh {b}
+     ... | eq = ≈-Reasoning.≈←≡ A ( cong (λ k →  k (id1 A b)) eq )
+     open ≈-Reasoning A
 
+-- ≈←≡ (cong (λ k → Nat2F {b} {y-obj x} k) ( ≈-≡ SetsAop yg=yh))  ⟩ 
 -- full (surjective)
 
 record CatSurjective { c₁ c₂ ℓ c₁' c₂' ℓ' : Level} ( A : Category c₁ c₂ ℓ ) ( B : Category c₁' c₂' ℓ' ) (F : Functor A B)