added natural transformations

examples/category-theory/CategoryTheory.gf

@@ -3,6 +3,7 @@ abstract CategoryTheory
   , Morphisms
   , InitialAndTerminal
   , Functor
+  , NaturalTransform
   , Equalizer
 ** {
 }

examples/category-theory/Functor.gf

@@ -12,7 +12,22 @@ data functor :  ({c1, c2} : Category)
 fun compF : ({c1,c2,c3} : Category) -> Functor c3 c2 -> Functor c1 c3 -> Functor c1 c2 ;
 def compF {c1} {c2} {c3} (functor {c3} {c2} f032 f132 eqid32 eqcmp32) (functor {c1} {c3} f013 f113 eqid13 eqcmp13) =
         functor (\x -> f032 (f013 x)) (\x -> f132 (f113 x)) (\x -> mapEqAr (f132 {?} {?}) eqid13) ? ;
+-}
 
+fun mapEl :  ({c1, c2} : Category)
+          -> Functor c1 c2
+          -> El c1
+          -> El c2 ;
+def mapEl {c1} {c2} (functor {c1} {c2} f0 f1 _ _) = f0 ;
+{-
+fun mapAr :  ({c1, c2} : Category)
+          -> ({x,y} : El c1)
+          -> (f : Functor c1 c2)
+          -> Arrow x y
+          -> Arrow (mapEl f x) (mapEl f y) ;
+def mapAr {c1} {c2} {x} {y} (functor {c1} {c2} f0 f1 _ _) = f1 {x} {y} ;
+-}
+{-
 fun mapEqAr :  ({c} : Category)
             -> ({x,y} : El c)
             -> ({f,g} : Arrow x y)

examples/category-theory/NaturalTransform.gf

@@ -0,0 +1,10 @@
+abstract NaturalTransform = Functor ** {
+
+cat NT ({c1,c2} : Category) (f,g : Functor c1 c2) ;
+
+data nt :  ({c1,c2} : Category)
+        -> (f,g : Functor c1 c2)
+        -> ((x : El c1) -> Arrow (mapEl f x) (mapEl g x))
+        -> NT f g ;
+
+}