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

[Thomas Streicher <stre...@mathematik.tu-darmstadt.de>]

Now at first sight it looks as if doing toposes in a univalent
metatheory makes them inconsistent in the sense that all toposes are
trivial.

But, luckily, that is not the case. If a and a' are in A then (a,refl(a))
and (a',refl(a')) are in Single(a) and Single(a') respectively. These
types are certainly isomorphic but not judgementally equal. You can project
(a,refl(a)) on a and (a',refl(a')) to a' by applying DIFFERENT first
projection functions pi and pi' respectively. But you cannot apply pi'
to (a,refl(a)) before having it transformed into an object of Single(a')
along an iso between Single(a) and Single(a'). Thorsten has claimed
that this were possible in LEAN but it shouldn't!

Here is an excerpt from Thorsten's original mail

> Hence by extProp
>
>   extProp p : Single(true) = Single(false)
>
> now we can use transport on (true,refl) : Single(true) to obtain
>
>   x = (extProp p)*(true,refl) : Single(false)
>
> and we can show that
>
>   second x : first x = false
>
> but since Lean computationally ignores (extProp p)* we also get
> (definitionally):
>
>   first x == true
> 

he clearly says that "since Lean computationally ignores (extProp p)*"

but that is balatantly wrong since it mixes judgemental and propositional
equality.

And there we are back to what I originally said. Of course, {a} and {a'} are
isomorphic and thus equal as elements of P(A) if we postulate UA for P(A).
Thus we shouldn't!

Another gap in Thorsten's argument is the following. Though Single(a) and
Single(a') are isomorphic in order to conclude that they are propositionally
equal they would have to be elements of a univalent universe BUT I don't see
where such a universe should come from in the general topos case!

Thomas