Two Queries about Univalent Foundations

[JOSEPH SHIPMAN]

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