Skip to the Main Content

Note:These pages make extensive use of the latest XHTML and CSS Standards. They ought to look great in any standards-compliant modern browser. Unfortunately, they will probably look horrible in older browsers, like Netscape 4.x and IE 4.x. Moreover, many posts use MathML, which is, currently only supported in Mozilla. My best suggestion (and you will thank me when surfing an ever-increasing number of sites on the web which have been crafted to use the new standards) is to upgrade to the latest version of your browser. If that's not possible, consider moving to the Standards-compliant and open-source Mozilla browser.

March 1, 2018

Univalence From Scratch

Posted by Mike Shulman

Martín Escardó has written “a self-contained, brief and complete formulation of Voevodsky’s Univalence Axiom” in English and Agda:

The introduction says:

In introductions to the subject for a general audience of mathematicians or logicians, the univalence axiom is typically explained by handwaving. This gives rise to several misconceptions, which cannot be properly addressed in the absence of a precise definition.

Unlike most “introductions to the subject”, Martín is not trying to introduce homotopy type theory or univalent foundations in general; he’s just taking a geodesic route to a rigorous statement of the univalence axiom. I think this is a good supplement to the existing introductions to the subject: for someone who’s read some of those to get a “feel” for what univalence looks like, here is a fairly short and fully precise reference for exactly what it says (and doesn’t say).

Posted at March 1, 2018 12:15 PM UTC

TrackBack URL for this Entry:   https://golem.ph.utexas.edu/cgi-bin/MT-3.0/dxy-tb.fcgi/3024

16 Comments & 0 Trackbacks

arXiv version

A slightly modified version is now on the arXiv – A self-contained, brief and complete formulation of Voevodsky’s Univalence Axiom.

Posted by: David Corfield on March 7, 2018 3:18 PM | Permalink | Reply to this

Re: arXiv version

It’s not clear to me what kind of background is assumed. I looked at the paper last night. It feels like you need to have a good feel for Martin-Lof’s type theory [what is it for? what does it do?] to understand what’s being said.

Posted by: Eugene on March 7, 2018 4:57 PM | Permalink | Reply to this

Re: arXiv version

Well, as it says in the introduction,

This will be enough to illustrate the important fact that in order to understand univalence we first need to understand Martin-Löf type theory well.

I can’t speak for Martín, but I guess that maybe there are two audiences. If a reader does understand MLTT, then this is a brief and precise statement of univalence that they can understand. If a reader doesn’t understand MLTT, then the paper may at least convince them that they need to understand it before they can make informed statements about univalence.

Posted by: Mike Shulman on March 7, 2018 9:33 PM | Permalink | Reply to this

Re: arXiv version

I think I’ve just about scrambled into that first group. It’s very useful.

Posted by: David Corfield on March 7, 2018 9:53 PM | Permalink | Reply to this

Re: Univalence From Scratch

FWIW, here’s what Martín said about this paper on the HoTT list:

I have often seen competent mathematicians and logicians, outside our circle, making technically erroneous comments about the univalence axiom, in conversations, in talks, and even in public material, in journals or the web.

For some time I was a bit upset about this. But maybe this is our fault, by often trying to explain univalence only imprecisely, mixing the explanation of the models with the explanation of the underlying theory (MLTT, identity types, universe), with none of the two explained sufficiently precisely.

There are long, precise explanations such as the HoTT book, for example, or, the formalizations in Coq, Agda and Lean.

But perhaps we don’t have publicly available material with a self-contained, brief and complete formulation of univalence, so that interested mathematicians and logicians can try to contemplate the axiom in a fully defined form.

Posted by: Mike Shulman on March 7, 2018 9:30 PM | Permalink | Reply to this

Re: Univalence From Scratch

I really like the paper, I wish more people took time to write papers like this!

I have for a long time been rather skeptical of the univalence axiom from a foundational point of view. It clearly is very interesting, and it clearly is a big breakthrough when it comes to synthetic homotopy theory, and thus I am not at all disputing its importance in itself. But I’m unclear on whether it helps much in a broader foundational sense (there was for instance once a long discussion here about whether HoTT gives a synthetic theory of weak \infty-groupoids; I was, and still am, skeptical, contrary to the mainstream opinion!).

