From d9d00e172a377c11427bdc0848f45c1d74aaa289 Mon Sep 17 00:00:00 2001
From: krasimir <krasimir@chalmers.se>
Date: Sat, 8 Jan 2011 20:43:45 +0000
Subject: [PATCH] fix the definition of functor composition in category theory

---
 examples/category-theory/Functor.gf | 16 ++++++++++------
 1 file changed, 10 insertions(+), 6 deletions(-)

diff --git a/examples/category-theory/Functor.gf b/examples/category-theory/Functor.gf
index 4acea7aa6..e70254839 100644
--- a/examples/category-theory/Functor.gf
+++ b/examples/category-theory/Functor.gf
@@ -23,7 +23,10 @@ abstract Functor = Categories ** {
   -- 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) ? ;
+           functor (\x -> f032 (f013 x))
+                   (\x -> f132 (f113 x))
+                   (\x -> eqTran (eqSym (mapEqAr f032 f132 (eqid13 x))) (eqid32 (f013 x)))
+                   (\f,g -> eqTran (eqSym (mapEqAr f032 f132 (eqcmp13 f g))) (eqcmp32 (f113 f) (f113 g))) ;
 
   fun mapObj :  ({c1, c2} : Category)
             -> Functor c1 c2
@@ -38,12 +41,13 @@ abstract Functor = Categories ** {
             -> Arrow (mapObj f x) (mapObj f y) ;
   def mapAr (functor f0 f1 _ _) = f1 ;
 
-  fun mapEqAr :  ({c} : Category)
-              -> ({x,y} : Obj c)
+  fun mapEqAr :  ({c1,c2} : Category)
+              -> ({x,y} : Obj c1)
               -> ({f,g} : Arrow x y)
-              -> (func : Arrow x y -> Arrow x y)
+              -> (f0 : Obj c1 -> Obj c2)
+              -> (f1 : Arrow x y -> Arrow (f0 x) (f0 y))
               -> EqAr f g
-              -> EqAr (func f) (func g) ;
-  def mapEqAr func (eqRefl f) = eqRefl (func f) ;
+              -> EqAr (f1 f) (f1 g) ;
+  def mapEqAr f0 f1 (eqRefl f) = eqRefl (f1 f) ;
 
 }