Mercurial > hg > Members > kono > Proof > category

changeset 476:6ccda88f5561

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
add README
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Tue, 07 Mar 2017 13:16:43 +0900
parents 4c0a955b651d
children bcf941e20737
files README.txt
diffstat 1 files changed, 56 insertions(+), 0 deletions(-) [+]
line wrap: on
line diff
--- /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