--- a/yoneda.agda	Sun Jul 16 14:05:18 2017 +0900
+++ b/yoneda.agda	Wed Jul 19 20:38:02 2017 +0900
@@ -311,3 +311,16 @@
 YonedaLemma21 :   { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ )  {a x : Obj A} ( f : ( FObj (FObj (YonedaFunctor A ) a) x) ) →  inv A f  ≡ a
 YonedaLemma21 A {a} {x} f = refl
 
+-- open import  Relation.Binary.HeterogeneousEquality
+-- 
+-- a1 : { c₁ : Level} {A B : Set c₁ } {a : A } { b : B } → a ≅ b → A ≡ B 
+-- a1 refl = refl
+-- 
+-- YonedaInjective :   { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ )  {a b : Obj A}
+--     → FObj (YonedaFunctor A ) a ≡ FObj (YonedaFunctor A ) b 
+--     → a ≡ b
+-- YonedaInjective A {a} {b} eq = y1 ( ≡-cong ( λ k → FObj k a) eq ) 
+--   where
+--     y1 : Hom A a a ≡ Hom A a b  → a ≡ b
+--     y1 eq = {!!}
+