Mercurial > hg > Members > kono > Proof > category

changeset 182:346e8eb35ec3

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
contravariant continue ...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Wed, 28 Aug 2013 17:00:49 +0900
parents b58453d90db6
children ea6fc610b480
files yoneda.agda
diffstat 1 files changed, 15 insertions(+), 3 deletions(-) [+]
line wrap: on
line diff
--- 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