From 21ad608e2a7a587805a6b99e8c07c6255de348c5 Mon Sep 17 00:00:00 2001
From: krasimir <krasimir@chalmers.se>
Date: Mon, 22 Feb 2010 14:40:28 +0000
Subject: [PATCH] functors

---
 examples/category-theory/CategoryTheory.gf |  1 +
 examples/category-theory/Functor.gf        | 12 ++++++++++++
 2 files changed, 13 insertions(+)
 create mode 100644 examples/category-theory/Functor.gf

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