In constructive mathematics, a more careful definition is required: an extended natural number is an infinite sequence of binary digits (each or ) with the property that if for any ; that is, the sequence is monotone. Then the natural number is identified with a sequence of copies of followed by s, while infinity is identified with a sequence of all s. It is not constructively valid that every natural number is either finite or infinite, but it is valid that any that is not finite is infinite, while Markov's principle is the converse.
comes naturally equipped with a map as defined below:
You can think of as mapping an element of to the number of times that must be applied in succession, starting from , before being taken out of . Since this may never occur, we need as a possible value.
Note that this universal property also holds constructively (which is why we can be sure that the constructive definition above is correct). We define constructively as follows:
We may naturally give a topology giving it the structure of a compact Hausdorff space; unusually, this works even in weak constructive foundations (without having to use the fan theorem or pass to a locale).
We may define the topology simply (and constructively) as follows: a subset of is open if, whenever , there is a finite such that whenever . In other words, is a neighbourhood of just when almost every finite number also belongs to .
In this way, is the Alexandroff compactification of the discrete space . The space is obviously compact because, given an open cover , we have for some , so alone contains almost every point, and only finitely many more open sets are needed.
It is sometimes convenient to represent as a subspace of the real line , which we can do by interpreting the natural number as and as . Constructively, the monotone bit sequence becomes the real number
which always converges. Another common representation uses instead of .
Given any topological space , an infinite sequence in may be thought of as a continuous map to from the discrete space . Then this sequence converges? iff this map can be extended to a continuous map on . For this reason, is sometimes called the universal convergent sequence. (Strictly speaking, unless is at least sequentially Hausdorff, a map to from contains more information than a sequence in with the property of convergence.)
This may all be generalised from sequences to other nets; given a directed set , we form by adjoining and taking as a neighbourhood of iff owns almost all of . (Constructively, this may require using locales for the general case.)
Concepts in higher category theory often come in -versions where is an extended natural number. (Sometimes it’s also possible to give a few negative values as well; see negative thinking.) Typically, the -version is all-encompassing, with the -versions as special cases. On the other hand, the -version is usually more familiar outside of category theory.
See also categorification.
The claim that every extended natural number is either finite or infinite is equivalent to the limited principle of omniscience () for natural numbers. On the other hand, the for extended natural numbers is simply true; given any function from to , it is either all s or has a . See Escardó (2011).