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?

  • 6
    $\begingroup$ 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. $\endgroup$ – David Roberts Oct 23 '18 at 5:01
  • $\begingroup$ @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? $\endgroup$ – Robert Furber Oct 23 '18 at 22:07
  • 2
    $\begingroup$ @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. $\endgroup$ – David Roberts Oct 24 '18 at 0:23
  • 6
    $\begingroup$ @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. $\endgroup$ – Mike Shulman Oct 24 '18 at 7:45
  • 1
    $\begingroup$ Thank you for the explanations, David Roberts and Mike Shulman (the MathOverflow software doesn't let me notify two people at once). $\endgroup$ – Robert Furber Oct 24 '18 at 18:24

Cubical type theory is a variant of type theory which has all the usual (and some unusal) computational properties, and the Univalence Axiom is a theorem of cubical type theory. As was already pointed out in the comments, there are implementations of cubical type theory that one can play with (even for 90 hours).

| cite | improve this answer | |
  • $\begingroup$ Awesome! I'll check it out. Also, thanks for converting me to constructivism. Your Five Stages of Accepting Constructive Mathematics lecture/article was very convincing! $\endgroup$ – ಠ_ಠ Oct 24 '18 at 9:49
  • 4
    $\begingroup$ Whenever someone sounds very convincing you should hear a little alarm going off in your head. $\endgroup$ – Andrej Bauer Oct 24 '18 at 13:34
  • $\begingroup$ I think I snoozed my alarm this time. ;) $\endgroup$ – ಠ_ಠ Oct 24 '18 at 22:32

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.