--- a/yoneda.agda	Wed Aug 28 11:41:17 2013 +0900
+++ b/yoneda.agda	Wed Aug 28 13:26:01 2013 +0900
@@ -12,6 +12,14 @@
 -- Contravariant Functor : op A → Sets  ( Obj of Sets^{A^op} )
 open Functor
 
+-- A is Locally small
+postulate ≈-≡ : {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 )
+postulate extensionality : Relation.Binary.PropositionalEquality.Extensionality c₂ c₂
+
+
 CF : (a : Obj A) → Functor A Sets
 CF a = record {
         FObj = λ b → Hom A a b
@@ -22,13 +30,24 @@
              ; ≈-cong = cong1
         } 
     } where
+        lemma-CF1 : {b : Obj A } → (x : Hom A a b) → A [ id1 A b o x ] ≡ x
+        lemma-CF1 {b} x = let open ≈-Reasoning (A) in ≈-≡ idL
         identity : {b : Obj A} → Sets [ (λ (g : Hom A a b ) → A [ id1 A b o g ]) ≈ ( λ g → g ) ]
-        identity = let open ≈-Reasoning A in {!!}
+        identity {b} = extensionality lemma-CF1
+        lemma-CF2 : (a₁ b c : Obj A) (f : Hom A a₁ b) (g : Hom A b c) → (x : Hom A a a₁ )→ A [ A [ g o f ] o x ] ≡ (Sets [ _[_o_] A g o _[_o_] A f ]) x
+        lemma-CF2 a₁ b c f g x = let open ≈-Reasoning (A) in ≈-≡ ( begin
+               A [ A [ g o f ] o x ]
+             ≈↑⟨ assoc ⟩
+               A [ g o A [ f o x ] ] 
+             ≈⟨⟩
+               ( λ x →  A [ g o x  ]  ) ( ( λ x → A [ f o x ] ) x )
+             ∎ )
         distr1 :   (a₁ b c : Obj A) (f : Hom A a₁ b) (g : Hom A b c) →
                 Sets [ (λ g₁ → A [ A [ g o f ] o g₁ ]) ≈ Sets [ (λ g₁ → A [ g o g₁ ]) o (λ g₁ → A [ f o g₁ ]) ] ]
-        distr1 a b c f g = {!!}
+        distr1 a b c f g = extensionality ( λ x → lemma-CF2 a b c f g x )
         cong1 :  {A₁ B : Obj A} {f g : Hom A A₁ B} → A [ f ≈ g ] → Sets [ (λ g₁ → A [ f o g₁ ]) ≈ (λ g₁ → A [ g o g₁ ]) ]
-        cong1 eq = {!!}
+        cong1 eq = extensionality ( λ x → ( ≈-≡ (  
+                 (IsCategory.o-resp-≈  ( Category.isCategory A )) ( IsEquivalence.refl (IsCategory.isEquivalence  ( Category.isCategory A ))) eq )))