From mboxrd@z Thu Jan  1 00:00:00 1970
X-Received: by 10.66.232.227 with SMTP id tr3mr3641365pac.45.1466088121930;
        Thu, 16 Jun 2016 07:42:01 -0700 (PDT)
X-BeenThere: homotopytypetheory@googlegroups.com
Received: by 10.157.20.228 with SMTP id r33ls535237otr.92.gmail; Thu, 16 Jun
 2016 07:42:01 -0700 (PDT)
X-Received: by 10.157.35.12 with SMTP id j12mr47374otb.29.1466088121434;
        Thu, 16 Jun 2016 07:42:01 -0700 (PDT)
Return-Path: <urs.sc...@googlemail.com>
Received: from mail-vk0-x22f.google.com (mail-vk0-x22f.google.com. [2607:f8b0:400c:c05::22f])
        by gmr-mx.google.com with ESMTPS id r140si1730081vkf.0.2016.06.16.07.42.01
        for <HomotopyT...@googlegroups.com>
        (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128);
        Thu, 16 Jun 2016 07:42:01 -0700 (PDT)
Received-SPF: pass (google.com: domain of urs.sc...@googlemail.com designates 2607:f8b0:400c:c05::22f as permitted sender) client-ip=2607:f8b0:400c:c05::22f;
Authentication-Results: gmr-mx.google.com;
       dkim=pass head...@googlemail.com;
       spf=pass (google.com: domain of urs.sc...@googlemail.com designates 2607:f8b0:400c:c05::22f as permitted sender) smtp.mailfrom=urs.sc...@googlemail.com;
       dmarc=pass (p=QUARANTINE dis=NONE) header.from=googlemail.com
Received: by mail-vk0-x22f.google.com with SMTP id u64so76008856vkf.3
        for <HomotopyT...@googlegroups.com>; Thu, 16 Jun 2016 07:42:01 -0700 (PDT)
DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed;
        d=googlemail.com; s=20120113;
        h=mime-version:in-reply-to:references:from:date:message-id:subject:to
         :cc;
        bh=EIJliGJfqZIfOTJRym6nYvd2vLrJgMGpMWx3r7PYPGI=;
        b=u6veRNIAwelCG96nsE+FyyfgEN26DaT3Z2tBtp+OcT4QiRIEwYic4fIi1Qq96xgHoQ
         AowZ6Wh64EtGK7BZUdTp4AtTxDlAofbjThubTpf20Ies0jDlFgCw1GL2tFu5bqH7Iw0z
         Z9icjhWbcN6mjRToiByYjssaf0FFvIjls0e9DLyXSXXAN9M9Mun3WylNcenY4U6+ZpTv
         4Cpmiq53FfX6XP2ERjQwdM3qXEmLq2HC5kY736oJAa6XS7k0JrNFZZwq7rEi+owst/VT
         2z6xtFmQeopczInIi+s7h1fTZastO9z+WHNBZpirDY0XwcHORbXYezw7hldyB71uzkKt
         JTLA==
X-Gm-Message-State: ALyK8tKHrGJxfAyDasRsz+yqZYy49M+jrYXZYT2suGpJ9V3DtqYVf7qc8q5B3kQON5WRg9kn9ZDqhO17EgyDaQ==
X-Received: by 10.31.217.129 with SMTP id q123mr2255084vkg.102.1466088121113;
 Thu, 16 Jun 2016 07:42:01 -0700 (PDT)
MIME-Version: 1.0
Received: by 10.103.88.140 with HTTP; Thu, 16 Jun 2016 07:42:00 -0700 (PDT)
In-Reply-To: <CAOoPQuS0FR4FeZfpxM2RMFkyFOa0XintNLs=TxAE7NnM5g_OJw@mail.gmail.com>
References: <e1248ef7-cf62-4bde-accc-c8a7b135501b@googlegroups.com>
 <8C57894C7413F04A98DDF5629FEC90B138B93747@Pli.gst.uqam.ca>
 <CAHPPr6wawT-R7eXjKca7Cx3zE-9jdM7HOkqgMOrHKt-RD5W4Cw@mail.gmail.com>
 <2850536B-0DB8-4F6D-AB3F-D5C28F6855B4@cmu.edu> <CAHPPr6yvYwQzOgbBZA1kDqm=6SQ601xBEWYeHqRw3H62zyJA_A@mail.gmail.com>
 <CAB0nkh1uyh_xC_zX3Fpb-Ec_Gjrgi=puZfEWgf4oWKjWy7TFrA@mail.gmail.com>
 <CAHPPr6zVU0AKD5XeGjj=ks5vRb+tuGdidPK2CNJKb8KCZt4KdA@mail.gmail.com> <CAOoPQuS0FR4FeZfpxM2RMFkyFOa0XintNLs=TxAE7NnM5g_OJw@mail.gmail.com>
From: Urs Schreiber <urs.sc...@googlemail.com>
Date: Thu, 16 Jun 2016 16:42:00 +0200
Message-ID: <CA+Kbugfs0ZmTGq2mp5Xrm74-vGWFT2mnvW26+2N33qB6KwxFwA@mail.gmail.com>
Subject: Re: [HoTT] Is synthetic the right word?
To: Bas Spitters <b.a.w.s...@gmail.com>
Cc: =?UTF-8?Q?andr=C3=A9_hirschowitz?= <a...@unice.fr>, 
	Andrej Bauer <andrej...@andrej.com>, 
	Homotopy Type Theory <HomotopyT...@googlegroups.com>
Content-Type: text/plain; charset=UTF-8

> The Blakers-Massey theorem has *interesting* interpretations in other
> oo-toposes.
> Are you suggesting that the same may be true for the synthetic results
> that have been proved about spheres?
> The consensus seemed that be that that was not the case (yet?).

Indeed, for spheres the case is not so interesting..This is because,
at least in Grothendieck infinity-toposes H, then the fact that the
inverse image functor

  H <--- S

from the base S (left adjoint to global section) preserves all
homotopy colimits and finite homotopy limits,  means that the usual
spheres in H coincide with the usual spheres in S.

But synthetic homotopy theory is not only about spheres.