Mercurial > hg > Members > kono > Proof > category
directory / @ 684:5d9d7c2f2718
| name | size | permissions |
|---|---|---|
 doc/
|
drwxr-xr-x | |
 CatExponetial.agda
|
5829 | -rw-r--r-- |
|
Comma.agda
|
4899 | -rw-r--r-- |
|
Comma1.agda
|
7536 | -rw-r--r-- |
|
HomReasoning.agda
|
8320 | -rw-r--r-- |
|
LICENSE.TXT
|
1552 | -rw-r--r-- |
|
README.txt
|
932 | -rw-r--r-- |
|
S.agda
|
2494 | -rw-r--r-- |
|
SetsCompleteness.agda
|
14779 | -rw-r--r-- |
|
adj-monad.agda
|
4273 | -rw-r--r-- |
|
cat-utility.agda
|
21690 | -rw-r--r-- |
|
category-ex.agda
|
266 | -rw-r--r-- |
|
code-data.agda
|
9201 | -rw-r--r-- |
|
comparison-em.agda
|
6705 | -rw-r--r-- |
|
comparison-functor.agda
|
9618 | -rw-r--r-- |
|
discrete.agda
|
6895 | -rw-r--r-- |
|
em-category.agda
|
13051 | -rw-r--r-- |
|
equalizer.agda
|
20520 | -rw-r--r-- |
|
free-monoid.agda
|
14583 | -rw-r--r-- |
|
freyd.agda
|
6482 | -rw-r--r-- |
|
freyd1.agda
|
16232 | -rw-r--r-- |
|
freyd2.agda
|
21232 | -rw-r--r-- |
|
idF.agda
|
1808 | -rw-r--r-- |
|
kleisli.agda
|
23988 | -rw-r--r-- |
|
level-ex.agda
|
244 | -rw-r--r-- |
|
limit-to.agda
|
14848 | -rw-r--r-- |
|
list-level.agda
|
4243 | -rw-r--r-- |
|
list-monoid-cat.agda
|
4100 | -rw-r--r-- |
|
list-nat.agda
|
4066 | -rw-r--r-- |
|
list-nat0.agda
|
3181 | -rw-r--r-- |
|
list.agda
|
128 | -rw-r--r-- |
|
maybe-monad.agda
|
4999 | -rw-r--r-- |
|
maybeCat.agda
|
6920 | -rw-r--r-- |
|
monoid-monad.agda
|
7766 | -rw-r--r-- |
|
negnat.agda
|
4190 | -rw-r--r-- |
|
pullback.agda
|
29723 | -rw-r--r-- |
|
record-ex.agda
|
975 | -rw-r--r-- |
|
system-f.agda
|
11008 | -rw-r--r-- |
|
system-t.agda
|
8328 | -rw-r--r-- |
|
universal-mapping.agda
|
34980 | -rw-r--r-- |
|
yoneda.agda
|
16366 | -rw-r--r-- |