[Agda] Classical Mathematics for a Constructive World

[Peter Divianszky]

On 27/11/2012 23:37, Martin Escardo wrote:
>>>> Isn't the latter more "classical"?
>>>
>>> What is a classical space?
>>
>> I would use the phrase "classical space" for a space (¬ ¬ A) for some A
>> and "classical function space" for a function space (B → ¬ ¬ A). What do
>> you think about it?
>
> Spaces of the form ¬¬X have at most one element.

What a pity.

I would try then

   classical-space A
     = Sigma (A -> Set) (\P -> ¬¬ Sigma A P)

   classical-function-space A B
     = classical-space (A -> B)

   classical-sequence A
     = classical-function-space Nat A

I have to read more and compare this definition to others.

Thanks,
Peter