Mercurial > hg > Members > kono > Proof > category
diff yoneda.agda @ 253:24e83b8b81be
fix
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Wed, 11 Sep 2013 20:26:48 +0900 |
| parents | b2874c5086ea |
| children | 8c72f5284bc8 |
line wrap: on
line diff
--- a/yoneda.agda Mon Sep 09 16:15:09 2013 +0900 +++ b/yoneda.agda Wed Sep 11 20:26:48 2013 +0900 @@ -305,13 +305,14 @@ -- YondaLemma2 : {a b x : Obj A } → (FObj (FObj YonedaFunctor a) x) ≡ (FObj (FObj YonedaFunctor b ) x) → -- a ≡ b -- YondaLemma2 {a} {b} eq = {!!} +-- N.B = ≡-cong gives you ! a ≡ b, so we cannot cong inv to prove a ≡ b -- --- Instead we prove +-- Instead we prove only -- inv ( FObj YonedaFunctor a ) ≡ a inv : {a x : Obj A} ( f : FObj (FObj YonedaFunctor a) x) → Obj A inv {a} f = Category.cod A f -YonedaLemma21 : (a x : Obj A) { f : ( FObj (FObj YonedaFunctor a) x) } → inv f ≡ a -YonedaLemma21 a x {f} = refl +YonedaLemma21 : {a x : Obj A} ( f : ( FObj (FObj YonedaFunctor a) x) ) → inv f ≡ a +YonedaLemma21 {a} {x} f = refl