Post #1846794

2026-04-26 16:40 UTC

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

Replies (2)

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

@zwarich I see what you mean… I don't think, however, that anyone has really been benefitting from this truce. The truce doesn't matter either way to classical mathematicians, because they're doing classical mathematics. The truce, however, hobbles constructive mathematics very badly. I'm not exactly interested in fighting a war or getting one over on my "enemies", so the question of whether or not changing the terms of the deal will cause war to break out don't really affect me, because I'm not and don't intend to be at war. I'm more interested in everyone having the best possible tools to do the things that interest them. I think that constructive mathematicians need this particular tool more than classical mathematicians do, but everyone can benefit from it (in the same way that inaccessible cardinals do not have a "killer app" but they clarify a lot of things). So that should be factored in when one is deciding what "neutral *CONSTRUCTIVE* mathematics" should mean.

Open ##1846795
@zwarich@hachyderm.io 2026-04-26 17:02

@jonmsterling Also, since there has recently been a lot of discourse about LLM-generated blog posts containing statements that those within the wider type theory community might consider to be unfair at best, I couldn't help but think of a parallel from 15 years ago. Voevodsky did some material harm to the reputation of univalence/HoTT early on by giving a talk espousing a very misleading understanding of Gödel's Incompleteness Theorem and proposing HoTT as a potential solution to an inconsistency in PA. It's also amusing to think back and imagine that at one point, HoTT was the darling of funding, albeit at a much different level (IAS thematic years rather than VC-backed AI startups).

Open ##1846796