Mercurial > hg > Members > kono > Proof > category

changeset 184:d2d749318bee

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
oeration
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Wed, 28 Aug 2013 18:28:23 +0900
parents ea6fc610b480
children 173d078ee443
files yoneda.agda
diffstat 1 files changed, 17 insertions(+), 2 deletions(-) [+]
line wrap: on
line diff
--- a/yoneda.agda	Wed Aug 28 17:29:01 2013 +0900
+++ b/yoneda.agda	Wed Aug 28 18:28:23 2013 +0900
@@ -51,8 +51,8 @@
 
 open import Function
 
-CF : (a : Obj A) → Functor (Category.op A) Sets
-CF a = record {
+CF : {a : Obj A} → Functor (Category.op A) (Sets {c₂})
+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 {
@@ -79,3 +79,18 @@
                 Category.op A [ g o x ]
              ∎ )
 
+YObj = Functor (Category.op A) (Sets {c₂})
+YHom = λ (f : YObj ) → λ (g : YObj ) → NTrans (Category.op A) Sets f g
+
+open NTrans 
+Yid : {a : YObj} → YHom a a
+Yid {a} = record { TMap = \a -> \x -> x ; isNTrans = isNTrans1 {a} } where
+   isNTrans1 : {a : YObj } → IsNTrans (Category.op A) (Sets {c₂}) a a (\a -> \x -> x )
+   isNTrans1 {a} = record { commute = refl  }
+
+_+_ : {a b c : YObj} → YHom b c → YHom a b → YHom a c
+_+_  = {!!}
+
+isSetsAop :  IsCategory YObj YHom _≡_ _+_ Yid
+isSetsAop  =  {!!}
+