[Agda] Classical Mathematics for a Constructive World

[Dan Licata]

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