From mboxrd@z Thu Jan  1 00:00:00 1970
X-Received: by 10.107.135.195 with SMTP id r64mr4238293ioi.19.1466087579010;
        Thu, 16 Jun 2016 07:32:59 -0700 (PDT)
X-BeenThere: homotopytypetheory@googlegroups.com
Received: by 10.157.14.29 with SMTP id c29ls526565otc.10.gmail; Thu, 16 Jun
 2016 07:32:58 -0700 (PDT)
X-Received: by 10.157.41.201 with SMTP id g9mr30936otd.7.1466087578578;
        Thu, 16 Jun 2016 07:32:58 -0700 (PDT)
Return-Path: <marc....@gmail.com>
Received: from mail-qk0-x233.google.com (mail-qk0-x233.google.com. [2607:f8b0:400d:c09::233])
        by gmr-mx.google.com with ESMTPS id h76si688329ywc.7.2016.06.16.07.32.58
        for <HomotopyT...@googlegroups.com>
        (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128);
        Thu, 16 Jun 2016 07:32:58 -0700 (PDT)
Received-SPF: pass (google.com: domain of marc....@gmail.com designates 2607:f8b0:400d:c09::233 as permitted sender) client-ip=2607:f8b0:400d:c09::233;
Authentication-Results: gmr-mx.google.com;
       dkim=pass head...@gmail.com;
       spf=pass (google.com: domain of marc....@gmail.com designates 2607:f8b0:400d:c09::233 as permitted sender) smtp.mailfrom=marc....@gmail.com;
       dmarc=pass (p=NONE dis=NONE) header.from=gmail.com
Received: by mail-qk0-x233.google.com with SMTP id c73so54411110qkg.2
        for <HomotopyT...@googlegroups.com>; Thu, 16 Jun 2016 07:32:58 -0700 (PDT)
DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed;
        d=gmail.com; s=20120113;
        h=mime-version:in-reply-to:references:from:date:message-id:subject:to
         :cc;
        bh=522W1753xU3M6dkfGb7Iwmkwftn3qiHcKXCOsjDP7Oo=;
        b=XxsLOEUYd9dtRJoDJWF4R7PenrXhfrbFjdwbEtsTqx5WFUOA9RlaffhNu812FhGqR7
         akRNArk1LNCFEW4uP0y8KHFmzxUXirkHWuecaEI4a6tpBswH1+klNDCkgvI06RrvWf0A
         apgk/2aClpzhERfXxIatV3gfPkrI7/aJLOLowT6kNTXm6kubp1hE2oxDZno2ZWkBxPYW
         IxGtVTC2P0C9L10sWn8YfyhYrHGO69ZKMbEP4q0nYAYbHjrW2+5XG1zA/dxcMFICCxPA
         3roPqxPDSMTEAen1AoO8iBx9tF4CQSLlI2qbNKWlLm2gAZeWmi1pnHHlwyedGtjvsn/W
         WFZw==
X-Gm-Message-State: ALyK8tKYJd0a40TE3gBY1w209xqR8MzpV6JRBqofBCNxFf+4QRUtoK7Gn/0bQlk9N0ROLqcN61NRnw8+KtiYSw==
X-Received: by 10.200.39.142 with SMTP id w14mr5236338qtw.59.1466087578408;
 Thu, 16 Jun 2016 07:32:58 -0700 (PDT)
MIME-Version: 1.0
Received: by 10.237.38.71 with HTTP; Thu, 16 Jun 2016 07:32:57 -0700 (PDT)
In-Reply-To: <CAHPPr6zVU0AKD5XeGjj=ks5vRb+tuGdidPK2CNJKb8KCZt4KdA@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>
From: Marc Bezem <marc....@gmail.com>
Date: Thu, 16 Jun 2016 16:32:57 +0200
Message-ID: <CAJU3+YWeXJLezUgv1dv92rEzDn3n-LxY2LJiLRWxyaJZw+6W_A@mail.gmail.com>
Subject: Re: [HoTT] Is synthetic the right word?
To: =?UTF-8?Q?andr=C3=A9_hirschowitz?= <a...@unice.fr>
Cc: Andrej Bauer <andrej...@andrej.com>, 
	Homotopy Type Theory <HomotopyT...@googlegroups.com>
Content-Type: multipart/alternative; boundary=001a11c13dcc5243590535661d0e

--001a11c13dcc5243590535661d0e
Content-Type: text/plain; charset=UTF-8

"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."

What are "usual spheres" given that any classical theory of real numbers
also has non-standard models?

Marc

--001a11c13dcc5243590535661d0e
Content-Type: text/html; charset=UTF-8

<div dir="ltr"><div><div>&quot;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.&quot;<br><br></div>What are &quot;usual spheres&quot; given that any classical theory of real numbers also has non-standard models?<br><br></div>Marc<br><div><div><br><div class="gmail_extra"><br></div></div></div></div>

--001a11c13dcc5243590535661d0e--