There may be some confusion about univalence and equality of subsets

of a type. 

Univalence is compatible with the fact that two subsets A,B of a type

X are equal iff they have the same elements.

In fact, univalence implies that.

Define Prop=Σ(P : U),isProp P where isProp(P:U) = Π(x,y:P),x=y. This

is a large type (it lives in the same universe as U, rather than in

U). You may wish to make this small (like in UniMath), or not, but

this is orthogonal to this discussion.

Then define the powerset of a type X by ℙ X = X → Prop.

(As in topos theory.)

Then for A : ℙ X and x : X we write x ∈ A to mean A x.

(As in the internal language of a topos.)

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

Without assuming univalence, we can't prove (or disprove) this

equality. Not in intensional MLTT, or even in so-called extensional

MLTT (= intensional MLTT + equality reflection). This is because in

order to prove this equality, we need both functional and

propositional extensionality. Extensional MLTT has the former but not

the latter. Univalent MLTT has both.

Here, the quantifier ∀ is a function of type (X → Prop) → Prop and the

logical connective _⇔_ is a function Prop → Prop → Prop (or Prop ×

Prop → Prop, it doesn't matter).

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.

Example: X=ℕ, A=isEven and B=isOdd. Then A ≠ B but A'=B' (because A'

and B' are isomorphic sets).

However, we do have that

  ℙ X ≃ Σ (A' : U), Σ (e : A' → X), isEmbedding e,

where (isEmbedding e) means that the fibers of e are propositions.

Then the elements (Σ isEven, (_ , _)) and (Σ isOdd, (_ , _)) of the

rhs type, for uniquely determined "_", are different, even though the

types Σ isEven and Σ isOdd are equal.

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.

Best,

Martin