diff --git a/examples/category-theory/Adjoints.gf b/examples/category-theory/Adjoints.gf
index cb4c8c6c0..b4987228d 100644
--- a/examples/category-theory/Adjoints.gf
+++ b/examples/category-theory/Adjoints.gf
@@ -1,11 +1,16 @@
 abstract Adjoints = NaturalTransform ** {
 
-cat Adjoints ({c1,c2} : Category) (Functor c1 c2) (Functor c2 c1) ;
+  ----------------------------------------------------------
+  -- Adjoint functors - pair of functors such that
+  -- there is a natural transformation from the identity
+  -- functor to the composition of the functors.
 
-data adjoints : ({c1,c2} : Category)
-              -> (f : Functor c1 c2)
-              -> (g : Functor c2 c1)
-              -> NT (idF c1) (compF g f)
-              -> Adjoints f g ;
+  cat Adjoints ({c1,c2} : Category) (Functor c1 c2) (Functor c2 c1) ;
 
-}
\ No newline at end of file
+  data adjoints : ({c1,c2} : Category)
+                -> (f : Functor c1 c2)
+                -> (g : Functor c2 c1)
+                -> NT (idF c1) (compF g f)
+                -> Adjoints f g ;
+
+}
diff --git a/examples/category-theory/Categories.gf b/examples/category-theory/Categories.gf
index 00fcdad7e..b20dccde9 100644
--- a/examples/category-theory/Categories.gf
+++ b/examples/category-theory/Categories.gf
@@ -1,5 +1,9 @@
 abstract Categories = {
 
+  -------------------------------------------------------
+  -- Basic category theory: categories, objects, 
+  -- arrows and equality of arrows
+
   cat Category ;
       Obj Category ;
       Arrow ({c} : Category) (Obj c) (Obj c) ;
@@ -11,14 +15,23 @@ abstract Categories = {
   fun codom : ({c} : Category) -> ({x,y} : Obj c) -> Arrow x y -> Obj c ;
   def codom {_} {x} {y} _ = y ;
 
+  -- 'id x' is the identity arrow for object x
   fun id   : ({c} : Category) -> (x : Obj c) -> Arrow x x ;
 
+  -- composition of arrows
   fun comp : ({c} : Category) -> ({x,y,z} : Obj c) -> Arrow z y -> Arrow x z -> Arrow x y ;
 
+
+  -------------------------------------------------------
+  -- The basic equality properties: reflexive, 
+  -- symetric and transitive relation. 
+  -- Only the reflexivity is an axiom.
+
   data eqRefl :  ({c} : Category)
               -> ({x,y} : Obj c)
               -> (a : Arrow x y)
               -> EqAr a a ;
+
   fun  eqSym  : ({c} : Category)
               -> ({x,y} : Obj c)
               -> ({a,b} : Arrow x y)
@@ -34,21 +47,18 @@ abstract Categories = {
              -> EqAr g h ;
   def eqTran (eqRefl a) eq = eq ;
 
-  fun eqCompL :  ({c} : Category)
-              -> ({x,y,z} : Obj c)
-              -> ({g,h} : Arrow x z)
-              -> (f : Arrow z y)
-              -> EqAr g h
-              -> EqAr (comp f g) (comp f h) ;
-  def eqCompL f (eqRefl g) = eqRefl (comp f g) ;
 
-  fun eqCompR :  ({c} : Category)
-              -> ({x,y,z} : Obj c)
-              -> ({g,h} : Arrow z y)
-              -> EqAr g h
-              -> (f : Arrow x z)
-              -> EqAr (comp g f) (comp h f) ;
-  def eqCompR (eqRefl g) f = eqRefl (comp g f) ;
+  -------------------------------------------------------
+  -- Now we prove some theorems which are specific for
+  -- the equality of arrows
+  --
+  -- First we assert the axioms:
+  --
+  --    a . id == id . a == a
+  --    f . (g . h) == (f . g) . h
+  --
+  -- and after that we prove that the composition
+  -- preserves the equality.
 
   fun eqIdL  : ({c} : Category)
              -> ({x,y} : Obj c)
@@ -66,6 +76,28 @@ abstract Categories = {
               -> (h : Arrow x z)
               -> EqAr (comp f (comp g h)) (comp (comp f g) h) ;
 
+  fun eqCompL :  ({c} : Category)
+              -> ({x,y,z} : Obj c)
+              -> ({g,h} : Arrow x z)
+              -> (f : Arrow z y)
+              -> EqAr g h
+              -> EqAr (comp f g) (comp f h) ;
+  def eqCompL f (eqRefl g) = eqRefl (comp f g) ;
+
+  fun eqCompR :  ({c} : Category)
+              -> ({x,y,z} : Obj c)
+              -> ({g,h} : Arrow z y)
+              -> EqAr g h
+              -> (f : Arrow x z)
+              -> EqAr (comp g f) (comp h f) ;
+  def eqCompR (eqRefl g) f = eqRefl (comp g f) ;
+
+
+  -------------------------------------------------------
+  -- Operations over categories
+  --
+  
+  -- 1. Dual category
   data Op   :  (c : Category)
             -> Category ;
        opObj:  ({c} : Category)
@@ -86,6 +118,7 @@ abstract Categories = {
            -> EqAr (opAr f) (opAr g) ;
   def eqOp (eqRefl f) = eqRefl (opAr f) ;
 
+  -- 2. Slash of a category
   data Slash     :  (c : Category)
                  -> (x : Obj c)
                  -> Category ;
@@ -102,6 +135,7 @@ abstract Categories = {
   def  id (slashObj x {y} a) = slashAr x (id y) ;
   def  comp (slashAr t azy) (slashAr ~t axz) = slashAr t (comp azy axz) ;
 
+  -- 3. CoSlash of a category
   data CoSlash   :  (c : Category)
                  -> (x : Obj c)
                  -> Category ;
@@ -118,6 +152,7 @@ abstract Categories = {
   def  id (coslashObj x {y} a) = coslashAr x (id y) ;
   def  comp (coslashAr t ayz) (coslashAr ~t azx) = coslashAr t (comp azx ayz) ;
 
+  -- 4. Cartesian product of two categories
   data Prod   :  (c1,c2 : Category)
               -> Category ;
        prodObj:  ({c1,c2} : Category)
@@ -139,6 +174,7 @@ abstract Categories = {
   fun snd : ({c1,c2} : Category) -> Obj (Prod c1 c2) -> Obj c2 ;
   def snd (prodObj _ x2) = x2 ;
   
+  -- 5. Sum of two categories
   data Sum    :  (c1,c2 : Category)
               -> Category ;
        sumLObj:  ({c1,c2} : Category)
diff --git a/examples/category-theory/Functor.gf b/examples/category-theory/Functor.gf
index 45f519edf..4acea7aa6 100644
--- a/examples/category-theory/Functor.gf
+++ b/examples/category-theory/Functor.gf
@@ -1,40 +1,49 @@
 abstract Functor = Categories ** {
 
-cat Functor (c1, c2 : Category) ;
+  ----------------------------------------------------------
+  -- Functor - an arrow (a morphism) between two categories
+  --
+  -- The functor is defined by two morphisms - one for the
+  -- objects and one for the arrows. We also require that
+  -- the morphisms preserve the categorial structure.
 
-data functor :  ({c1, c2} : Category) 
-             -> (f0 : Obj c1 -> Obj c2)
-             -> (f1 : ({x,y} : Obj c1) -> Arrow x y -> Arrow (f0 x) (f0 y))
-             -> ((x : Obj c1) -> EqAr (f1 (id x)) (id (f0 x)))
-             -> (({x,y,z} : Obj c1) -> (f : Arrow x z) -> (g : Arrow z y) -> EqAr (f1 (comp g f)) (comp (f1 g) (f1 f)))
-             -> Functor c1 c2 ;
+  cat Functor (c1, c2 : Category) ;
 
-fun idF : (c : Category) -> Functor c c ;
-def idF c = functor (\x->x) (\f->f) (\x -> eqRefl (id x)) (\f,g -> eqRefl (comp g f)) ;
+  data functor :  ({c1, c2} : Category) 
+               -> (f0 : Obj c1 -> Obj c2)
+               -> (f1 : ({x,y} : Obj c1) -> Arrow x y -> Arrow (f0 x) (f0 y))
+               -> ((x : Obj c1) -> EqAr (f1 (id x)) (id (f0 x)))
+               -> (({x,y,z} : Obj c1) -> (f : Arrow x z) -> (g : Arrow z y) -> EqAr (f1 (comp g f)) (comp (f1 g) (f1 f)))
+               -> Functor c1 c2 ;
 
-fun compF : ({c1,c2,c3} : Category) -> Functor c3 c2 -> Functor c1 c3 -> Functor c1 c2 ;
-def compF (functor f032 f132 eqid32 eqcmp32) (functor f013 f113 eqid13 eqcmp13) =
-         functor (\x -> f032 (f013 x)) (\x -> f132 (f113 x)) (\x -> mapEqAr f132 eqid13) ? ;
+  -- identity functor
+  fun idF : (c : Category) -> Functor c c ;
+  def idF c = functor (\x->x) (\f->f) (\x -> eqRefl (id x)) (\f,g -> eqRefl (comp g f)) ;
 
-fun mapObj :  ({c1, c2} : Category)
-          -> Functor c1 c2
-          -> Obj c1
-          -> Obj c2 ;
-def mapObj (functor f0 f1 _ _) = f0 ;
+  -- composition of two functors
+  fun compF : ({c1,c2,c3} : Category) -> Functor c3 c2 -> Functor c1 c3 -> Functor c1 c2 ;
+  def compF (functor f032 f132 eqid32 eqcmp32) (functor f013 f113 eqid13 eqcmp13) =
+           functor (\x -> f032 (f013 x)) (\x -> f132 (f113 x)) (\x -> mapEqAr f132 eqid13) ? ;
 
-fun mapAr :  ({c1, c2} : Category)
-          -> ({x,y} : Obj c1)
-          -> (f : Functor c1 c2)
-          -> Arrow x y
-          -> Arrow (mapObj f x) (mapObj f y) ;
-def mapAr (functor f0 f1 _ _) = f1 ;
+  fun mapObj :  ({c1, c2} : Category)
+            -> Functor c1 c2
+            -> Obj c1
+            -> Obj c2 ;
+  def mapObj (functor f0 f1 _ _) = f0 ;
 
-fun mapEqAr :  ({c} : Category)
-            -> ({x,y} : Obj c)
-            -> ({f,g} : Arrow x y)
-            -> (func : Arrow x y -> Arrow x y)
-            -> EqAr f g
-            -> EqAr (func f) (func g) ;
-def mapEqAr func (eqRefl f) = eqRefl (func f) ;
+  fun mapAr :  ({c1, c2} : Category)
+            -> ({x,y} : Obj c1)
+            -> (f : Functor c1 c2)
+            -> Arrow x y
+            -> Arrow (mapObj f x) (mapObj f y) ;
+  def mapAr (functor f0 f1 _ _) = f1 ;
+
+  fun mapEqAr :  ({c} : Category)
+              -> ({x,y} : Obj c)
+              -> ({f,g} : Arrow x y)
+              -> (func : Arrow x y -> Arrow x y)
+              -> EqAr f g
+              -> EqAr (func f) (func g) ;
+  def mapEqAr func (eqRefl f) = eqRefl (func f) ;
 
 }
diff --git a/examples/category-theory/Morphisms.gf b/examples/category-theory/Morphisms.gf
index e86059115..10020686a 100644
--- a/examples/category-theory/Morphisms.gf
+++ b/examples/category-theory/Morphisms.gf
@@ -1,5 +1,9 @@
 abstract Morphisms = Categories ** {
 
+-------------------------------------------------------
+-- 1. Isomorphism - pair of arrows whose composition
+-- is the identity arrow
+
 cat Iso ({c} : Category) ({x,y} : Obj c) (Arrow x y) (Arrow y x) ;
 
 data iso :  ({c} : Category)
@@ -18,6 +22,7 @@ fun isoOp : ({c} : Category)
          -> Iso (opAr g) (opAr f) ;
 def isoOp (iso f g id_fg id_gf) = iso (opAr g) (opAr f) (eqOp id_fg) (eqOp id_gf) ;
 
+-- every isomorphism is also monomorphism
 fun iso2mono :  ({c} : Category)
              -> ({x,y} : Obj c)
              -> ({f} : Arrow x y)
@@ -34,6 +39,7 @@ def iso2mono (iso f g id_fg id_gf) =
                                                                                    (eqCompL g eq_fh_fm))))))))) ;  -- g . (f . h) = g . (f . m)
                                                                                                                    --      f . h  = f . m
 
+-- every isomorphism is also epimorphism
 fun iso2epi  :  ({c} : Category)
              -> ({x,y} : Obj c)
              -> ({f} : Arrow x y)
@@ -51,6 +57,14 @@ def iso2epi (iso fff g id_fg id_gf) =
                                                                                    (eqCompR eq_hf_mf g))))))))) ; -- (h . f) . g = (m . f) . g
                                                                                                                   --  h . f      =  m . f
 
