From mboxrd@z Thu Jan  1 00:00:00 1970
X-Received: by 10.176.1.73 with SMTP id 67mr3469172uak.8.1466082905011;
        Thu, 16 Jun 2016 06:15:05 -0700 (PDT)
X-BeenThere: homotopytypetheory@googlegroups.com
Received: by 10.140.82.227 with SMTP id h90ls1437929qgd.2.gmail; Thu, 16 Jun
 2016 06:15:04 -0700 (PDT)
X-Received: by 10.140.94.85 with SMTP id f79mr3514887qge.0.1466082904396;
        Thu, 16 Jun 2016 06:15:04 -0700 (PDT)
Return-Path: <andrej...@andrej.com>
Received: from mail-qk0-x232.google.com (mail-qk0-x232.google.com. [2607:f8b0:400d:c09::232])
        by gmr-mx.google.com with ESMTPS id h76si668471ywc.7.2016.06.16.06.15.03
        for <HomotopyT...@googlegroups.com>
        (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128);
        Thu, 16 Jun 2016 06:15:03 -0700 (PDT)
Received-SPF: neutral (google.com: 2607:f8b0:400d:c09::232 is neither permitted nor denied by best guess record for domain of andrej...@andrej.com) client-ip=2607:f8b0:400d:c09::232;
Authentication-Results: gmr-mx.google.com;
       dkim=pass head...@andrej-com.20150623.gappssmtp.com;
       spf=neutral (google.com: 2607:f8b0:400d:c09::232 is neither permitted nor denied by best guess record for domain of andrej...@andrej.com) smtp.mailfrom=andrej...@andrej.com
Received: by mail-qk0-x232.google.com with SMTP id s186so51817639qkc.1
        for <HomotopyT...@googlegroups.com>; Thu, 16 Jun 2016 06:15:03 -0700 (PDT)
DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed;
        d=andrej-com.20150623.gappssmtp.com; s=20150623;
        h=mime-version:in-reply-to:references:from:date:message-id:subject:to
         :content-transfer-encoding;
        bh=FT64LgskspeFhz/Uce0H4yB+WoIYbYnerzYmXH6SPTk=;
        b=V6RucgsCSYAniquCoZckG5pbT+4tHfbf72K9M64G/jbcn6DG2VR3qfCyABJnDr5sTo
         tLDbExw5Bk7Znko5lZkUil9h62KgZktfme4SfMzpY6wY4HC/0/H5dcEoP23wMWKcQD14
         JELjPwr9hkD8clJr9+sN/Fwx/zMzUugFqqBw1sZEF5RbHVypQ916aht2JOlVTas5Pw4O
         A8WTdqO01Fm712iMrmBiMWyU3OmnWqbrRsB0hJeDCzCJ8PyfqP6//ibeUiq2FNq6yTO3
         lj2XSaVvkl5GgcQS1mojA0Ampx+lJIDa4epRTXNAcAycRpXTh5afvojqK5aEjevgTUBR
         GqUg==
X-Gm-Message-State: ALyK8tI//0Yxk7KB+8JYQSL79cETuHae+BdSKAhfz3fMZrOZS8gscnNNSlUh2M33wmF6/FnvQvMN5Sth3xssCQ==
X-Received: by 10.233.235.83 with SMTP id b80mr4671093qkg.83.1466082903660;
 Thu, 16 Jun 2016 06:15:03 -0700 (PDT)
MIME-Version: 1.0
Received: by 10.55.27.73 with HTTP; Thu, 16 Jun 2016 06:15:03 -0700 (PDT)
In-Reply-To: <CAHPPr6yvYwQzOgbBZA1kDqm=6SQ601xBEWYeHqRw3H62zyJA_A@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>
From: Andrej Bauer <andrej...@andrej.com>
Date: Thu, 16 Jun 2016 14:15:03 +0100
Message-ID: <CAB0nkh1uyh_xC_zX3Fpb-Ec_Gjrgi=puZfEWgf4oWKjWy7TFrA@mail.gmail.com>
Subject: Re: [HoTT] Is synthetic the right word?
To: Homotopy Type Theory <HomotopyT...@googlegroups.com>
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: quoted-printable

On Thu, Jun 16, 2016 at 2:04 PM, andr=C3=A9 hirschowitz <a...@unice.fr> wro=
te:
> I am afraid of the discussion which could follow if I try to argue that t=
he
> synthetic sphere is definitely different of the classical one...

The HoTT objects, such as the circles and the spheres expressed as
HITs, may be interpreted in many different models, some of which will
give "old objects" and other "new ones". 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.

With kind regards,

Andrej