--- a/yoneda.agda	Wed Aug 28 10:20:04 2013 +0900
+++ b/yoneda.agda	Wed Aug 28 11:41:17 2013 +0900
@@ -12,18 +12,23 @@
 -- Contravariant Functor : op A → Sets  ( Obj of Sets^{A^op} )
 open Functor
 
-CF : (a : Obj A) → Functor (Category.op A) Sets
+CF : (a : Obj A) → Functor A Sets
 CF a = record {
         FObj = λ b → Hom A a b
-        ; FMap =   λ {b c : Obj A } → λ ( f : Hom A c b ) → {!!} 
+        ; FMap =   λ {b c : Obj A } → λ ( f : Hom A b c ) → λ (g : Hom A a b ) →  A [ f o g ] 
         ; isFunctor = record {
-             identity = IsEquivalence.refl (IsCategory.isEquivalence  ( Category.isCategory Sets ))
-             ; distr = (IsEquivalence.refl (IsCategory.isEquivalence  ( Category.isCategory Sets )))
+             identity = identity
+             ; distr = λ {a} {b} {c} {f} {g} → distr1 a b c f g
              ; ≈-cong = cong1
         } 
     } where
-        cong1 : {b c : Obj A } { f g : Hom  A b c} → A [ f ≈ g ] →   Sets [ {!!} ≈ {!!} ] 
-        cong1 eq = _≡_.refl
+        identity : {b : Obj A} → Sets [ (λ (g : Hom A a b ) → A [ id1 A b o g ]) ≈ ( λ g → g ) ]
+        identity = let open ≈-Reasoning A in {!!}
+        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 = {!!}
+        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 = {!!}