Jason (jcreed) wrote,
Jason
jcreed

-

Experimenting with ideas about higher-order kinds.

They're useful for defining categories in the
way I've defined pullbacks; I have (with informal notation)

cat_con : {obj : type} {mor : obj -> obj -> type}
{id : {a : obj} mor a a}
etc...
and then theoretically there would be destructors,
but I don't plan to implement them in this framework.
It's pretty damn slow, for one thing, and more importantly
there doesn't seem to be any way of eliding internal
quantifiers, which makes things horrendously difficult to
write.
Subscribe
  • Post a new comment

    Error

    Anonymous comments are disabled in this journal

    default userpic

    Your reply will be screened

    Your IP address will be recorded 

  • 0 comments