Conatural Number

The conatural numbers $\mathbb{N}^{\infty}$ are the categorical dual to the Natural Numbers; EG: Final Coalgebras for the functor $1+(-)$. There are a couple of possible constructions of the conaturals:

• Via a coinductive type ala $\nu\,X.\,1+X$
• Via sequences $\mathbb{N}\to\mathbb{B}$ with at most one 0.
• Via "decreasing" sequences, EG: $\alpha:\mathbb{N}\to\mathbb{B}$ such that $\alpha(i+1)\leq\alpha(i)$.

One defining feature of the conaturals is that they have an extra point adjoined at infinity. Moreover, this point cannot be distinguished from the rest of the conaturals in constructive foundations: this is equivalent to the Limited Principle of Omniscience.

It seems like decreasing sequences are the nicest to deal with from an arithmetic POV.

Topology

The type of conaturals can be equipped with a Topology by saying that a subset $U\subseteq\mathbb{N}^{\infty}$ if whenever $\infty\in U$, there exists some finite $k$ such that $n\in U$ whenever $k\leq n$.

Arithmetic

Constructively, conaturals can be added and multiplied, relying on the fact that $(1+x)(1+y)+z=1+(xy+(x+y+z))$.

Exponentiation seems trickier: classically, we should be able to do this by defining $\infty^{1+n}=\infty$, $\infty^{0}=1$, $(n+1)^{\infty}=\infty$, $0^{\infty}=0$. However, this does not work constructively, as we cannot decide when something is $\infty$; this is equivalent to the Limited Principle of Omniscience as noted above.

Moreover, the trick we used for multiplication doesn't quite seem to work, as we can never factor out a successor, EG: ${n}^{k+2}$