Correction (that you already spotted, of course):

On Friday, 22 December 2017 21:20:21 UTC, Martín Hötzel Escardó wrote:

Then, assuming univalence, we have (theorem of intensional MLTT+UA):

  (A=B) = ∀(x:X), x ∈ A ⇔ x ∈ B.

(Because the middle equality is that of two sets, we don't need to
worry about which specific equality we pick - there is at most
one. This again relies on univalence.)

It is an equality of two *propositions*, of course, which is what I meant to say.

M.