caledon-2.0.0.0: examples/record.ncc

defn functor : (prop -> prop) -> prop
   | functorImp = {f : prop -> prop} ({a : prop }{b : prop} (a -> b -> prop) -> f a -> f b -> prop) -> functor f

defn fmap : {f} functor f => {a}{b} (a -> b -> prop) -> f a -> f b -> prop
   | getFMap = {f : prop -> prop}{fm : {a}{b} (a -> b -> prop) -> f a -> f b -> prop}
                {a : prop}{b : prop}{foo : a -> b -> prop}{fa : f a }{fb : f b }
               fm foo fa fb -> fmap foo fa fb
{-
defn identity : prop -> prop
   | cons = {a} a -> identity a

defn mapIdentity : {a}{b} (a -> b -> prop) -> identity a -> identity b -> prop
   | mapIdentityImp = {foo}{a}{b} foo a b -> mapIdentity foo (cons a) (cons b)


defn functorIdentity : functor identity
  as functorImp mapIdentity
-}