# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1377652804 -32400
# Node ID f017d892d8c3e85e66042415572aea65c1e1295d
# Parent  6626a7cd9129ea5cac4d8142db60a9ee05d82588
fix

diff -r 6626a7cd9129 -r f017d892d8c3 yoneda.agda
--- a/yoneda.agda	Tue Aug 27 23:35:05 2013 +0900
+++ b/yoneda.agda	Wed Aug 28 10:20:04 2013 +0900
@@ -5,23 +5,25 @@
 
 open import HomReasoning
 open import cat-utility
-open import Category.Cat
+open import Relation.Binary.Core
+open import Relation.Binary
+
 
 -- Contravariant Functor : op A → Sets  ( Obj of Sets^{A^op} )
+open Functor
 
-CF : (a : Obj A) → Functor (op A) Sets
+CF : (a : Obj A) → Functor (Category.op A) Sets
 CF a = record {
         FObj = λ b → Hom A a b
-        ; FMap = {b c : Obj A } λ (f : Hom A b c) → (Hom A c a) → (Hom A b a)
+        ; FMap =   λ {b c : Obj A } → λ ( f : Hom A c b ) → {!!} 
         ; isFunctor = record {
              identity = IsEquivalence.refl (IsCategory.isEquivalence  ( Category.isCategory Sets ))
              ; distr = (IsEquivalence.refl (IsCategory.isEquivalence  ( Category.isCategory Sets )))
              ; ≈-cong = cong1
         } 
     } where
-        cong1 : {ℓ′ : Level} → {b c : Set ℓ′} { f g : Hom (Sets {ℓ′}) b c} → 
-                   Sets [ f ≈ g ] → Sets [ f ≈  g ]
-        cong1 _≡_.refl = _≡_.refl
+        cong1 : {b c : Obj A } { f g : Hom  A b c} → A [ f ≈ g ] →   Sets [ {!!} ≈ {!!} ] 
+        cong1 eq = _≡_.refl
 
-open Functor
 
+