[Agda] Classical Mathematics for a Constructive World

[Martin Escardo]

On 27/11/12 09:16, Altenkirch Thorsten wrote:
>
>
> On 26/11/2012 20:21, "Martin Escardo" <m.escardo at cs.bham.ac.uk> wrote:
>
>> Coquand and Spivak have shown that MLTT remains strongly normalizing if
>> you add recursion schemes such as the one used to give a proof term for
>> the double-negation shift.
>
> Do you mean DNS for Nat or is there a generic one?

Only for Nat. More generally DNS can be given a proof term for a variety 
of discrete types, such as CoNat->Nat, where discrete means decidable 
equality.

But beyond discrete types, postulating DNS renders your entire system 
classical.

Best,
Martin