# Progress towards a computational interpretation of the univalence axiom?

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?

• IIRC the univalence axiom is a theorem in at least some of the cubical type theories, and there are proof assistants implementing these (eg $\mathsf{\color{Red}{red}PRL}$ redprl.org/en/latest but also 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. – David Roberts Oct 23 '18 at 5:01
• @DavidRoberts If you'll excuse the interruption, is Brunerie's number newspeak 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? – Robert Furber Oct 23 '18 at 22:07
• @RobertFurber yes, it is that $n$—in the guise of $\pi_4(S^3)$—but instead of $\pi_4(S^3)$ one has $||\Omega^4 S^3||_0$ where all these things are defined in HoTT: $S^3$ is a suitable suspension of the higher inductive type $S^1$, loop spaces are function types and $||\cdot||_0$ is the 0-truncation. In the model in Kan complexes this is indeed the classical thing, but in other models $S^3$, for instance, is not the (homotopy type of the) 3-sphere. – David Roberts Oct 24 '18 at 0:23
• @RobertFurber However, it should be pointed out that it is in fact known that this $n=2$ in all models 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. – Mike Shulman Oct 24 '18 at 7:45
• Thank you for the explanations, David Roberts and Mike Shulman (the MathOverflow software doesn't let me notify two people at once). – Robert Furber Oct 24 '18 at 18:24