Category Exercise on Higher order categorical logic
====

These are set of Agda exercise for Introduction to Higher order categorical logic.

https://www.amazon.co.jp/gp/product/0521356539

Based on Category Library (https://github.com/shinji-kono/category-agda)

	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
	freyd1.agda               "
	freyd2.agda               "
	graph.agda               Category generated by a Graph 
	idF.agda                 identit functor
	kleisli.agda             Kleisli Category
	level-ex.agda
	limit-to.agda            Example related to Limits p.24
	list-level.agda
	list-monoid-cat.agda
	list-nat.agda
	list-nat0.agda
	list.agda
	maybe-monad.agda
	maybeCat.agda
	monad→monoidal.agda      Monad on Sets is a monoidal functor 
	monoid-monad.agda        Monad with Monoid  p.28
	monoidal.agda            Monoidal Functor
	negnat.agda
	pullback.agda            Pullback p.24
	record-ex.agda
	stdalone-kleisli.agda
	system-f.agda
	system-t.agda
	universal-mapping.agda   Universal mapping p.13
	yoneda.agda              Yoneda Functor p.11