I will preface this by saying that I am not an expert on type theory. I am just a curious outsider slowly making my way through the HoTT book when I (rarely) have some spare time.

I am just curious if there has been any progress towards a computational interpretation of univalence? If not, is the general feeling that univalence is not compatible with computation?

`cubical`

github.com/simhu/cubical and`cubicaltt`

github.com/mortberg/cubicaltt). Favonia ran a computation for 90 or so hours trying to calculate Brunerie's number using Brunerie's formalised existence proof, and this proof did use univalence. $\endgroup$ – David Roberts Oct 23 '18 at 5:01Brunerie's numbernewspeak for the $n$ such that $\pi_4(S^2) \cong \mathbb{Z}/n\mathbb{Z}$ or is it a number that occurs when you generalize this fact, known for the usual homotopy category, to other homotopy categories in which homotopy type theory can be interpreted? $\endgroup$ – Robert Furber Oct 23 '18 at 22:07isin fact known that this $n=2$ inallmodels of homotopy type theory (to be more specific, in all models of Book HoTT, which is not quite the same as all models of a cubical type theory), because in addition to proving that such an $n$ exists, Brunerie proved (in Book HoTT) that $n=2$. So it's not that we don't know what it is, we just want to be able to "run" the proof of its existence (which is substantially shorter than the proof that it equals 2) to find it. $\endgroup$ – Mike Shulman Oct 24 '18 at 7:45