Two Queries about Univalent Foundations

[Timothy Y. Chow]

Joe Shipman wrote:
> I'm sorry, Kevin, but this seems to miss both of the points I was 
> making.

Technically, yes; but I think Kevin's point is that your questions, or at 
least the first question, somehow misses the point of univalent 
foundations.

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.

https://math.andrej.com/2014/01/13/univalent-foundations-subsume-classical-mathematics/

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.

Tim