From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 10.28.199.199 with SMTP id x190mr2938186wmf.7.1466087935172; Thu, 16 Jun 2016 07:38:55 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 10.28.30.212 with SMTP id e203ls1066649wme.38.canary; Thu, 16 Jun 2016 07:38:54 -0700 (PDT) X-Received: by 10.28.4.210 with SMTP id 201mr873847wme.6.1466087934446; Thu, 16 Jun 2016 07:38:54 -0700 (PDT) Return-Path: Received: from mail-lf0-x22d.google.com (mail-lf0-x22d.google.com. [2a00:1450:4010:c07::22d]) by gmr-mx.google.com with ESMTPS id y20si1197227lbl.1.2016.06.16.07.38.54 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Thu, 16 Jun 2016 07:38:54 -0700 (PDT) Received-SPF: pass (google.com: domain of ericf...@gmail.com designates 2a00:1450:4010:c07::22d as permitted sender) client-ip=2a00:1450:4010:c07::22d; Authentication-Results: gmr-mx.google.com; dkim=pass head...@gmail.com; spf=pass (google.com: domain of ericf...@gmail.com designates 2a00:1450:4010:c07::22d as permitted sender) smtp.mailfrom=ericf...@gmail.com; dmarc=pass (p=NONE dis=NONE) header.from=gmail.com Received: by mail-lf0-x22d.google.com with SMTP id f6so41894822lfg.0 for ; Thu, 16 Jun 2016 07:38:54 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20120113; h=mime-version:references:in-reply-to:from:date:message-id:subject:to :cc; bh=aIS4UI9vSvvK8YmuFE0baJ4qD2CU4BetVFM1Urf7mgQ=; b=au5DIwv/p9PUN3pfVJQENatMytakWC6t7JJN1X8FIRV84il46OI7VBFrs5SAYHLrVJ 7bUSAdNGtPfrVUDFS3abtfOPko+ybqdgi1OfTW3pO/yX5RQ9JJQIrY8IWL+cyr9qZTPV cKI1VB3k2xG3cAfi6NpSvHshLaAqTPu9fMq5dt+xSFxL5aHcm286kI+MhhqKxpl1fS3Y Wnsih7sRn1rSXyx3NGhOhSClv9mmTkaYk99loZW0uTiXyojL+EyEoSjvJ+vv4XWAeRPi Lkw7iUnpFSn9aqAz28N4fAEaVO4xXkQy2KWHRCFxACqmoGmcDfjCBSf4fG5Rv0JMUm1Z rQYg== X-Gm-Message-State: ALyK8tLCpPGPBfgJZEScoCJ78z4iR9M3jcLoAvnSuJG/PHIh9BfuRz/hhbl9yJW3o5KZPOPlARLpNwAJikdxnw== X-Received: by 10.46.33.152 with SMTP id h24mr1268675lji.38.1466087934213; Thu, 16 Jun 2016 07:38:54 -0700 (PDT) MIME-Version: 1.0 References: <8C57894C7413F04A98DDF5629FEC90B138B93747@Pli.gst.uqam.ca> <2850536B-0DB8-4F6D-AB3F-D5C28F6855B4@cmu.edu> In-Reply-To: From: Eric Finster Date: Thu, 16 Jun 2016 14:38:44 +0000 Message-ID: Subject: Re: [HoTT] Is synthetic the right word? To: Bas Spitters , =?UTF-8?Q?andr=C3=A9_hirschowitz?= Cc: Andrej Bauer , Homotopy Type Theory Content-Type: multipart/alternative; boundary=001a1142c1d28741370535663253 --001a1142c1d28741370535663253 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: quoted-printable > > 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=C3=A9 hirschowitz w= rote: > > 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=C3=A9 H > > > > > > > > -- > > You received this message because you are subscribed to the Google Grou= ps > > "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. > --001a1142c1d28741370535663253 Content-Type: text/html; charset=UTF-8 Content-Transfer-Encoding: quoted-printable
= 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 top= os [Fin_*, S] of functors on finite, pointed spaces to spaces,=C2=A0
<= div>I don't think I would say that the interpretation is more interesti= ng: 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 resu= lts.

But since this topos lies outside of the real= m in which we can interpret univalent
type theory right now, we s= till have to rely on the infty-categorified proof to
say that we = indeed know the theorem holds.=C2=A0

Eric
=C2=A0

On Thu, Jun 16, 2016 at 4:07 PM, andr=C3=A9 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 res= pect
> to positions, publications and the like) to make clear in which sense<= br> > synthetic spheres strictly encompass classical ones (and potentially > "non-euclidian" future ones).
>
> And instead of stressing that these HoTT proofs are *also* about the u= sual
> spheres, we should rather stress that these HoTT proofs are *not at al= l
> only* about the usual spheres.
>
> andr=C3=A9 H
>
>
>
> --
> You received this message because you are subscribed to the Google Gro= ups
> "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 &= quot;Homotopy Type Theory" group.
To unsubscribe from this group and stop receiving emails from it, send an e= mail to HomotopyTypeThe...@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.
--001a1142c1d28741370535663253--