//
These are set of Agda exercise for
Introduction to Higher order categorical logic](https://www.amazon.co.jp/gp/product/0521356539)
CCC.agda Cartesian closed category p.52 and Topos p.139
CCCGraph.agda CCC generated from Graph (iconmplete) p.55
CCCSets.agda CCC on Sets and Topos on Sets (not on the book)
CCChom.agda CCC as Hom Isomorphism p.54
CatExponetial.agda Functor Cattegory p.8
Comma.agda Comma category p.27
Comma1.agda Comma category p.27
HomReasoning.agda Reasoning utilities
Polynominal.agda Polynominal Category and functional completeness
S.agda Simple example on Sets Completeness
SetsCompleteness.agda Completeness of Sets
ToposEx.agda Topos Exercise (incomplete) p.141
ToposIL.agda Topos Internal Language (incomplete) p.143
ToposSub.agda Topos Subobject classifier (incomplete)
adj-monad.agda Adjunction implies Monad p.28
applicative.agda Applicative Functor
bi-ccc.agda Bi-cartesian closed category p.65
cat-utility.agda various definitions
category-ex.agda simple ex
code-data.agda simple ex
cokleisli.agda kleisli category on coMonad
comparison-em.agda Elienburg Moore Comparison
comparison-functor.agda kleisli Comparison
em-category.agda Elienburg Moore Resolution
epi.agda epi example
equalizer.agda Equalizer example p.21
free-monoid.agda free monoid
freyd.agda Adjoin Functor Theorem p.26
graph.agda Category generated by a Graph
idF.agda identit functor
kleisli.agda Kleisli Category
limit-to.agda Example related to Limits p.24
monad→monoidal.agda Monad on Sets is a monoidal functor
monoid-monad.agda Monad with Monoid p.28
monoidal.agda Monoidal Functor
pullback.agda Pullback p.24
universal-mapping.agda Universal mapping p.13
yoneda.agda Yoneda Functor p.11