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

added equality proof in the constructor for natural trasformations

Browse Source
This commit is contained in:
krasimir
2010-06-14 11:21:52 +00:00
parent 357cacd7d7
commit cfd034ab21
1 changed files with 6 additions and 1 deletions
Download Patch File Download Diff File Expand all files Collapse all files

7
examples/category-theory/NaturalTransform.gf
View File

@@ -8,7 +8,12 @@ abstract NaturalTransform = Functor ** {
data nt : ({c1,c2} : Category)
-> (f,g : Functor c1 c2)
-> ((x : Obj c1) -> Arrow (mapObj f x) (mapObj g x))
-> (n : (x : Obj c1) -> Arrow (mapObj f x) (mapObj g x))
-> ( ({x,y} : Obj c1)
-> (ar : Arrow x y)
-> EqAr (comp (n y) (mapAr f ar))
(comp (mapAr g ar) (n x))
)
-> NT f g ;
}