[Agda] A proof of omniscience in Agda

[Martin Escardo]

Dear Hank,

Thanks for pointing out that my opportunities of employment are not
nil if the funding policies proceed in the direction they seem to be
going.

More seriously:

On 03/09/11 16:04, Peter Hancock wrote:
> Have you really debauched the set of natural numbers, or just made
> some other set of other things?(Smiley.)

This is a fair question. I have three answers.

Firstly, in the current Agda files I do embed ℕ into ℕ∞ so that only
one new element, namely ∞, arises, dutifully formally proved (not
because I wanted to justify this to people who might ask, but because
it is needed for the proof of the theorem (twice: once directly, and
once indirectly in the density theorem).

Secondly, in the accompanying paper cited in the Agda files I do
mention that another way of seeing ℕ∞ is as a co-inductive definition
using 0 and successor, in which you hence get the new point ∞ in the
usual well known way (as an infinite piling of successor
functions). (The first way of adding the point is that of traditional
constructive mathematics.)

Thirdly, I could have written the Agda proof using the co-inductive
definition, and in fact this is a nice exercise for people in this
list trying to understand how Agda works. The reason I didn't do that
is that there will be a next installment of the Agda proof, showing
that plenty of other subsets of the Cantor space are omniscient. For
this generalized setting, it is more convenient to have ℕ∞ in the way
I currently defined it.

Anyway, I sense that you were only joking and that you didn't really
intend me to answer this.

Best wishes,
Martin