Post #1846786

2026-04-26 15:13 UTC

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.

Replies (2)

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

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.

Open ##1846788
@jac@types.pl 2026-04-26 16:43

@jonmsterling I could see a sort of two-worlds claim that it's reasonable. Namely, one may believe that truly everything is either true or false, that axiom of choice holds, etc, and yet still distinguish truth from the notion of construction. But under unique choice these must be the same. One could of course *still* take the narrower choice that commutes \exists! and thus results in a proposition "there exists a unique function"

Open ##1846843