|
476
|
1 -- basic training
|
|
|
2
|
|
|
3 level-ex.agda
|
|
|
4 list-level.agda
|
|
|
5 list.agda
|
|
|
6 record-ex.agda
|
|
|
7 negnat.agda
|
|
|
8
|
|
|
9 system-f.agda
|
|
|
10 system-t.agda
|
|
|
11
|
|
|
12 -- Category Utilities
|
|
|
13
|
|
|
14 HomReasoning.agda -- extensions for reasoning
|
|
|
15 cat-utility.agda -- basic category constructs
|
|
|
16
|
|
|
17 -- Category Theorems
|
|
|
18
|
|
|
19 idF.agda
|
|
|
20 category-ex.agda
|
|
|
21 list-monoid-cat.agda
|
|
|
22 list-nat.agda
|
|
|
23 list-nat0.agda
|
|
|
24 maybeCat.agda
|
|
|
25 monoid-monad.agda
|
|
|
26
|
|
|
27 yoneda.agda
|
|
|
28
|
|
|
29 -- Monad and adjunction
|
|
|
30
|
|
|
31 kleisli.agda
|
|
|
32 em-category.agda
|
|
|
33 adj-monad.agda
|
|
|
34 comparison-em.agda
|
|
|
35 comparison-functor.agda
|
|
773
|
36 maybe-monad.agda
|
|
|
37 maybeCat.agda
|
|
476
|
38
|
|
|
39 -- Limit
|
|
|
40
|
|
|
41 equalizer.agda
|
|
|
42 universal-mapping.agda
|
|
|
43 free-monoid.agda
|
|
|
44 CatExponetial.agda
|
|
773
|
45 pullback.agda -- including limit from product and equalizer
|
|
476
|
46 discrete.agda
|
|
|
47 limit-to.agda
|
|
773
|
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
|
|
476
|
63
|
|
|
64 -- no yet finished
|
|
|
65
|
|
|
66 -- repositories
|
|
|
67
|
|
|
68 https://bitbucket.org/shinji_kono/category-exercise-in-agda/src
|
|
773
|
69
|
