# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1377676849 -32400
# Node ID 346e8eb35ec323a01a5db6dd9e8bf1d4ddc79d75
# Parent  b58453d90db6ffdb9dfb0e2b39fa2fed916bd31a
contravariant continue ...

diff -r b58453d90db6 -r 346e8eb35ec3 yoneda.agda
--- a/yoneda.agda	Wed Aug 28 13:26:01 2013 +0900
+++ b/yoneda.agda	Wed Aug 28 17:00:49 2013 +0900
@@ -20,8 +20,8 @@
 postulate extensionality : Relation.Binary.PropositionalEquality.Extensionality c₂ c₂
 
 
-CF : (a : Obj A) → Functor A Sets
-CF a = record {
+CF' : (a : Obj A) → Functor A Sets
+CF' a = record {
         FObj = λ b → Hom A a b
         ; FMap =   λ {b c : Obj A } → λ ( f : Hom A b c ) → λ (g : Hom A a b ) →  A [ f o g ] 
         ; isFunctor = record {
@@ -49,5 +49,17 @@
         cong1 eq = extensionality ( λ x → ( ≈-≡ (  
                  (IsCategory.o-resp-≈  ( Category.isCategory A )) ( IsEquivalence.refl (IsCategory.isEquivalence  ( Category.isCategory A ))) eq )))
 
+open import Function
 
-
+CF : (a : Obj A) → Functor (Category.op A) Sets
+CF a = record {
+        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 ( λ x → lemma-CF1 {b} x )
+             ; distr = λ {a} {b} {c} {f} {g} → {!!}
+             ; ≈-cong = {!!}
+        } 
+    }  where
+        lemma-CF1 : {b : Obj A } → (x : Hom A b a) →  (Category.op A) [ id1 A b o x ] ≡ x
+        lemma-CF1 {b} x = let open ≈-Reasoning (Category.op A) in ≈-≡ idL