Post #1846788

2026-04-26 15:27 UTC

Univalence isn't non-useful for classical mathematics, of course. For constructivists, it is useful because it allows you to do certain constructions at all. In classical mathematics, you may already have the constructions, but you may wish to show that they were independent of an arbitrary choice. That's the same principle at play, just at another level. Univalence helps here too.

Replies (4)

@zwarich@hachyderm.io 2026-04-26 15:53

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

Open ##1846791
@MartinEscardo@mathstodon.xyz 2026-04-26 15:55

@jonmsterling There is one sense in which univalence is not neutral, namely that it its about the structural view of mathematics. Although I used the term "neutral" in my 7WFTop talk in Venice, I don't think I will ever use it again. It is prone to a lot of misinterpretation. "Neutral" isn't a neutral term, I've learned from the discussion, including discussions I agree and disagree with. In my case, I was thinking in analogy with neutral geometry (Euclidean geometry without assuming the parallel postulate), which is also called "absolute geometry". Thankfully it didn't cross my mind to speak of "absolute mathematics", which would have been even worse.

Open ##1846807
@carloangiuli@mathstodon.xyz 2026-04-26 16:08

@jonmsterling Some other interesting questions: What about propositional resizing? (I guess it isn't neutral?) Also, for those understandably reluctant to call univalence neutral, is propositional univalence neutral?

Open ##1846809
@oantolin@mathstodon.xyz 2026-04-26 16:18

@jonmsterling I bet you chose the double negation in "Univalence isn't non-useful for classical mathematics" so the sentence is valid constructively, but I, as a classical mathematician, will simplify it to "univalence is useful in classical mathematics". 😛

Open ##1846842