[Agda] Classical Mathematics for a Constructive World

[wren ng thornton]

On 11/25/12 5:36 PM, Peter Divianszky wrote:
> I guess "a relation between Nat and 2 for which it is not absurd that it
> is total" gives the same interpretation for classical sequences as the
> one with "weak values" in the paper "Classical Mathematics for a
> Constructive World".

The crucial thing in CMfaCW is that the function space operator is taken 
to the be the one from intuitionistic logic. That is, "=>" (in Russell's 
notation) is primitive; it is not defined via the classical "not a `or` 
b", which would be taking classical disjunction and classical negation 
as primitives.

In light of this, and since 2 is 1+1 not 1`or`1, I'm not sure how N=>2 
has anything (directly) to do with weak values?


> Is there a question about predicativity here?

Well, X->2 is essentially the same thing as a predicate on X. So the 
question of what X can be in X->2 is going to be essentially the same as 
asking what you can predicate over.

-- 
Live well,
~wren