Re: [HoTT] Is synthetic the right word?

[Eric Finster <ericf...@gmail.com>]

[-- Attachment #1: Type: text/plain, Size: 2209 bytes --]

>
> The Blakers-Massey theorem has *interesting* interpretations in other
> oo-toposes.
>

At least in the case which I know best, that of interpreting the theorem in
the
presheaf topos [Fin_*, S] of functors on finite, pointed spaces to spaces,
I don't think I would say that the interpretation is more interesting: it
is just
interpreted pointwise.

It is rather the interaction of the theorem with another set of modalities
in
[Fin_*, S] which I think is interesting, and gives some new results.

But since this topos lies outside of the realm in which we can interpret
univalent
type theory right now, we still have to rely on the infty-categorified
proof to
say that we indeed know the theorem holds.

Eric


>
> On Thu, Jun 16, 2016 at 4:07 PM, andré hirschowitz <a...@unice.fr> wrote:
> > 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
> >
> >
> >
> > --
> > 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.
>
> --
> 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.
>

[-- Attachment #2: Type: text/html, Size: 3266 bytes --]