Mercurial > hg > Members > kono > Proof > category

changeset 193:4e6f080f0107

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
isomorphic problem written
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Fri, 30 Aug 2013 16:49:28 +0900
parents d7e4b7b441be
children 3271d2d04b17
files yoneda.agda
diffstat 1 files changed, 7 insertions(+), 1 deletions(-) [+]
line wrap: on
line diff
--- a/yoneda.agda	Fri Aug 30 16:34:48 2013 +0900
+++ b/yoneda.agda	Fri Aug 30 16:49:28 2013 +0900
@@ -236,5 +236,11 @@
 
 
 Nat2F : {a : Obj A} → {F : Obj SetsAop} →  Hom SetsAop (CF {a}) F  → FObj F a 
-Nat2F  =  {!!}
+Nat2F {a} {F} ha =  ( TMap ha a ) (id1 A a)
 
+F2Nat→Nat2F : {a : Obj A } → {F : Obj SetsAop} → (fa : FObj F a) →  Nat2F {a} {F} (F2Nat {a} {F} fa) ≡ fa 
+F2Nat→Nat2F  = {!!}
+
+Nat2F→F2Nat : {a : Obj A } → {F : Obj SetsAop} → (ha : Hom SetsAop (CF {a}) F) →  SetsAop [ F2Nat {a} {F} (Nat2F {a} {F} ha) ≈ ha ]
+Nat2F→F2Nat = {!!}
+