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

Huh? Your isEven/isOdd example is fine, but there, X ≠ 1. Is it not the 
case that if A'=B' for A,B : ℙ 1 then A=B? (Note the specialization to 1.)