Mercurial > hg > Members > kono > Proof > category
directory / @ 772:b7a774977345
name | size | permissions |
---|---|---|
doc/ | drwxr-xr-x | |
.hgtags | 539 | -rw-r--r-- |
CatExponetial.agda | 5829 | -rw-r--r-- |
Comma.agda | 4899 | -rw-r--r-- |
Comma1.agda | 7536 | -rw-r--r-- |
HomReasoning.agda | 8333 | -rw-r--r-- |
LICENSE.TXT | 1552 | -rw-r--r-- |
README.txt | 932 | -rw-r--r-- |
S.agda | 2494 | -rw-r--r-- |
SetsCompleteness.agda | 14976 | -rw-r--r-- |
adj-monad.agda | 4371 | -rw-r--r-- |
applicative.agda | 40248 | -rw-r--r-- |
bitbucket-pipelines.yml | 409 | -rw-r--r-- |
cat-utility.agda | 21773 | -rw-r--r-- |
category-ex.agda | 266 | -rw-r--r-- |
code-data.agda | 9233 | -rw-r--r-- |
comparison-em.agda | 6693 | -rw-r--r-- |
comparison-functor.agda | 9561 | -rw-r--r-- |
discrete.agda | 6895 | -rw-r--r-- |
em-category.agda | 13238 | -rw-r--r-- |
equalizer.agda | 20520 | -rw-r--r-- |
free-monoid.agda | 14532 | -rw-r--r-- |
freyd.agda | 6270 | -rw-r--r-- |
freyd1.agda | 16231 | -rw-r--r-- |
freyd2.agda | 21363 | -rw-r--r-- |
idF.agda | 1808 | -rw-r--r-- |
kleisli.agda | 24315 | -rw-r--r-- |
level-ex.agda | 244 | -rw-r--r-- |
limit-to.agda | 14807 | -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-- |
monad→monoidal.agda | 35708 | -rw-r--r-- |
monoid-monad.agda | 7766 | -rw-r--r-- |
monoidal.agda | 24771 | -rw-r--r-- |
negnat.agda | 4190 | -rw-r--r-- |
pullback.agda | 30189 | -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 | 36359 | -rw-r--r-- |
yoneda.agda | 16284 | -rw-r--r-- |