[tel]

Sorry, on the propositions themselves, yes, but it's hard to internalize equality: the big sticking point between ITT, OTT, HTT, etc.

[pron]

It's only hard if you're constructive (and so all relations have to be computable, including equality).