some comments in the code for category theory

5 files changed, 138 insertions, 62 deletions

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) ;

-

-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 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 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 mapObj :  ({c1, c2} : Category)

-          -> Functor c1 c2

-          -> Obj c1

-          -> Obj c2 ;

-def mapObj (functor f0 f1 _ _) = f0 ;

-

-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) ;

+  ----------------------------------------------------------

+  -- 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) 

+               -> (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 ;

+

+  -- 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) ? ;

+

+  fun mapObj :  ({c1, c2} : Category)

+            -> Functor c1 c2

+            -> Obj c1

+            -> Obj c2 ;

+  def mapObj (functor f0 f1 _ _) = f0 ;

+

+  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 ;
 
 }