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.