Mercurial > hg > Members > kono > Proof > category

comparison README.txt @ 773:60942538dc41

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Fri, 29 Dec 2017 11:32:19 +0900
parents 6ccda88f5561
children 2c5ae3015a05
comparison
equal deleted inserted replaced
772:b7a774977345 773:60942538dc41
19 idF.agda 19 idF.agda
20 category-ex.agda 20 category-ex.agda
21 list-monoid-cat.agda 21 list-monoid-cat.agda
22 list-nat.agda 22 list-nat.agda
23 list-nat0.agda 23 list-nat0.agda
24 maybe-monad.agda
25 maybeCat.agda 24 maybeCat.agda
26 monoid-monad.agda 25 monoid-monad.agda
27 26
28 yoneda.agda 27 yoneda.agda
29 28
32 kleisli.agda 31 kleisli.agda
33 em-category.agda 32 em-category.agda
34 adj-monad.agda 33 adj-monad.agda
35 comparison-em.agda 34 comparison-em.agda
36 comparison-functor.agda 35 comparison-functor.agda
36 maybe-monad.agda
37 maybeCat.agda
37 38
38 -- Limit 39 -- Limit
39 40
40 equalizer.agda 41 equalizer.agda
41 universal-mapping.agda 42 universal-mapping.agda
42 free-monoid.agda 43 free-monoid.agda
43 CatExponetial.agda 44 CatExponetial.agda
44 pullback.agda 45 pullback.agda -- including limit from product and equalizer
45 discrete.agda 46 discrete.agda
46 limit-to.agda 47 limit-to.agda
48 SetsCompleteness.agda
49
50 -- Freyd Adjoint Functor Theorem
51
52 Comma.agda
53 Comma1.agda
54 freyd.agda
55 freyd1.agda
56 freyd2.agda
57
58 -- Monoidal functor and Applicative
59
60 monoidal.agda -- Monoidal category and Functor
61 applicative.agda -- Applicative functor is a monoidal functor
62 monad→monoidal.agda
47 63
48 -- no yet finished 64 -- no yet finished
49
50 freyd.agda
51 Comma.agda
52 linton.agda
53 65
54 -- repositories 66 -- repositories
55 67
56 https://bitbucket.org/shinji_kono/category-exercise-in-agda/src 68 https://bitbucket.org/shinji_kono/category-exercise-in-agda/src
69