So at least at this level it
is a bit pointless to discuss things in absolute terms. The HoTT
proofs are *also* about the usual spheres.
I disagree with this formulation. It is not
at all pointless (with respect to positions, publications and the like)
to make clear in which sense synthetic spheres strictly encompass classical ones (and
potentially "non-euclidian" future ones).
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.