Post #1815120

2026-04-26 15:09 UTC

I increasingly find that mathematics without *either* the axiom of choice *or* the axiom of univalence is very punishing. This may be one way to rationalise the mistaken propaganda of certain people that univalence is about constructivism. It&#39;s obviously not about constructivism, but I think that constructive mathematics is probably not viable without univalence. So it&#39;s a question of who needs whom... The reason is that there are many places where you can do some construction using either the axiom of choice, or (if only something were uniquely determined) the principle of *unique* choice, which is built into neutral constructive mathematics from the start. Univalence is the thing that makes a lot more stuff uniquely determined.

Replies (1)

@jonmsterling@mathstodon.xyz 2026-04-26 15:13

The question of what "neutral constructive mathematics" should actually mean was raised recently. There's one level that you'll get sucked into discussing if you go to Padova, which is whether the principle of unique choice is neutral. With great respect and deference to the Padova school, I have to say that it is neutral, and that it is hard to conceive of a formalism in which it fails as describing *mathematics*. It may describe some other thing that is worthy of study, but not mathematics… But another level where there is a more productive discussion to be had is whether univalence is neutral. I believe that it is, because the models of both classical and constructive mathematics can always be viewed as fragments of univalent systems (e.g. by taking sheaves valued in infinity-groupoids, or by other means). It can also be given a computational interpretation, via cubical type theory, which I think satisfies another condition of neutrality. I think what "neutral constructive mathematics" means should naturally change over time as we learn new principles of reasoning. Today, I think univalence belongs in the canon.

Open ##1846786