--- a/yoneda.agda	Sat Jul 13 00:18:17 2019 +0900
+++ b/yoneda.agda	Sun Mar 15 14:26:39 2020 +0900
@@ -91,7 +91,7 @@
          }
 
 -- A is Locally small
-postulate ≈-≡ :  { c₁ c₂ ℓ : Level} { A : Category c₁ c₂ ℓ }  {a b : Obj A } { x y : Hom A a b } →  (x≈y : A [ x ≈ y  ]) → x ≡ y
+postulate ≡←≈ :  { c₁ c₂ ℓ : Level} { A : Category c₁ c₂ ℓ }  {a b : Obj A } { x y : Hom A a b } →  (x≈y : A [ x ≈ y  ]) → x ≡ y
 
 import Relation.Binary.PropositionalEquality
 -- Extensionality a b = {A : Set a} {B : A → Set b} {f g : (x : A) → B x} → (∀ x → f x ≡ g x) → f ≡ g → ( λ x → f x ≡ λ x → g x )
@@ -117,10 +117,10 @@
         } 
     }  where
         lemma-y-obj1 : {b : Obj A } → (x : Hom A b a) →  (Category.op A) [ id1 A b o x ] ≡ x
-        lemma-y-obj1 {b} x = let open ≈-Reasoning (Category.op A) in ≈-≡ {_} {_} {_} {A} idL
+        lemma-y-obj1 {b} x = let open ≈-Reasoning (Category.op A) in ≡←≈ {_} {_} {_} {A} idL
         lemma-y-obj2 :  (a₁ b c : Obj A) (f : Hom A b a₁) (g : Hom A c b ) → (x : Hom A a₁ a )→ 
                Category.op A [ Category.op A [ g o f ] o x ] ≡ (Sets [ _[_o_] (Category.op A) g o _[_o_] (Category.op A) f ]) x
-        lemma-y-obj2 a₁ b c f g x = let open ≈-Reasoning (Category.op A) in ≈-≡ {_} {_} {_} {A} ( begin
+        lemma-y-obj2 a₁ b c f g x = let open ≈-Reasoning (Category.op A) in ≡←≈ {_} {_} {_} {A} ( begin
                Category.op A [ Category.op A [ g o f ] o x ]
              ≈↑⟨ assoc ⟩
                Category.op A [ g o Category.op A [ f o x ] ]
@@ -128,7 +128,7 @@
                ( λ x →  Category.op A [ g o x  ]  ) ( ( λ x → Category.op A [ f o x ] ) x )
              ∎ )
         lemma-y-obj3 :  {b c : Obj A} {f g : Hom A c b } → (x : Hom A b a ) → A [ f ≈ g ] →  Category.op A [ f o x ] ≡ Category.op A [ g o x ]
-        lemma-y-obj3 {_} {_} {f} {g} x eq =  let open ≈-Reasoning (Category.op A) in ≈-≡ {_} {_} {_} {A}   ( begin
+        lemma-y-obj3 {_} {_} {f} {g} x eq =  let open ≈-Reasoning (Category.op A) in ≡←≈ {_} {_} {_} {A}   ( begin
                 Category.op A [ f o x ]
              ≈⟨ resp refl-hom eq ⟩
                 Category.op A [ g o x ]
@@ -150,7 +150,7 @@
    lemma-y-obj4 : {a₁ b₁ : Obj (Category.op A)} {g : Hom (Category.op A) a₁ b₁} → {a b : Obj A } → (f : Hom A a b ) →
         Sets [ Sets [ FMap (y-obj A b) g o y-tmap A a b f a₁ ] ≈
         Sets [ y-tmap A a b f b₁ o FMap (y-obj A a) g ] ]
-   lemma-y-obj4 {a₁} {b₁} {g} {a} {b} f = let open ≈-Reasoning A in extensionality A ( λ x →  ≈-≡ {_} {_} {_} {A} ( begin
+   lemma-y-obj4 {a₁} {b₁} {g} {a} {b} f = let open ≈-Reasoning A in extensionality A ( λ x →  ≡←≈ {_} {_} {_} {A} ( begin
                 A [ A [ f o x ] o g ]
              ≈↑⟨ assoc ⟩
                 A [ f o A [ x  o g ] ]
@@ -177,7 +177,7 @@
   } where
         ≈-cong : {a b : Obj A} {f g : Hom A a b} → A [ f ≈ g ] → SetsAop A [ y-map A f ≈ y-map A g ]
         ≈-cong {a} {b} {f} {g} eq  =  let open ≈-Reasoning (A) in  -- (λ x g₁ → A [ f o g₁ ] ) ≡ (λ x g₁ → A [  g o  g₁ ] )
-             extensionality A ( λ h → ≈-≡ {_} {_} {_} {A}  ( begin
+             extensionality A ( λ h → ≡←≈ {_} {_} {_} {A}  ( begin
                 A [ f o h ]
              ≈⟨ resp refl-hom eq ⟩
                 A [ g o h ]
@@ -185,7 +185,7 @@
           ) ) 
         identity : {a : Obj A} → SetsAop A [ y-map A (id1 A a) ≈ id1 (SetsAop A) (y-obj A a )  ]
         identity  {a} =  let open ≈-Reasoning (A) in -- (λ x g → A [ id1 A a o g ] ) ≡ (λ a₁ x → x)
-             extensionality A ( λ g →  ≈-≡ {_} {_} {_} {A}  ( begin
+             extensionality A ( λ g →  ≡←≈ {_} {_} {_} {A}  ( begin
                 A [ id1 A a o g ] 
              ≈⟨ idL ⟩
                 g
@@ -193,7 +193,7 @@
           ) )  
         distr1 : {a b c : Obj A} {f : Hom A a b} {g : Hom A b c} → SetsAop A [ y-map A (A [ g o f ]) ≈ SetsAop A [ y-map A g o y-map A f ] ]
         distr1 {a} {b} {c} {f} {g} = let open ≈-Reasoning (A) in -- (λ x g₁ → (A [  (A [ g o f]  o g₁ ]))) ≡ (λ x x₁ → A [  g o A [ f o x₁ ] ] )
-           extensionality A ( λ h →  ≈-≡ {_} {_} {_} {A}  ( begin
+           extensionality A ( λ h →  ≡←≈ {_} {_} {_} {A}  ( begin
                 A [ A [ g o f ]  o h ]
              ≈↑⟨ assoc  ⟩
                 A [  g o A [ f o h ] ]
@@ -277,7 +277,7 @@
                     TMap ha b (FMap (y-obj A a) g (Category.Category.Id A))
                 ≡⟨⟩
                     TMap ha b ( (A Category.o Category.Category.Id A) g )
-                ≡⟨  ≡-cong ( TMap ha b ) ( ≈-≡ {_} {_} {_} {A} (IsCategory.identityL  ( Category.isCategory A ))) ⟩
+                ≡⟨  ≡-cong ( TMap ha b ) ( ≡←≈ {_} {_} {_} {A} (IsCategory.identityL  ( Category.isCategory A ))) ⟩
                     TMap ha b g
                 ∎ 
              )) ⟩