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.