9
$\begingroup$

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?

Improve this question
$\endgroup$
5
  • 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, 2018 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, 2018 at 22:07
  • 3
    $\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, 2018 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, 2018 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, 2018 at 18:24

2 Answers 2

Reset to default
10
$\begingroup$

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).

Improve this answer
$\endgroup$
3
  • $\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, 2018 at 9:49
  • 9
    $\begingroup$ Whenever someone sounds very convincing you should hear a little alarm going off in your head. $\endgroup$
    – Andrej Bauer
    Oct 24, 2018 at 13:34
  • $\begingroup$ I think I snoozed my alarm this time. ;) $\endgroup$
    – ಠ_ಠ
    Oct 24, 2018 at 22:32
2
$\begingroup$

The Arend programming language provides an alternative approach. It does not actually provide a computational interpretation. Instead, it provides a function converting isomorphism into a path, and it built-in a computation rule that transportation along a path constructed from univalence will reduce to the application to the function in the isomorphism. In other words, it's type theory with the following primitives (simplified for reading ease -- the actual definitions are slightly more general):

  • Isomorphism-to-path: iso : (Iso A B) -> A = B
  • Transport: coe : A = B -> A -> B
  • Computation rule coe (iso f) ==> f

If you look at the library, you'll see that even with these simple rules we can do a lot of HoTT already (from a type theoretical perspective, imagine a constructive version of MLTT with various extensionalities -- the community has done a lot with MLTT, and we can do everything there in Arend as well. Also, it has higher inductive types, so we can have some HoTT things there).

This style is similar to the HoTT-Agda library, but unlike the library, Arend doesn't introduce notions of REWRITING and stuffs -- because Agda wants to have a general notation of custom reduction rule, and Arend focus on HoTT. The underlying type theory is called HoTT-I by the author.

Improve this answer
$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.