3
$\begingroup$

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$?

$\endgroup$
  • 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 Yuan Dec 23 '13 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 Yuan Dec 23 '13 at 5:52
7
$\begingroup$

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].

$\endgroup$
  • $\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$ – Qiaochu Yuan Dec 23 '13 at 5:42

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.