Want to take part in these discussions? Sign in if you have an account, or apply for one below
Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.
Does this general notion of extended natural numbers object appear somewhere in the literature?
I’m reminded of the object Martin Escardo likes using, the type of non-increasing boolean sequences. Classically this is the naturals plus a point at infinity. In topological models it’s the one-point compactification of N. But in computational settings it’s richer. In particular, the complement of N that sits inside is not the infinite point, but you cannot construct a term that’s not either a finite number of infinity. This sees to me to be interesting in other toposes, for instance: in the category of sheaves of a space, is the corresponding object the sheaf of continuous functions to the one-point compactification of N? In the way the Dedekind reals are the real-valued functions, and the Cauchy reals are the locally constant real functions.
1 to 3 of 3