Yesterday, I read the following question : Finding a space such that $X\cong X+2$ and $X\not\cong X+1$, and found the result very astounding.
Does it still hold in homotopy type theory? As a type theorist, I don't really understand the answer…
I tried to redo the proof, translating it in type-theoretic words, but and I don't seem to find a description of Stone-Čech compactification easily translatable to HoTT.
Is there an analogous of SČ-compactification in homotopy type theory (or at least, a description of $\beta\mathbb N$)?
The question you linked to is, if I understand it correctly, asking about homeomorphism of topological spaces (that's what the symbol $\cong$ usually means). Types in HoTT behave like $\infty$-groupoids, which can (classically) be presented by topological spaces, but only up to homotopy equivalence. So the first question is whether for the example spaces listed, it might still be the case that $X+1\simeq X$ even though $X+1\not\cong X$. I don't know. However, if it does happen that $X+1\not\simeq X$ as well, then it will automatically be true in the "standard" model of HoTT (where types are interpreted by classical $\infty$-groupoids) that such a type exists. However, that is a very different thing from saying that such a type can be constructed inside the formal system of HoTT. In particular, the Stone-Cech compactification is an operation on topological spaces, not on $\infty$-groupoids, so there is no obvious way to give it meaning inside HoTT.