Two Queries about Univalent Foundations
Timothy Y. Chow
tchow at math.princeton.edu
Mon Feb 13 08:30:57 EST 2023
Joe Shipman wrote:
> I'm sorry, Kevin, but this seems to miss both of the points I was
Technically, yes; but I think Kevin's point is that your questions, or at
least the first question, somehow misses the point of univalent
The second question is fairly straightforward, at least if interpreted
literally. UF does not (currently) lead to any faster algorithms for
computing homotopy groups of spheres. The way you might hope this would
play out would be something like this: we take the simplicial set model as
given, and then compute homotopy groups of spheres "purely synthetically."
If you take this route, however, then you find that even computing the
fundamental group is harder than it is classically.
While it's not unreasonable to ask for faster algorithms as a benchmark
for progress, it's not necessarily the only way, or even the best way, to
understand whether a new theory is giving new insights about old objects.
For example, does the Lebesgue integral give us faster algorithms for
numerical integration? Not that I know of, but in some sense that's not
the only, or even the best, way of judging whether the Lebesgue integral
is buying us anything.
Your first question, if I understand it correctly, has sort of a boring
answer. To begin with, as Kevin said, there isn't a unique UF, because
there are some optional axioms. If you limit excluded middle and choice
then what you get is essentially a subset of classical mathematics. On
the other hand, I believe that by strengthening the axioms a bit you get
something like ZFC + inaccessibles, which then trivially proves something
not provable in ZFC, namely "ZFC is consistent." Some of these points are
elucidated in more detail in this blog post by Andrej Bauer.
But again, logical strength is not necessarily the right metric by which
to judge a new foundation. Is there any theorem of classical algebraic
geometry provable using schemes that is unprovable without them? No. But
that's an irrelevant question when it comes to assessing whether schemes
represent a conceptual advance.
In short, I think at the answer to these high-level questions is basically
the same as they were back in October 2014, when you asked the same
questions here on FOM. If you want an example of something people wanted
to prove before HoTT was around and whose proof was made easier by HoTT,
then Blakers-Massey still fits the bill. If you want to know whether HoTT
or UF is a superior foundation for all of mathematics, as some of its
enthusiasts claim, then the jury is still out. Even Jacob Lurie has
expressed measured skepticism about whether HoTT helps him answer the
homotopy-theoretic questions that he's interested in. Outside of
algebraic topology and algebraic geometry and the world of proof
assistants, HoTT has not had much impact.
More information about the FOM