--- a/yoneda.agda	Sun Mar 05 11:14:32 2017 +0900
+++ b/yoneda.agda	Mon Mar 06 15:45:51 2017 +0900
@@ -93,7 +93,7 @@
 
 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 )
-postulate extensionality : { c₁ c₂ ℓ : Level} { A : Category c₁ c₂ ℓ } → Relation.Binary.PropositionalEquality.Extensionality c₂ c₂
+postulate extensionality : { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) → Relation.Binary.PropositionalEquality.Extensionality c₂ c₂
 
 
 ----
@@ -109,9 +109,9 @@
         FObj = λ b → Hom (Category.op A) a b  ;
         FMap =   λ {b c : Obj A } → λ ( f : Hom  A c b ) → λ (g : Hom  A b a ) →  (Category.op A) [ f o g ] ;
         isFunctor = record {
-             identity =  λ {b} → extensionality {_} {_} {_} {A} ( λ x → lemma-y-obj1 {b} x ) ;
-             distr = λ {a} {b} {c} {f} {g} → extensionality {_} {_} {_} {A} ( λ x → lemma-y-obj2 a b c f g x ) ;
-             ≈-cong = λ eq → extensionality {_} {_} {_} {A} ( λ x →  lemma-y-obj3 x eq ) 
+             identity =  λ {b} → extensionality A ( λ x → lemma-y-obj1 {b} x ) ;
+             distr = λ {a} {b} {c} {f} {g} → extensionality A ( λ x → lemma-y-obj2 a b c f g x ) ;
+             ≈-cong = λ eq → extensionality A ( λ x →  lemma-y-obj3 x eq ) 
         } 
     }  where
         lemma-y-obj1 : {b : Obj A } → (x : Hom A b a) →  (Category.op A) [ id1 A b o x ] ≡ x
@@ -148,7 +148,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 ] ]
@@ -175,7 +175,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 ]
@@ -183,7 +183,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
@@ -191,7 +191,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 ] ]
@@ -224,7 +224,7 @@
                 Sets [ FMap F f o F2Natmap A {a} {F} {x} a₁ ]
              ≈⟨⟩
                 Sets [ FMap F f o (λ ( g : Hom A a₁ a ) → ( FMap F g ) x) ]
-             ≈⟨ extensionality {_} {_} {_} {A}  ( λ (g : Hom A  a₁ a) → commute1 {a₁} {b} {f} g ) ⟩
+             ≈⟨ extensionality A  ( λ (g : Hom A  a₁ a) → commute1 {a₁} {b} {f} g ) ⟩
                 Sets [  (λ ( g : Hom A b a ) → ( FMap F g ) x) o FMap (y-obj A a) f ] 
              ≈⟨⟩
                 Sets [ F2Natmap A {a} {F} {x} b o FMap (y-obj A a) f ] 
@@ -268,7 +268,7 @@
                 TMap (F2Nat A {a} {F} (Nat2F A {a} {F} ha)) b
              ≡⟨⟩
                 (λ g → FMap F g (TMap ha a (Category.Category.Id A)))
-             ≡⟨  extensionality {_} {_} {_} {A}  (λ g → (
+             ≡⟨  extensionality A  (λ g → (
                 begin
                     FMap F g (TMap ha a (Category.Category.Id A)) 
                 ≡⟨  ≡-cong (λ f → f (Category.Category.Id A)) (IsNTrans.commute (isNTrans ha)) ⟩