[Agda] Classical Mathematics for a Constructive World
Dan Licata
drl at cs.cmu.edu
Tue Nov 27 01:05:23 CET 2012
On Nov26, Martin Escardo wrote:
> Notice that HoTT proves the negation of excluded middle, which MLTT
> doesn't. But you can have the negation of DNS together with the negation of
> EM, I believe. I believe the DNS may hold in suitable HoTT models, as
> continuity is one of the assumptions that give DNS.
Maybe I missed this earlier in the thread, but what exactly do you mean
by "negation of EM"? I thought you would mean "double-negation of EM",
but
em : {A : Set0} -> ((Either A (A -> Void0)) -> Void0) -> Void0
em f = f (Inr (\ x -> f (Inl x)))
seems to work in plain MLTT.
I'd like to understand exactly what statement is true in HoTT but not
plain MLTT.
Thanks!
-Dan
More information about the Agda
mailing list