[pron]

> but propositions are too rich to support finite equality

Why do you say that? The finitary deduction rules of all logic systems provide both equivalence (<=>) and partial order (=> or |-) relations. Classical logic gives rise to a boolean algebra, while intuirionistic logic forms a Heyting algebra, of which boolean algebra is a special case. The latter is more general, but both are bounded lattices, and both are perfectly fine.

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