--- a/src/CCCGraph.agda	Sat Mar 06 19:11:01 2021 +0900
+++ b/src/CCCGraph.agda	Sat Mar 06 23:02:33 2021 +0900
@@ -95,6 +95,14 @@
                     Sets [ f ≈ f' ] → Sets [ f * ≈ f' * ]
                 *-cong refl = refl
 
+--             ○ b
+--       b -----------→ 1
+--       |              |
+--     m |              | ⊤
+--       ↓    char m    ↓
+--       a -----------→ Ω
+--             h
+
 data II  {c : Level } : Set c where
      true : II
      false : II

--- a/src/yoneda.agda	Sat Mar 06 19:11:01 2021 +0900
+++ b/src/yoneda.agda	Sat Mar 06 23:02:33 2021 +0900
@@ -311,6 +311,14 @@
 -- f ∈ FMap (FObj YonedaFunctor a') a
 --
 
+--    g       f
+-- b --→ a ------→ a'      
+--       |         |
+--       |         |
+--       ↓         ↓
+--     H a ------→ H a'
+--          H f
+--
 _^ : {a a' b : Obj A } → (f : Hom A a  a' )  → Hom A b a →  Hom A b a' 
 _^ {a} {a'} {b} f g = (FMap (FObj YonedaFunctor a') g) f
 
@@ -323,11 +331,32 @@
 
 postulate
         eqObj0 : { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) → {a a' b b' : Obj A}  → Hom A a b ≡ Hom A a' b' → a ≡ a'
-        eqObj1 : { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) → {a a' b b' : Obj A}  → Hom A a b ≡ Hom A a' b' → b ≡ b'
         eqHom0 : {a b c : Obj A } {f f' : Hom A b c } {g g' : Hom A a b } → A [ f o g ] ≡ A [ f' o g' ] → f ≡ f'
         eqHom1 : {a b c : Obj A } {f f' : Hom A b c } {g g' : Hom A a b } → A [ f o g ] ≡ A [ f' o g' ] → g ≡ g'
         -- eqTMap : { y b : Obj A} { x z : Obj Sets} → {g h : NTrans (Category.op A) Sets (y-obj b) ? } {w : {!!} } → TMap g x {!!} ≡ TMap h x w → g ≡ h
 
+open import Category.Cat
+
+
+≃→a=a : {c₁ c₂ ℓ : Level}  (B : Category c₁ c₂ ℓ ) → {a b a' b' : Obj B }
+      → ( f : Hom B a b )
+      → ( g : Hom B a' b' )
+      → [_]_~_ B f g → a ≡ a'
+≃→a=a B f g (refl eqv) = refl
+
+≃→b=b : {c₁ c₂ ℓ : Level}  (B : Category c₁ c₂ ℓ ) → {a b a' b' : Obj B }
+      → ( f : Hom B a b )
+      → ( g : Hom B a' b' )
+      → [_]_~_ B f g → b ≡ b'
+≃→b=b B f g (refl eqv) = refl
+
+open import  Relation.Binary.HeterogeneousEquality as HE using (_≅_) 
+
+eqObj1 : { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) → {a b  : Obj A}  → Hom A a a ≡ Hom A a b → a ≡ b
+eqObj1 A {a} {b}  eq = lem (subst (λ k → k) eq (id1 A a)) eq where
+      lem : (f : Hom A a b ) → f ≅ id1 A a →  Hom A a a ≡ Hom A a b →  a ≡ b
+      lem _ HE.refl refl = refl 
+
 -- full (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 ] ]
@@ -358,8 +387,6 @@
      ylem10 : {y : Obj A} → (λ z  → TMap g y (A [ f o z ])) ≡ (λ z → TMap h y (A [ f o z ] ))
      ylem10 = yg=yh
 
-open import  Relation.Binary.HeterogeneousEquality as HE using (_≅_) 
-
 Yoneda-full-embed : {a b : Obj A } → FObj YonedaFunctor a ≡ FObj YonedaFunctor b → a ≡ b
 Yoneda-full-embed {a} {b} eq = eqObj1 A ylem1 where
      ylem1 : Hom A a a ≡ Hom A a b