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.