Jason (jcreed) wrote,
Jason
jcreed

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