2 files changed, 13 insertions, 0 deletions
diff --git a/examples/category-theory/CategoryTheory.gf b/examples/category-theory/CategoryTheory.gf
index d896ceb35..d75f71694 100644
--- a/examples/category-theory/CategoryTheory.gf
+++ b/examples/category-theory/CategoryTheory.gf
@@ -2,6 +2,7 @@ abstract CategoryTheory
   = Categories
   , Morphisms
   , InitialAndTerminal
+  , Functor
 
 ** {
 }
 \ No newline at end of file
diff --git a/examples/category-theory/Functor.gf b/examples/category-theory/Functor.gf
new file mode 100644
index 000000000..70ec1a940
--- /dev/null
+++ b/examples/category-theory/Functor.gf
@@ -0,0 +1,12 @@
+abstract Functor = Categories ** {
+
+cat Functor (c1, c2 : Category) ;
+
+data functor :  ({c1, c2} : Category) 
+             -> (f0 : El c1 -> El c2)
+             -> (f1 : ({x,y} : El c1) -> Arrow x y -> Arrow (f0 x) (f0 y))
+             -> ((x : El c1) -> EqAr (f1 (id x)) (id (f0 x)))
+             -> (({x,y,z} : El c1) -> (f : Arrow x z) -> (g : Arrow z y) -> EqAr (f1 (comp g f)) (comp (f1 g) (f1 f)))
+             -> Functor c1 c2 ;
+
+}
+\ No newline at end of file