Post #1846792

2026-04-26 16:00 UTC

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

Replies (2)

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

@zwarich Related to #1,#3, Lurie is working extremely informally, but there are other people doing higher category theory from the univalent point of view in ways that are more formal and also non-type-theoretic. So I don't think that univalence needs MLTT; the univalence axiom is usually phrased in MLTT, but it can also be expressed as the universal property of the object classifier and this makes sense even in a simply typed system.

Open ##1846793
@zwarich@hachyderm.io 2026-04-26 16:40

@jonmsterling Maybe #1 is more just an observation that a push for univalence threatens the informal truce between constructive mathematics and classical mathematics. Constructive mathematics could generally be seen as a restricted form of classical mathematics, one which admits more models, and even classical mathematicians could pay homage to the idea that these additional models had some mathematical use. Univalence inverts this relationship, making classical (SET-based) mathematics a desiccated zero-dimensional truncation of full (SPACE-based) mathematics. In order for anyone to bother disturbing a compromise like this, there needs other be some perceived benefit, which is what I was getting at with #3. If the people doing that kind of cutting-edge mathematics considered univalence essential for explaining or simplifying their work, it would probably successfully push against the natural resistance of #1. Barring that, I don't really see anyone bothering upsetting the status quo on the math side. And while #2 might mostly be a metamathematical or logical question rather than a mathematical question, many mathematicians will just ask their local logician for advice (rather than diving deeply into the subject themselves) when such questions on the boundary between the two arise.

Open ##1846794