From 930cc116846c762334abfb77a227aff09e400328 Mon Sep 17 00:00:00 2001
From: Floris van Doorn <fpv@andrew.cmu.edu>
Date: Thu, 6 Nov 2014 22:17:08 -0500
Subject: [PATCH] doc(algebra): update markdown files

---
 library/algebra/algebra.md           |  3 ++-
 library/algebra/category/category.md | 16 ++++++++++++++++
 2 files changed, 18 insertions(+), 1 deletion(-)
 create mode 100644 library/algebra/category/category.md

diff --git a/library/algebra/algebra.md b/library/algebra/algebra.md
index ad3aa0e8c..b95e7492d 100644
--- a/library/algebra/algebra.md
+++ b/library/algebra/algebra.md
@@ -8,4 +8,5 @@ Algebraic structures.
 * [binary](binary.lean) : binary operations
 * [wf](wf.lean) : well-founded relations
 * [group](group.lean)
-* [category](category.lean)
\ No newline at end of file
+* [category](category/category.md) : category theory
+
diff --git a/library/algebra/category/category.md b/library/algebra/category/category.md
new file mode 100644
index 000000000..169990601
--- /dev/null
+++ b/library/algebra/category/category.md
@@ -0,0 +1,16 @@
+category
+=======
+
+Algebraic structures.
+
+* [basic](basic.lean) : definition of fully and partially bundled categories
+* [morphism](morphism.lean) : isos, retracts, sections, monos, epis
+* [functor](functor.lean) : functors, category of (smaller) categories
+* [natural_transformation](natural_transformation.lean)
+* [constructions](constructions.lean) : constructions of basic examples and constructions of categories: opposite, type, discrete, product, functor, slice and arrow categories
+
+The following files hardly have any content so far.
+
+* [limit](limit.lean) : limits and colimits
+* [adjoint](adjoint.lean) : adjoint functors
+* [yoneda](yoneda.lean) : Yoneda embedding and Yoneda lemma
\ No newline at end of file