Mercurial > hg > Members > kono > Proof > category

changeset 190:b82d7b054f28

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
one to one nat
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Thu, 29 Aug 2013 16:07:45 +0900
parents c6ce3115cb1b
children 45191dc3f78a
files yoneda.agda
diffstat 1 files changed, 19 insertions(+), 0 deletions(-) [+]
line wrap: on
line diff
--- a/yoneda.agda	Thu Aug 29 12:47:28 2013 +0900
+++ b/yoneda.agda	Thu Aug 29 16:07:45 2013 +0900
@@ -202,4 +202,23 @@
           ) )  )
 
 
+------
+--
+--  F : A → Sets  ∈ Obj SetsAop
+--
+--  F(a) ⇔ Nat(h_a,F)
+--
+------
 
+F2Natmap :  {a : Obj A} → {F : Obj SetsAop} → (x : Obj (Category.op A)) → Hom Sets (FObj (CF {a}) x) (FObj F x)
+F2Natmap = {!!}
+
+F2Nat : {a : Obj A} → {F : Obj SetsAop} →  FObj F a  → Hom SetsAop (CF {a}) F
+F2Nat {a} {F} x = record { TMap = F2Natmap {a} {F} ; isNTrans = isNTrans1 {a} } where
+   isNTrans1 : {a : Obj A } → IsNTrans (Category.op A) (Sets {c₂}) (CF {a}) F (F2Natmap {a} {F})
+   isNTrans1 {a} = record { commute = {!!}  }
+
+
+Nat2F : {a : Obj A} → {F : Obj SetsAop} →  Hom SetsAop (CF {a}) F  → FObj F a 
+Nat2F  =  {!!}
+