From mboxrd@z Thu Jan  1 00:00:00 1970
X-Received: by 10.107.128.160 with SMTP id k32mr4035542ioi.20.1466083987043;
        Thu, 16 Jun 2016 06:33:07 -0700 (PDT)
X-BeenThere: homotopytypetheory@googlegroups.com
Received: by 10.36.60.150 with SMTP id m144ls637876ita.20.gmail; Thu, 16 Jun
 2016 06:33:06 -0700 (PDT)
X-Received: by 10.66.41.81 with SMTP id d17mr3466494pal.31.1466083986327;
        Thu, 16 Jun 2016 06:33:06 -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 v190si21059vkf.2.2016.06.16.06.33.06
        for <HomotopyT...@googlegroups.com>
        (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128);
        Thu, 16 Jun 2016 06:33:06 -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 d185so70978103vkg.0
        for <HomotopyT...@googlegroups.com>; Thu, 16 Jun 2016 06:33:06 -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=yHSlNzl9yrWiTOzgh2vEn1UpEobC2zOt1nT0VulBmSA=;
        b=a98kfNt6b+I70X5W1RErhyQTrkGtMSJ/JB8f05ckFQh8mz96JsPz+wA5dfREqrPCzM
         yGpDOXNEIs/ABpA1WXE14r+CqkhMsOhvq2jjfMxJXrfs8Tr2VmD1gWBDDnCVuJDODaMx
         FNf8EQGSgARbI7S4HvNvMcW4Nkk1gSfkqwIyvjmp1dYjaWwephr1zZ1L8LxV+kpY6V2p
         LvCB45BRr/5l2Zn/Byos70GhwqPqtj7MsdhUnx3DU6w19T9N8VHs8Omt1cYPyjasFVDk
         xVT6xM55eacfxtmHwiwFbQ46vUGe9cXCtmAxEQomnB2kDhD32svaevxTrhnq3vfb63zr
         hCng==
X-Gm-Message-State: ALyK8tJ3My9bWRs7iOZJ165An5tWjvMOPhMO7dzqRgzMdPyFOmNE60XjkcOPnJHStbt8kRAoAadI/Q01d0vQFA==
X-Received: by 10.31.191.76 with SMTP id p73mr2041792vkf.11.1466083986030;
 Thu, 16 Jun 2016 06:33:06 -0700 (PDT)
MIME-Version: 1.0
Received: by 10.103.88.140 with HTTP; Thu, 16 Jun 2016 06:33:05 -0700 (PDT)
In-Reply-To: <CAOoPQuRQkbTz587BENVu9Hhu=_ubnn2rsF4e=0_UQ=O_DYWJwQ@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>
 <CAOoPQuRQkbTz587BENVu9Hhu=_ubnn2rsF4e=0_UQ=O_DYWJwQ@mail.gmail.com>
From: Urs Schreiber <urs.sc...@googlemail.com>
Date: Thu, 16 Jun 2016 15:33:05 +0200
Message-ID: <CA+Kbugf5zMOVSFRxGur=ehfkF9PWERqfiiai=E9ybPE7L0ckkg@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>, 
	Steve Awodey <awo...@cmu.edu>, =?UTF-8?Q?Joyal=2C_Andr=C3=A9?= <joyal...@uqam.ca>, 
	Homotopy Type Theory <HomotopyT...@googlegroups.com>
Content-Type: text/plain; charset=UTF-8

> It is "the same" in the standard model, but the theorem in HoTT gives
> a more general result than the one in classical homotopy.

Indeed, and this is usefully compared to the original use of
"synthetic" in "synthetic geomety":

Euclid's synthetic axioms for geometry (without the parallel axiom)
were thought to apply only to classical flat Euclidean space. The
surprise was immense when it was realized that the same synthetic
geometry has interpretation also in hyperbolic geometry and in
elliptic geometry.

That is the prospect of synthetic homotopy theory: to be for homotopy
theory what the generalization from flat to curved spaces has been for
geometry.