Post #1846791

2026-04-26 15:53 UTC

@jonmsterling I think that univalence has a few aspects that hurt its prospects for canonization: 1) It can seemingly only be formulated in MLTT. Other principles (e.g. most of the weak forms of choice) that people add to weak formal systems can generally be reformulated for any reasonable base system. There's a big difference between thinking "MLTT is interesting, some logicians should study it" and "all of mathematics should rely on principles that can seemingly only be formulated in MLTT". 2) Standard constructions of models establish conservativity of univalence over the base theory for arithmetic (and a bit more?). I think there would need to be a better understanding of the mathematical impact of the truly new consequences of univalence (rather than just proofs that are shortened by using univalence). 3) The mathematicians (e.g. Jacob Lurie) doing the most fashionable new mathematics that a less informed observer might think would be a good application of univalence actually don't seem to care about it that much. I am far from an expert, but this seems related to limitations (which may be fundamental?) of expressing coherence relative to the more elaborate sets of conditions that interest mathematicians.

Replies (1)

@jonmsterling@mathstodon.xyz 2026-04-26 16:00

@zwarich I don't find the social reasons (#3) compelling. The reason Lurie doesn't care is that his work IS the development of univalent foundations, just in a different formalism and less abstractly). His goal is not to build a formalism, but to do mathematics. He has found that the best way to do mathematics is when you have object classifiers. That's the univalent point of view, period. We don't begrudge him not using type theory. It's a strength of the univalent point of view that it is equally applicable without using the type theoretic formalism. For #1, #2, I think those are more interesting points. However, I think that if the question is about "what is neutral constructive mathematics", then we probably have to be using MLTT or something univalent at the moment simply because constructive mathematics without univalence is very badly behaved. So it might be best to think of #1 as an objection to constructive mathematics, rather than an objection to univalence. But we may still yet find other univalent formalisms that work differently from MLTT. Strongly agree with #2. One thing I'd note, however, is that the question is a little subtle. A mathematician can be sure that univalence implies no actually new consequences about *sets*, for the simple reason that SET embeds fully faithfully into SPACES. On the other hand, there are questions about formal derivability in these systems that we are nowhere near answering. These are good and important questions to pursue, but I think they are questions of Mathematical Logic, more than questions of Mathematics.

Open ##1846792