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

incomplete code for composition of functors

Browse Source
This commit is contained in:
krasimir
2010-03-15 10:47:00 +00:00
parent 77be515422
commit 347347d411
1 changed files with 12 additions and 0 deletions
Download Patch File Download Diff File Expand all files Collapse all files

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

@@ -8,5 +8,17 @@ data functor : ({c1, c2} : Category)
-> ((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 ;
{-
fun compF : ({c1,c2,c3} : Category) -> Functor c3 c2 -> Functor c1 c3 -> Functor c1 c2 ;
def compF {c1} {c2} {c3} (functor {c3} {c2} f032 f132 eqid32 eqcmp32) (functor {c1} {c3} f013 f113 eqid13 eqcmp13) =
functor (\x -> f032 (f013 x)) (\x -> f132 (f113 x)) (\x -> mapEqAr (f132 {?} {?}) eqid13) ? ;
fun mapEqAr : ({c} : Category)
-> ({x,y} : El c)
-> ({f,g} : Arrow x y)
-> (func : Arrow x y -> Arrow x y)
-> EqAr f g
-> EqAr (func f) (func g) ;
def mapEqAr {c} {x} {y} {f} {f} func (eqRefl {c} {x} {y} f) = eqRefl (func f) ;
-}
}