fix the definition of functor composition in category theory

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

 

 }