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