[Agda] Classical Mathematics for a Constructive World

[Martin Escardo]

On 27/11/12 00:05, Dan Licata wrote:
> I'd like to understand exactly what statement is true in HoTT but not
> plain MLTT.


Let EM be the (large) type (Pi X : Type. X + ¬X).

    (1) MLTT cannot inhabit EM (of course).

    (2) MLTT cannot inhabit ¬EM (because classical ZF gives a model in
    which EM is inhabited).

So EM is independent of MLTT.

Now consider MLTT with the univalence axiom.

By Hedberg's theorem, any type with decidable equality in an hset. So, 
if EM holds, then every type is an hset.

But if univalence holds, then there are large types which are not
hsets, as is well known.

Combining these two procedures, you get an inhabitant of ¬EM.

Martin