GitHub/gf-core
1
0
Fork 1
mirror of https://github.com/GrammaticalFramework/gf-core.git synced 2026-04-09 04:59:31 -06:00
Code Issues Packages Projects Releases Wiki Activity

fix the definition of functor composition in category theory

Browse Source
This commit is contained in:
krasimir
2011-01-08 20:43:45 +00:00
parent e41df3c873
commit d9d00e172a
1 changed files with 10 additions and 6 deletions
Download Patch File Download Diff File Expand all files Collapse all files

16
examples/category-theory/Functor.gf
View File

@@ -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) ;
}