some comments in the code for category theory

examples/category-theory/Adjoints.gf

@@ -1,5 +1,10 @@
 abstract Adjoints = NaturalTransform ** {
 
+  ----------------------------------------------------------
+  -- Adjoint functors - pair of functors such that
+  -- there is a natural transformation from the identity
+  -- functor to the composition of the functors.
+
   cat Adjoints ({c1,c2} : Category) (Functor c1 c2) (Functor c2 c1) ;
 
   data adjoints : ({c1,c2} : Category)

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)
+  -- Now we prove some theorems which are specific for
-              -> ({g,h} : Arrow z y)
+  -- the equality of arrows
-              -> EqAr g h
+  --
-              -> (f : Arrow x z)
+  -- First we assert the axioms:
-              -> EqAr (comp g f) (comp h f) ;
+  --
-  def eqCompR (eqRefl g) f = eqRefl (comp g f) ;
+  --    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)

examples/category-theory/Functor.gf

@@ -1,5 +1,12 @@
 abstract Functor = Categories ** {
 
+  ----------------------------------------------------------
+  -- 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.
+
   cat Functor (c1, c2 : Category) ;
 
   data functor :  ({c1, c2} : Category) 
@@ -9,9 +16,11 @@ data functor :  ({c1, c2} : Category)
                -> (({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 ;
 
+  -- 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)) ;
 
+  -- 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) ? ;

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)

examples/category-theory/NaturalTransform.gf

@@ -1,5 +1,9 @@
 abstract NaturalTransform = Functor ** {
 
+  ----------------------------------------------------------
+  -- Natural transformation - a pair of functors which 
+  -- differ up to an arrow
+
   cat NT ({c1,c2} : Category) (f,g : Functor c1 c2) ;
 
   data nt :  ({c1,c2} : Category)