"And instead of
stressing that these HoTT proofs are *also* about the usual spheres, we
should rather stress that these HoTT proofs are *not at all only* about
the usual spheres."
What are "usual spheres" given that any classical theory of real numbers also has non-standard models?