-

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.