Two Queries about Univalent Foundations

JOSEPH SHIPMAN joeshipman at
Fri Feb 10 19:44:56 EST 2023

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

More information about the FOM mailing list