Fw: Two Queries about Univalent Foundations

[Epstein, Adam]

Hi Kevin.

I hadn't realized this:
"However the majority of entries in this table are proved using techniques which rely on the analytic interpretation. The univalent people don't have access to this analytic interpretation and hence they seem to be currently far more limited in what they can prove;"

Can you be more explicit here? Which arguments do you have in mind? Presumably, "analytic" refers to the use of the actual unit interval of real numbers, as opposed to some formal categorically formulation via lifting properties? Can you signpost some operation, some long exact sequence, etc. that requires analytic tools?

Adam Epstein

________________________________
From: FOM <fom-bounces at cs.nyu.edu> on behalf of JOSEPH SHIPMAN <joeshipman at aol.com>
Sent: 12 February 2023 15:45
To: Buzzard, Kevin M <k.buzzard at imperial.ac.uk>
Cc: Foundations of Mathematics <fom at cs.nyu.edu>
Subject: Re: Two Queries about Univalent Foundations

I’m sorry, Kevin, but this seems to miss both of the points I was making.

1) I don’t care about theorems that are only relevant to particular formal systems, I care about theorems OF MATHEMATICS. It must be a goal of Univalent Foundations, even if it is not the only goal, to allow mathematicians to settle mathematical questions at least as easily or reliably or verifiably or communicable as in another foundation like ZFC, and I am only talking about *questions of mathematics which are capable both of being formalized in ZFC, and of being formalized in some system appropriate to call “univalent foundations”*. In other words, I DO INDEED insist that a concept of “the same theorem” exist, not a complete concept, but simply one which allows a *question of mathematics* to be translated into the system in such a way that a proof in the system of the translated question would be recognized as an answer to the original question of mathematics.

2) This is complicating a simple question. There is a combinatorial definition of homotopy groups that applies, such that there is no ambiguity at all about the kind of answer I am seeking: given k and n, the standard mathematical understanding of pi_k(S_n) is a certain finitely generated abelian group. I didn’t ask if homotopy type theory gives new or shorter proofs directly in particular cases, I asked if it had led to *new insights* about homotopy types applicable to the case of homotopy groups of spheres, which might lead to a faster calculation of them in a formalism completely different from HOTT.

If you aren’t getting new insights about homotopy types of spheres, are there any previously-considered-important questions about homotopy types which HOTT has led to new insights about, insights concrete enough that it’s conceivable they could allow something new to be calculated?

— JS

Sent from my iPhone

On Feb 12, 2023, at 6:27 AM, Buzzard, Kevin M <k.buzzard at imperial.ac.uk> wrote:



  1.  I am not convinced that the first question is sufficiently precise to have an answer yet. I'm not sure there is "a" system of univalent foundations. But let me punt at an answer which is valid in all systems of univalent foundations which I know about, and you can tell me if it's good enough for you. In univalent foundations you can prove X=Y if X and Y are any sets with two elements. In ZFC no proof of this is known because it's false, for example {0,1} != {0,2}. This is because the symbol `=` means totally different things in univalent foundations and ZFC. Because the two systems are using = in such different ways, one has to be extremely careful here. Your question implicitly assumes that there is some concept of "a theorem" in a univalent system and "the same theorem" in ZFC. I don't think life is so easy.


  1.  Again there is an issue here, because "Sn" can mean several different things. To the univalent people it is a synthetic higher type with an intrinsic "space structure" -- I hesitate to call it a "topology" because it is not a topology in the traditional sense of a collection of open subsets etc. Let's call this object the "combinatorial model" of Sn. To the ZFC people Sn it almost always some explicit subset of reals^{n+1}. Let's call this the "analytic model". The definition of "homotopy group" is different in both cases. For the combinatorial model, the homotopy groups are defined in a combinatorial way, valid in both ZFC and in a univalent theory. In ZFC one can also define homotopy groups of the analytic model using continuous maps from spaces like [0,1] and higher-dimensional generalisations; note that it is not possible to make a higher synthetic type accurately representing the topological space [0,1] in some flavours of univalent type theory (for example in Voevodsky's "book HoTT").

There are many theorems that one can prove about the values of homotopy groups of Sn in ZFC; see for example https://en.wikipedia.org/wiki/Homotopy_groups_of_spheres#Table_of_homotopy_groups . In ZFC the theorems apply to both the analytic model and the combinatorial model, because in ZFC both constructions make sense and one can also construct a functorial isomorphism between the two constructions of the homotopy groups. However the majority of entries in this table are proved using techniques which rely on the analytic interpretation. The univalent people don't have access to this analytic interpretation and hence they seem to be currently far more limited in what they can prove; for example they only recently managed to formally verify that pi_4(S_3)=Z/2, although a paper proof was available earlier. My understanding is that they are nowhere near the table on the Wikipedia page yet. This is not surprising, because they have strictly fewer techniques available to them.

  1.

Kevin
________________________________
From: FOM <fom-bounces at cs.nyu.edu> on behalf of JOSEPH SHIPMAN <joeshipman at aol.com>
Sent: 11 February 2023 00:44
To: Foundations of Mathematics <fom at cs.nyu.edu>
Subject: Two Queries about Univalent Foundations


*******************
This email originates from outside Imperial. Do not click on links and attachments unless you recognise the sender.
If you trust the sender, add them to your safe senders list https://spam.ic.ac.uk/SpamConsole/Senders.aspx to disable email stamping for this address.
*******************
1) What is an example of a theorem proved in the system of Univalent Foundations that can be stated in ZFC but for which no ZFC proof is known?

2) Is my impression correct that, despite this reconstruction of mathematics upon homotopy type theory, there has been no new insight gained about homotopy types that allows the kth homotopy group of Sn to be calculated faster than by previously known algorithms (in my recollection these are at least Triple Exponential Time)?

— JS

Sent from my iPhone
-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20230219/95ab701c/attachment-0001.html>