From: Andrej Bauer <andrej...@andrej.com>
To: Homotopy Type Theory <HomotopyT...@googlegroups.com>
Subject: Re: [HoTT] Is synthetic the right word?
Date: Thu, 16 Jun 2016 14:15:03 +0100 [thread overview]
Message-ID: <CAB0nkh1uyh_xC_zX3Fpb-Ec_Gjrgi=puZfEWgf4oWKjWy7TFrA@mail.gmail.com> (raw)
In-Reply-To: <CAHPPr6yvYwQzOgbBZA1kDqm=6SQ601xBEWYeHqRw3H62zyJA_A@mail.gmail.com>
On Thu, Jun 16, 2016 at 2:04 PM, andré hirschowitz <a...@unice.fr> wrote:
> I am afraid of the discussion which could follow if I try to argue that the
> 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
next prev parent reply other threads:[~2016-06-16 13:15 UTC|newest]
Thread overview: 30+ messages / expand[flat|nested] mbox.gz Atom feed top
2016-06-15 18:26 andré hirschowitz
2016-06-15 23:13 ` [HoTT] " Joyal, André
2016-06-16 8:56 ` andré hirschowitz
2016-06-16 12:37 ` Steve Awodey
2016-06-16 13:04 ` andré hirschowitz
2016-06-16 13:15 ` Andrej Bauer [this message]
2016-06-16 13:35 ` Steve Awodey
2016-06-16 14:07 ` andré hirschowitz
2016-06-16 14:15 ` Bas Spitters
2016-06-16 14:38 ` Eric Finster
2016-06-16 17:07 ` Thierry Coquand
2016-06-16 17:51 ` Eric Finster
2016-06-16 17:58 ` Thierry Coquand
2016-06-16 18:18 ` Urs Schreiber
2016-06-16 18:41 ` Eric Finster
2016-06-16 14:42 ` Urs Schreiber
2016-06-16 16:55 ` andré hirschowitz
2016-06-16 14:32 ` Marc Bezem
2016-06-16 14:50 ` Steve Awodey
2016-06-16 13:16 ` Bas Spitters
2016-06-16 13:33 ` Urs Schreiber
2016-06-16 15:03 ` Joyal, André
[not found] ` <CAOvivQyNdvTLN5f8e8OikWbCKye0fk7ZocGVMfLkWL+5moBaxw@mail.gmail.com>
2016-06-16 16:28 ` Joyal, André
2016-06-16 16:52 ` Cale Gibbard
2016-06-16 10:27 ` Andrej Bauer
2016-06-16 11:08 ` Nicola Gambino
2016-06-16 11:17 ` Cale Gibbard
[not found] ` <5762889C.8080401@cs.bham.ac.uk>
2016-06-16 19:18 ` Martin Escardo
2016-06-16 20:02 ` Egbert Rijke
2016-06-16 21:41 ` Joyal, André
Reply instructions:
You may reply publicly to this message via plain-text email
using any one of the following methods:
* Save the following mbox file, import it into your mail client,
and reply-to-all from there: mbox
Avoid top-posting and favor interleaved quoting:
https://en.wikipedia.org/wiki/Posting_style#Interleaved_style
* Reply using the --to, --cc, and --in-reply-to
switches of git-send-email(1):
git send-email \
--in-reply-to='CAB0nkh1uyh_xC_zX3Fpb-Ec_Gjrgi=puZfEWgf4oWKjWy7TFrA@mail.gmail.com' \
--to="andrej..."@andrej.com \
--cc="HomotopyT..."@googlegroups.com \
/path/to/YOUR_REPLY
https://kernel.org/pub/software/scm/git/docs/git-send-email.html
* If your mail client supports setting the In-Reply-To header
via mailto: links, try the mailto: link
Be sure your reply has a Subject: header at the top and a blank line
before the message body.
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox;
as well as URLs for NNTP newsgroup(s).