Hi!

2016-06-16 15:15 GMT+02:00 Andrej Bauer <andrej...@andrej.com>:

> 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.

andré H