On Tuesday, 7 November 2017 21:50:24 UTC, Dimitris Tsementzis wrote:Dan,
It is an interesting idea to refer to univalence as a “mechanism” rather than an “axiom”.
Even if you did it for expository reasons, I believe that in certain contexts it is a good phrase to adopt.
I very much like this way of expression, too, even though univalence became a mechanism for the first time with cubicaltt.
Nevertheless, although Vladimir certainly didn't have a mechanism for univalence, he envisioned its possibility, and even formulated a conjecture that is still unsettled, namely that if univalence implies that there is a *number* n:N with a property P(n), then we can find, metatheoretically, using an algorithm, a *numeral* n':N (a closed term of type N) and a proof that univalence implies P(n'). No mechanism for univalence can currently provide that, as far as I know.
Martin