[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.
Martin
More information about the Agda
mailing list