[Agda] termination proofs

[Peter Hancock]

> The countability grounds is not relevant here, because I asked about an
> _algorithmic_ map in  Nat -> Nat.

For me, a function just *is* an algorithmic map which we can recognise as total.
The normal Cantor diagonalisation argument shows that Nat->Nat is uncountable.

I admit, this will seem strange at first, because there are only countably
many Turing machines, and the total ones will be a subset of these.  But
the notion of a cardinal is a bit strange constructively.  There are
arbitrarily many subsets of a singleton, constructively.  I suggest that
this argument is worth a bit more of your attention.

(I also admit I am sweeping some subtle points under the carpet.)

Regards,

Peter