[Agda] Classical Mathematics for a Constructive World

[Martin Escardo]

Small correction.

On 26/11/12 20:21, 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.

I meant to say "But you can have DNS together with the negation of EM, I 
believe."

M.