The n-Category Café

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.

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

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?

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.

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.

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

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.

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.

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 :-)?

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.

For somebody relatively new to the field of type theory, I have to say that the naive interpretation of univalence as ‘isomorphisms are equalities’ didn’t really make much sense to me, as equality is a function into the poset of truth values, while isomorphism is a functor into the category of sets, or a functor into the category of some set-derived structure like Ab or RMod. Neither ‘equality’ nor ‘isomorphism’ would refer to logical equivalence of propositions, nor equivalences of categories, nor 2-equivalences of 2-categories, et cetera, all of which are covered under the type theoretic identity type. The univalence axiom became clearer when I learned that identity types have an interpretation as (and are sometimes referred to as) path types, and then the interpretation becomes ‘path types are equivalent to equivalence types’. I would interpret ‘equality’ as only referring to propositional path types and ‘isomorphism’ as only referring to 0-truncated path types, as these tend to be the common usage of equality and isomorphism in everyday mathematics outside of type theory.