+
+-------------------------------------------------------
+-- 2. Monomorphism - an arrow f such that:
+-- 
+--        f . h == f . m  ==>  h == m
+--
+-- for every h and m.
+
 cat Mono ({c} : Category) ({x,y} : Obj c) (Arrow x y) ;
 
 data mono :  ({c} : Category)
@@ -59,6 +73,14 @@ data mono :  ({c} : Category)
           -> (({z} : Obj c) -> (h,m : Arrow z x) -> EqAr (comp f h) (comp f m) -> EqAr h m)
           -> Mono f ;
 
+
+-------------------------------------------------------
+-- 3. Epimorphism - an arrow f such that:
+-- 
+--        h . f == m . f  ==>  h == m
+--
+-- for every h and m.
+
 cat Epi ({c} : Category) ({x,y} : Obj c) (Arrow x y) ;
 
 data epi  :  ({c} : Category)
diff --git a/examples/category-theory/NaturalTransform.gf b/examples/category-theory/NaturalTransform.gf
index 6a3462985..e7da79b93 100644
--- a/examples/category-theory/NaturalTransform.gf
+++ b/examples/category-theory/NaturalTransform.gf
@@ -1,10 +1,14 @@
 abstract NaturalTransform = Functor ** {
 
-cat NT ({c1,c2} : Category) (f,g : Functor c1 c2) ;
+  ----------------------------------------------------------
+  -- Natural transformation - a pair of functors which 
+  -- differ up to an arrow
 
-data nt :  ({c1,c2} : Category)
-        -> (f,g : Functor c1 c2)
-        -> ((x : Obj c1) -> Arrow (mapObj f x) (mapObj g x))
-        -> NT f g ;
+  cat NT ({c1,c2} : Category) (f,g : Functor c1 c2) ;
+
+  data nt :  ({c1,c2} : Category)
+          -> (f,g : Functor c1 c2)
+          -> ((x : Obj c1) -> Arrow (mapObj f x) (mapObj g x))
+          -> NT f g ;
 
 }