the spheres are not a very good example of the way in which synthetic objects may differ from classical ones, since they are homotopy colimits and therefore are preserved by inverse image functors. Steve > On Jun 16, 2016, at 4:07 PM, andré hirschowitz wrote: > > Hi! > > 2016-06-16 15:15 GMT+02:00 Andrej Bauer >: > 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 > > > > > -- > You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group. > To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeThe...@googlegroups.com . > For more options, visit https://groups.google.com/d/optout .