From b2a0adf96984aa50669c25b082f509daabbb5d97 Mon Sep 17 00:00:00 2001
From: krasimir <krasimir@chalmers.se>
Date: Mon, 14 Jun 2010 11:21:52 +0000
Subject: [PATCH] added equality proof in the constructor for natural
 trasformations

---
 examples/category-theory/NaturalTransform.gf | 7 ++++++-
 1 file changed, 6 insertions(+), 1 deletion(-)

diff --git a/examples/category-theory/NaturalTransform.gf b/examples/category-theory/NaturalTransform.gf
index e7da79b93..60943737c 100644
--- 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 ;
 
 }