| Tue, 23 Jul 2013 01:45:56 +0900 |
Shinji KONO |
uniq-univeralMapping from Adjunction
|
| Tue, 23 Jul 2013 01:27:43 +0900 |
Shinji KONO |
f replacement
|
| Tue, 23 Jul 2013 00:29:17 +0900 |
Shinji KONO |
uniqness
|
| Mon, 22 Jul 2013 21:29:26 +0900 |
Shinji KONO |
Functor Identity
|
| Mon, 22 Jul 2013 19:07:31 +0900 |
Shinji KONO |
isFunctor
|
| Mon, 22 Jul 2013 18:13:57 +0900 |
Shinji KONO |
Adjunction to Universal Mapping end
|
| Mon, 22 Jul 2013 17:51:08 +0900 |
Shinji KONO |
Reasoning
|
| Mon, 22 Jul 2013 17:17:42 +0900 |
Shinji KONO |
reasoning
|
| Mon, 22 Jul 2013 17:11:05 +0900 |
Shinji KONO |
universalMapping
|
| Mon, 22 Jul 2013 16:47:45 +0900 |
Shinji KONO |
isUniversalMapping
|
| Mon, 22 Jul 2013 16:04:23 +0900 |
Shinji KONO |
f∗ = ε(b)F(f),
|
| Mon, 22 Jul 2013 15:16:56 +0900 |
Shinji KONO |
trying...
|
| Mon, 22 Jul 2013 14:54:52 +0900 |
Shinji KONO |
add Adj to Universal Mapping
|
| Mon, 22 Jul 2013 14:45:58 +0900 |
Shinji KONO |
Adjoint
|
| Mon, 22 Jul 2013 14:30:27 +0900 |
Shinji KONO |
add universal mapping
|
| Sat, 13 Jul 2013 18:12:57 +0900 |
Shinji KONO |
fix
|
| Sat, 13 Jul 2013 11:46:58 +0900 |
Shinji KONO |
notation
|
| Sat, 13 Jul 2013 03:05:43 +0900 |
Shinji KONO |
fix
|
| Fri, 12 Jul 2013 22:17:23 +0900 |
Shinji KONO |
fix
|
| Fri, 12 Jul 2013 20:45:54 +0900 |
Shinji KONO |
join association finish
|
| Fri, 12 Jul 2013 20:32:19 +0900 |
Shinji KONO |
on going
|
| Fri, 12 Jul 2013 18:58:16 +0900 |
Shinji KONO |
on going
|
| Fri, 12 Jul 2013 17:56:00 +0900 |
Shinji KONO |
join assoc on going...
|
| Fri, 12 Jul 2013 15:15:50 +0900 |
Shinji KONO |
add some law
|
| Fri, 12 Jul 2013 13:39:33 +0900 |
Shinji KONO |
unity law 1
|
| Fri, 12 Jul 2013 12:28:14 +0900 |
Shinji KONO |
clean up list-nat
|
| Fri, 12 Jul 2013 12:24:29 +0900 |
Shinji KONO |
nat
|
| Fri, 12 Jul 2013 11:39:06 +0900 |
Shinji KONO |
reasoning worked.
|
| Thu, 11 Jul 2013 19:37:35 +0900 |
Shinji KONO |
not working yet
|
| Tue, 09 Jul 2013 10:42:36 +0900 |
Shinji KONO |
sss
|
| Tue, 09 Jul 2013 10:36:20 +0900 |
Shinji KONO |
list nat
|
| Mon, 08 Jul 2013 17:55:04 +0900 |
Shinji KONO |
not yet worked
|
| Mon, 08 Jul 2013 11:00:05 +0900 |
Shinji KONO |
Reasoning on going...
|
| Sun, 07 Jul 2013 20:20:51 +0900 |
Shinji KONO |
Reasoning complete!
|
| Sun, 07 Jul 2013 19:20:37 +0900 |
Shinji KONO |
reasoning test
|
| Sun, 07 Jul 2013 18:45:48 +0900 |
Shinji KONO |
reasoning
|
| Sun, 07 Jul 2013 18:16:46 +0900 |
Shinji KONO |
reasoning
|
| Sun, 07 Jul 2013 16:38:48 +0900 |
Shinji KONO |
refl and trans
|
| Sun, 07 Jul 2013 13:14:54 +0900 |
Shinji KONO |
Reasoning
|
| Sat, 06 Jul 2013 16:28:26 +0900 |
Shinji KONO |
add accessor
|
| Sat, 06 Jul 2013 14:56:23 +0900 |
Shinji KONO |
Kleisli Proposition
|
| Sat, 06 Jul 2013 08:50:32 +0900 |
Shinji KONO |
fix
|
| Sat, 06 Jul 2013 07:27:57 +0900 |
Shinji KONO |
Kleisli
|
| Sat, 06 Jul 2013 03:30:31 +0900 |
Shinji KONO |
unity1 unity2
|
| Sat, 06 Jul 2013 02:15:24 +0900 |
Shinji KONO |
Monad
|
| Sat, 06 Jul 2013 00:34:08 +0900 |
Shinji KONO |
category agda
|
