Timeline for Type with $X\rightarrow X\cong X + 1$

5 events

when toggle format	what		by	license	comment
Feb 19, 2014 at 17:48	vote	accept	Luke
Dec 23, 2013 at 5:52	comment	added	Qiaochu Yuan		(I think the reason the details were more complicated than I expected is the following. The above line of reasoning suggests that $\mathbb{N}^{\mathbb{N}}$ should even be computably in bijection with $\mathbb{N}$. But if this is the case then the Lawvere fixed point theorem implies that every computable function $\mathbb{N} \to \mathbb{N}$ has a fixed point, which is clearly false. I think some fiddling around with partial functions is necessary to fix this. Probably Andrej Bauer knows the real story here.)
Dec 23, 2013 at 5:47	comment	added	Qiaochu Yuan		The following should morally be an example, but I don't know how to make it precise (I read some things about it once but the details were way more complicated than I expected). Find a topos, something like a topos of computable functions, where $\mathbb{N}^{\mathbb{N}}$ consists of the computable functions $\mathbb{N} \to \mathbb{N}$. These can be computably enumerated, so $\mathbb{N}^{\mathbb{N}}$ should be computably in bijection with $\mathbb{N} + 1$.
Dec 22, 2013 at 23:40	answer	added	Andreas Blass		timeline score: 7
Dec 22, 2013 at 23:06	history	asked	Luke	CC BY-SA 3.0