Added redirections of conatural numbers, conat, conumber, etc. and wrote a section on formalisation in proof assistants

]]>In that sense, the set of extended natural numbers is a decategorification of the category of countable sets. Identify $0$ with the empty set, $1$ with a singleton, …, $\infty$ with a countable set. And $p$ identifies with the operation of taking the complement of a singleton in a set. Eg $p(\emptyset)$ is undefined, $p(\{0\}) = \{0\} \setminus \{0\} = \emptyset$ is empty, $p(\{0, 1\}) = \{0, 1\} \setminus \{1\} = \{1\}$ is a singleton, … and $p(\{0, 1, 2, ... \}) = \{0, 1, 2, ...\} \setminus \{0\} = \{1, 2, \dots\}$ is countable.

So $\corec_S p(a)$ is the extended natural number identified with the subset of $\{p, p\circ p, p\circ p \circ p, \cdots \}$ containing those $p \circ \cdots \circ p$ that satisfy $(p \circ \cdots \circ p)(a) \in S$. Thanks for suggesting the change, David!

]]>[Administrative note: comments #1 - #8 originally belonged to a Latest Changes thread entitled ’Extended natural numbers’. The edit announcer does not know about page name changes that were made before it came into existence, so I have manually merged that thread with this one. I also deleted a one sentence comment of Mike’s in the old thread which basically just alerted to the fact that the edit announcer had used this thread. ]

]]>I changed the wording to “the maximum number of times that $p$ can be applied in succession, starting from $a$, before being taken out of $S$” to keep 0.

]]>Or redefine so that the number counts the times that $p$ can be applied while staying within $S$.

]]>Should the extended natural numbers start with $1$ instead? It is written in the section on universal property, “You can think of $corec_S p$ as mapping an element $a$ of $S$ to the number of times that $p$ must be applied in succession, starting from $a$, before being taken out of $S$.” In particular, if $p(a) = *$ is undefined, so $p$ must be applied $1$ time before being taken out of $S$, so $\corec_S p(a)$ should be equal to $1$, right?

So it seems that $\corec_S$ takes values $1, 2, \dots$ or $\infty$.

]]>@DR

Yes, there was supposed to be $x_i$ in there; I’ve fixed it. (I also divided by $2$ twice for some reason.)

The crazy way that it looked before is another itex “feature”.

]]>@David C. 2: That’s a nice way to put it! I don’t know if I put together before the facts that the ordinary natural numbers are the well-founded objects in the extended natural numbers (the inductive type sitting inside the coinductive type), whereas $n$-categories are conveniently defined inductively for finite $n$ and coinductively for infinite $n$.

]]>I have a query on the page about the embedding in $\mathbb{R}$, because even though I made a small fix, I still don’t think I got it right.

]]>Yes! (And looping makes a monoidal $pred(n)$-category.)

]]>So we could say decategorification and looping (as decribed in Categorification)) send $n$-categories to $pred(n)$-categories for all extended natural numbers (having tidied up numbering at the lower end and doing what is necessary to allow $\ast$-categories to be images of $(-2)$-categories).

]]>I moved extended natural number system to extended natural number and expanded it. In particular, it’s now a good place to link to if you want to say that an $n$-concept from higher category theory makes sense “for any extended natural number $n$”.

]]>