added equality proof in the constructor for natural trasformations

2010-06-14 11:21:52 +00:00
parent 07da5a43c9
commit b2a0adf969
1 changed files with 6 additions and 1 deletions
--- a/examples/category-theory/NaturalTransform.gf
+++ b/examples/category-theory/NaturalTransform.gf
@@ -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 ;

 }