Mercurial > hg > Members > kono > Proof > category
directory / @ 784:f27d966939f8
name | size | permissions |
---|---|---|
doc/ | drwxr-xr-x | |
.hgtags | 539 | -rw-r--r-- |
CCC.agda | 3739 | -rw-r--r-- |
CCChom.agda | 3013 | -rw-r--r-- |
CatExponetial.agda | 5829 | -rw-r--r-- |
Comma.agda | 4899 | -rw-r--r-- |
Comma1.agda | 7536 | -rw-r--r-- |
HomReasoning.agda | 8418 | -rw-r--r-- |
LICENSE.TXT | 1552 | -rw-r--r-- |
README.txt | 1314 | -rw-r--r-- |
S.agda | 2494 | -rw-r--r-- |
SetsCompleteness.agda | 15042 | -rw-r--r-- |
adj-monad.agda | 4371 | -rw-r--r-- |
applicative.agda | 40008 | -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 | 6624 | -rw-r--r-- |
em-category.agda | 13238 | -rw-r--r-- |
epi.agda | 6431 | -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 | 21435 | -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 | 14831 | -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 | 39321 | -rw-r--r-- |
monoid-monad.agda | 7902 | -rw-r--r-- |
monoidal.agda | 24837 | -rw-r--r-- |
negnat.agda | 4190 | -rw-r--r-- |
pullback.agda | 30186 | -rw-r--r-- |
record-ex.agda | 975 | -rw-r--r-- |
stdalone-kleisli.agda | 30085 | -rw-r--r-- |
system-f.agda | 11678 | -rw-r--r-- |
system-t.agda | 8328 | -rw-r--r-- |
universal-mapping.agda | 36372 | -rw-r--r-- |
yoneda.agda | 17082 | -rw-r--r-- |