On Friday, December 22, 2017 at 4:20:21 PM UTC-5, Martín Hötzel Escardó wrote:

There may be some confusion about univalence and equality of subsets

of a type. 

[...]

Now, from a subset A : ℙ X, we get a type A' and an embedding A' → X.

(The construction works like this: we have A : X → Prop, and a

projection Prop → U. Then the type A' is the sum (Σ) of composite

function. The embedding is the first projection.)

It is definitely not the case that if A'=B' for A,B : ℙ X then A=B.

[...]

All the misunderstandings in the previous messages are caused by

looking at the particular type X=1 without enough care.

And I think this is what Thomas is pointing out.