# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1488860203 -32400
# Node ID 6ccda88f55615405368af24e42c5c947ebaa450f
# Parent  4c0a955b651dce2594a07d11e49716c1b82308a3
add README

diff -r 4c0a955b651d -r 6ccda88f5561 README.txt
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/README.txt	Tue Mar 07 13:16:43 2017 +0900
@@ -0,0 +1,56 @@
+-- basic training
+
+    level-ex.agda
+    list-level.agda
+    list.agda
+    record-ex.agda
+    negnat.agda
+
+    system-f.agda
+    system-t.agda
+
+-- Category Utilities 
+
+    HomReasoning.agda             -- extensions for reasoning
+    cat-utility.agda              -- basic category constructs
+
+-- Category Theorems
+
+    idF.agda
+    category-ex.agda
+    list-monoid-cat.agda
+    list-nat.agda
+    list-nat0.agda
+    maybe-monad.agda
+    maybeCat.agda
+    monoid-monad.agda
+
+    yoneda.agda
+
+-- Monad and adjunction
+
+    kleisli.agda
+    em-category.agda
+    adj-monad.agda
+    comparison-em.agda
+    comparison-functor.agda
+
+-- Limit 
+
+    equalizer.agda
+    universal-mapping.agda
+    free-monoid.agda
+    CatExponetial.agda
+    pullback.agda
+    discrete.agda
+    limit-to.agda
+
+-- no yet finished
+
+    freyd.agda
+    Comma.agda
+    linton.agda
+
+-- repositories
+
+   https://bitbucket.org/shinji_kono/category-exercise-in-agda/src