Jason (jcreed) wrote,


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}
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

  • (no subject)

    Saw Mike Birbiglia's "Thank God for Jokes" with K in a little theater on bleeker. Funny show. I highly recommend his show "My girlfriend's boyfriend"…

  • (no subject)

    Second city yesterday was really funny. We got shoved in a front-row seat and picked on to provide detailed improv prompts for a big log improv…

  • (no subject)

    It was a shitty rainy night so we stayed in and ate italian and watched " Dress to Kill", which was pretty excellent. I already kind of knew most the…

  • Post a new comment


    Anonymous comments are disabled in this journal

    default userpic

    Your reply will be screened

    Your IP address will be recorded