This paper gives an occasion to maybe raise this skepticism in a slightly clearer way. Martin is at pains to steer people away from a naïve interpretation of the univalence axiom. But isn’t the naïve interpretation what people really would like?

To what extent does the univalence axiom help us in practise to avoid boilerplate coherence manipulations in 2-category or 3-category theory, for instance?

Posted by: Richard Williamson on March 8, 2018 8:20 AM | Permalink | Reply to this

Re: Univalence From Scratch

Maybe the naive version is what some people would really like. But I wouldn’t fault the univalence axiom for not being an impossible different thing that some people wish it were.

Posted by: Mike Shulman on March 8, 2018 1:41 PM | Permalink | Reply to this

Re: Univalence From Scratch

Isn’t the matter a little deeper than this, though? Here are some fairly recent slides of Martín’s. Have a look at page 5 and 1. on page 6.

Now, reading that, people new to the area probably think: great! That’s just what I’m looking for! Reading Martín’s note, they may now think: OK, all is not as it may appear on first glance. Is there not a bit of a discrepancy there, that might be worth addressing?

Posted by: Richard Williamson on March 8, 2018 9:48 PM | Permalink | Reply to this

Re: Univalence From Scratch

I don’t see any discrepancy. The points made on those slides are true, nothing to do with the wrong naive interpretation. In fact the new note makes about the same point in section 3.3 note #4.

Posted by: Mike Shulman on March 8, 2018 10:24 PM | Permalink | Reply to this

Re: Univalence From Scratch

Yes, I myself know there isn’t a mathematical discrepancy, I was thinking more about how one might try to persuade somebody not interested in homotopy theory, say, that the univalence axiom is something that should interest them. Probably it would be best if someone who doesn’t really knows the details and has just seen expository/’publicity’ material chimes in.

Posted by: Richard Williamson on March 9, 2018 5:41 AM | Permalink | Reply to this

Re: Univalence From Scratch

I’m rather lost here as to what exactly you both are referring to as “the naive interpretation”.

Posted by: David Corfield on March 9, 2018 8:31 AM | Permalink | Reply to this

Re: Univalence From Scratch

I think the “naive interpretation” is “isomorphic types are equal” — technically a true statement, but only if “equal” and “isomorphic” and “types” and “are” are interpreted correctly, and someone unfamiliar with MLTT especially is unlikely to interpret them correctly.

Posted by: Mike Shulman on March 9, 2018 8:37 AM | Permalink | Reply to this

Re: Univalence From Scratch

Ah, OK. Maybe then I’m not sure why one would want the naive interpretation to be the case.

So Bill Clinton was ahead of the game:

Univalence? It depends upon what the meaning of the word ‘is’ is.

Posted by: David Corfield on March 9, 2018 9:22 AM | Permalink | Reply to this

Re: Univalence From Scratch

Univalence? It depends upon what the meaning of the word ‘is’ is.

Hehe!

Maybe then I’m not sure why one would want the naive interpretation to be the case.

Well, I think one could turn this around: if there were no significant distinction between the naïve interpretation and the real one, why did Martín write his paper :-)?

Posted by: Richard Williamson on March 9, 2018 9:50 AM | Permalink | Reply to this

Re: Univalence From Scratch

I don’t know why one would want the naive version either, but Richard seemed to think one might. The last paragraph of his first comment suggested to me that he was imagining someone thinking something like “if isomorphisms are just equalities, then maybe we can do higher category theory without bothering about all those coherences”. I don’t know whether that would be a consequence of the “naive interpretation” because the “naive interpretation” doesn’t actually make any sense (as Martin says, it’s not even false), but I can see someone perhaps leaping to that conclusion.

Posted by: Mike Shulman on March 9, 2018 10:03 AM | Permalink | Reply to this

Re: Univalence From Scratch

Yes, exactly, thanks very much for expressing it more clearly!

Posted by: Richard Williamson on March 9, 2018 2:57 PM | Permalink | Reply to this

Post a New Comment