[Agda] Are there unicorns in Agda?

[Jacques Carette]

On 12-02-10 11:38 AM, Martin Escardo wrote:
>
> Similarly, the space Q={(x,m,n) in R x Z x N | x=m/(n+1) and gcd(m,n)=1}
> is discrete, even though the first projection into R is a 
> monomorphism. This is what the topological-topos compiler produces 
> when you take the subspace of rational numbers. In practice, it 
> becomes discrete because you can decide equality on Q. (As you showed 
> above in your example.)

This is a nice explanation of the fundamental reason that symbolic 
computation systems (Maple, Mathematica, Sage, ...) are so effective.  
They generally consider spaces that involve the pair (complex, algebraic 
numbers), but the point is the same: equality of algebraic numbers is 
decidable.  In fact, one ought to be able to extend this a little 
further, as long as one can uniformly bound the computations [in terms 
of the length of the description of the numbers] for deciding equality.

Nicely, this generalises to some spaces of functions too - this is why 
the theory of 'holonomic' functions is so rich, as they possess 
decidable equality.

Jacques