In the article Voevodsky’s Univalence Axiom in Homotopy Type Theory, an example is given of how types are not like sets: the existence of a nontrivial (nonzero) type $X$ such that $X\rightarrow X\cong X + 1$. However, I am unable to find this counterexample in the references in the article. Does anyone know this example? Is it a special case of some more general universal property, like maybe a type $X$ with $Y\rightarrow X \cong Y +1$ for all $Y$?
2
-
2$\begingroup$ 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$. $\endgroup$– Qiaochu YuanCommented Dec 23, 2013 at 5:47
-
2$\begingroup$ (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.) $\endgroup$– Qiaochu YuanCommented Dec 23, 2013 at 5:52
Add a comment
|
1 Answer
$\begingroup$
$\endgroup$
1
I'm not ready to venture into homotopy type theory yet, but there is an example in topos theory, which might be transportable into the context you want. In the object-classifier topos, the generic object $U$ satisfies $U^U\cong U+1$. This is Example 1 in an old paper of mine, "Functions on universal algebras" [J. Pure Appl. Alg. 42 (1986) 25-28].
answered Dec 22, 2013 at 23:40
-
$\begingroup$ As I understand it, homotopy type theory is supposed to be the syntax of e.g. $(\infty, 1)$-topoi and so in particular should be interpretable in any ordinary topos. $\endgroup$ Commented Dec 23, 2013 at 5:42