packages feed

gf-3.1.6: examples/category-theory/NaturalTransform.gf

abstract NaturalTransform = Functor ** {

cat NT ({c1,c2} : Category) (f,g : Functor c1 c2) ;

data nt :  ({c1,c2} : Category)
        -> (f,g : Functor c1 c2)
        -> ((x : El c1) -> Arrow (mapEl f x) (mapEl g x))
        -> NT f g ;

}