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 toworry about which specific equality we pick - there is at mostone. This again relies on univalence.)