Jason (jcreed) wrote,

More apalling chess losses. Very effectively humbling.

Doing a little work. Also trying to understand Girard's paradox better, after being reminded of it by this post and finding out that I didn't remeber it as well as I thought. Coquand's LICS'86 paper gives a definition of a universal system of notation for relations in some system as

A = ((Pi B : Type)((B->B->Prop)->Prop))->Prop
i = λB R x.x (B, R)

But I don't understand how to translate this into Martin-Löf + type:type so that all the types line up correctly.

  • (no subject)

    Guy from Seattle team we've been working with showed up today at work; no matter how much I'm generally comfortable working with remote teams (and I…

  • (no subject)

    Sean's back in town --- good fun working with nonremote teammates.

  • (no subject)

    Sean's in town at work, good times.

  • Post a new comment


    Anonymous comments are disabled in this journal

    default userpic

    Your reply will be screened

    Your IP address will be recorded