Two Queries about Univalent Foundations

[Buzzard, Kevin M]

  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/20230212/3a8b3f38/attachment-0001.html>