Re: [HoTT] Impredicative set + function extensionality + proof irrelevance consistent?

["Martín Hötzel Escardó" <"escardo..."@gmail.com>]

[-- Attachment #1.1: Type: text/plain, Size: 2520 bytes --]

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



[-- Attachment #1.2: Type: text/html, Size: 7723 bytes --]