[Agda] A proof of omniscience in Agda

[Peter Hancock]

> However, if you enlarge the set of natural numbers with a point at
> infinity, then you get a set that constructively satisfies the
> principle of omniscience (in all varieties of constructive
> mathematics).

I'm sure it's just a presentational point, but this *sounds* like
saying

   If you eat a lot of strong cheese before bed-time, you can get
   bad dreams

which makes me feel: well, in that case, don't eat strong cheese
before bed-time.  Maybe announcing mathematical results should be different
from writing headlines for red-top newspapers. Have you really debauched the
set of natural numbers, or just made some other set of other things?(Smiley.)

Hank
(Still struggling, in a decrepit way, through your Agda....)