Mercurial > hg > Members > kono > Proof > category

changeset 198:1edba4226474

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
comment
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sat, 31 Aug 2013 01:51:38 +0900
parents ec50ff189f62
children 0ce7795fa46b
files yoneda.agda
diffstat 1 files changed, 1 insertions(+), 1 deletions(-) [+]
line wrap: on
line diff
--- a/yoneda.agda	Sat Aug 31 01:47:49 2013 +0900
+++ b/yoneda.agda	Sat Aug 31 01:51:38 2013 +0900
@@ -325,4 +325,4 @@
 -- YondaLemma2 : {a b : Obj A }  → (λ x → FObj (FObj YonedaFunctor a) x)  ≡ (λ x → FObj (FObj YonedaFunctor b  ) x)  →  
 --        {f : Hom A a b } → a ≡ b 
 -- YondaLemma2 {a} {b} eq  {f}  = {!!} eq
-
+-- I cannot prove this, sorry