Two Queries about Univalent Foundations

[JOSEPH SHIPMAN]

The point of my questions was to see if there was any reason I personally should make the effort to learn HoTT or some other flavor of “univalent foundations”. I am not disputing that that system serves valuable purposes for other people!

My first question was about logical strength, and my impression that it can’t give any more than ZFC plus Grothendieck universes was correct; ZFC plus Grothendieck universes seems to be the limit of what is “publishable without remark”, and easily exceeds other mild strengthenings like MK, so I don’t have a reason along those lines to learn univalent foundations.

My second question was specifically about whether Homotopy Type Theory has given any new INSIGHT into homotopy groups of spheres, where “allows some to be computed that could not previously be computed” is a good proxy for “new insight”. Independently of caring about foundations and logical strength, I care about homotopy groups of spheres for purely mathematical reasons!

— JS

Sent from my iPhone

> On Feb 14, 2023, at 11:52 AM, Timothy Y. Chow <tchow at math.princeton.edu> wrote:
> 
> 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