[Agda] Classical Mathematics for a Constructive World

Martin Escardo m.escardo at cs.bham.ac.uk
Tue Nov 27 01:29:44 CET 2012

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.


More information about the Agda mailing list