|
1063
|
1 Category Exercise on Higher order categorical logic
|
|
|
2 ====
|
|
|
3
|
|
|
4 These are set of Agda exercise for Introduction to Higher order categorical logic.
|
|
|
5
|
|
|
6 https://www.amazon.co.jp/gp/product/0521356539
|
|
|
7
|
|
|
8 Based on Category Library (https://github.com/shinji-kono/category-agda)
|
|
|
9
|
|
|
10 CCC.agda Cartesian closed category p.52 and Topos p.139
|
|
|
11 CCCGraph.agda CCC generated from Graph (iconmplete) p.55
|
|
|
12 CCCSets.agda CCC on Sets and Topos on Sets (not on the book)
|
|
|
13 CCChom.agda CCC as Hom Isomorphism p.54
|
|
|
14 CatExponetial.agda Functor Cattegory p.8
|
|
|
15 Comma.agda Comma category p.27
|
|
|
16 Comma1.agda Comma category p.27
|
|
|
17 HomReasoning.agda Reasoning utilities
|
|
|
18 Polynominal.agda Polynominal Category and functional completeness
|
|
|
19 S.agda Simple example on Sets Completeness
|
|
|
20 SetsCompleteness.agda Completeness of Sets
|
|
|
21 ToposEx.agda Topos Exercise (incomplete) p.141
|
|
|
22 ToposIL.agda Topos Internal Language (incomplete) p.143
|
|
|
23 ToposSub.agda Topos Subobject classifier (incomplete)
|
|
|
24 adj-monad.agda Adjunction implies Monad p.28
|
|
|
25 applicative.agda Applicative Functor
|
|
|
26 bi-ccc.agda Bi-cartesian closed category p.65
|
|
|
27 cat-utility.agda various definitions
|
|
|
28 category-ex.agda simple ex
|
|
|
29 code-data.agda simple ex
|
|
|
30 cokleisli.agda kleisli category on coMonad
|
|
|
31 comparison-em.agda Elienburg Moore Comparison
|
|
|
32 comparison-functor.agda kleisli Comparison
|
|
|
33 em-category.agda Elienburg Moore Resolution
|
|
|
34 epi.agda epi example
|
|
|
35 equalizer.agda Equalizer example p.21
|
|
|
36 free-monoid.agda free monoid
|
|
|
37 freyd.agda Adjoin Functor Theorem p.26
|
|
|
38 freyd1.agda "
|
|
|
39 freyd2.agda "
|
|
|
40 graph.agda Category generated by a Graph
|
|
|
41 idF.agda identit functor
|
|
|
42 kleisli.agda Kleisli Category
|
|
|
43 level-ex.agda
|
|
|
44 limit-to.agda Example related to Limits p.24
|
|
|
45 list-level.agda
|
|
|
46 list-monoid-cat.agda
|
|
|
47 list-nat.agda
|
|
|
48 list-nat0.agda
|
|
|
49 list.agda
|
|
|
50 maybe-monad.agda
|
|
|
51 maybeCat.agda
|
|
|
52 monad→monoidal.agda Monad on Sets is a monoidal functor
|
|
|
53 monoid-monad.agda Monad with Monoid p.28
|
|
|
54 monoidal.agda Monoidal Functor
|
|
|
55 negnat.agda
|
|
|
56 pullback.agda Pullback p.24
|
|
|
57 record-ex.agda
|
|
|
58 stdalone-kleisli.agda
|
|
|
59 system-f.agda
|
|
|
60 system-t.agda
|
|
|
61 universal-mapping.agda Universal mapping p.13
|
|
|
62 yoneda.agda Yoneda Functor p.11
|
