|
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 maybe-monad.agda
|
|
|
25 maybeCat.agda
|
|
|
26 monoid-monad.agda
|
|
|
27
|
|
|
28 yoneda.agda
|
|
|
29
|
|
|
30 -- Monad and adjunction
|
|
|
31
|
|
|
32 kleisli.agda
|
|
|
33 em-category.agda
|
|
|
34 adj-monad.agda
|
|
|
35 comparison-em.agda
|
|
|
36 comparison-functor.agda
|
|
|
37
|
|
|
38 -- Limit
|
|
|
39
|
|
|
40 equalizer.agda
|
|
|
41 universal-mapping.agda
|
|
|
42 free-monoid.agda
|
|
|
43 CatExponetial.agda
|
|
|
44 pullback.agda
|
|
|
45 discrete.agda
|
|
|
46 limit-to.agda
|
|
|
47
|
|
|
48 -- no yet finished
|
|
|
49
|
|
|
50 freyd.agda
|
|
|
51 Comma.agda
|
|
|
52 linton.agda
|
|
|
53
|
|
|
54 -- repositories
|
|
|
55
|
|
|
56 https://bitbucket.org/shinji_kono/category-exercise-in-agda/src
|
