From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 10.157.27.240 with SMTP id v45mr2855258otv.21.1466072854071; Thu, 16 Jun 2016 03:27:34 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 10.140.22.38 with SMTP id 35ls1445429qgm.98.gmail; Thu, 16 Jun 2016 03:27:33 -0700 (PDT) X-Received: by 10.31.21.129 with SMTP id 123mr2837578vkv.11.1466072853598; Thu, 16 Jun 2016 03:27:33 -0700 (PDT) Return-Path: Received: from mail-qg0-x229.google.com (mail-qg0-x229.google.com. [2607:f8b0:400d:c04::229]) by gmr-mx.google.com with ESMTPS id c2si2332286ywf.5.2016.06.16.03.27.33 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Thu, 16 Jun 2016 03:27:33 -0700 (PDT) Received-SPF: neutral (google.com: 2607:f8b0:400d:c04::229 is neither permitted nor denied by best guess record for domain of andrej...@andrej.com) client-ip=2607:f8b0:400d:c04::229; Authentication-Results: gmr-mx.google.com; dkim=pass head...@andrej-com.20150623.gappssmtp.com; spf=neutral (google.com: 2607:f8b0:400d:c04::229 is neither permitted nor denied by best guess record for domain of andrej...@andrej.com) smtp.mailfrom=andrej...@andrej.com Received: by mail-qg0-x229.google.com with SMTP id v48so25768594qgd.2 for ; Thu, 16 Jun 2016 03:27:33 -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; bh=oXyufP+wa9Xs5lNiq7cuNFlQrMAwkbbX1nIMo20qTDo=; b=KvQqMaEKLl+g84kziP4ESqJ7P/6nu4a38AO7pOYjNERSXL1mpkj6+yTRBs3ZrVP8jS 5Z24czcxv0oPHGWNb0SZbXCTQXH8zfczQpoQz6VdSNfa21v6+ntMXhgUuJru8uyIudyy Hem1jzK82sNXB/1+4oFj7h8my8knUjZBuGnEfHluBbCopi9mghoozZCm0lEwHa66tFQI OXU340/3LkGHoahhwgGoi+69NFQmGhoUft4QwuzoyRiAIBqiafzPTOotmmuIx1i4B82S MzNjevB+EB/kAmMxnXg7bTzZvjFzQtiKk+8jgDoq0TbGMGEB+VXhuWj9BQMgvHfiEkQk EI1g== X-Gm-Message-State: ALyK8tJKzKdAnWUiHRV/KWUTVWWIV551GZojOjr+4jLVH58NEzps0V7K0DL+9A9/SQ5Tv03osRPKToUS6pjqDg== X-Received: by 10.140.44.34 with SMTP id f31mr3527398qga.63.1466072853093; Thu, 16 Jun 2016 03:27:33 -0700 (PDT) MIME-Version: 1.0 Received: by 10.55.27.73 with HTTP; Thu, 16 Jun 2016 03:27:32 -0700 (PDT) In-Reply-To: References: From: Andrej Bauer Date: Thu, 16 Jun 2016 11:27:32 +0100 Message-ID: Subject: Re: [HoTT] Is synthetic the right word? To: Homotopy Type Theory Content-Type: text/plain; charset=UTF-8 Various subjects have been called synthetic, and in every case I am aware of the subject develops a branch of mathematics in (the internal language of) a topos that is particularly suitable for the topic at hand. Thus we have had Synthetic Differential Geometry, Synthetic Domain Theory, Synthetic Topology and Synthetic Computability. The word "synthetic" here refers to the fact that we create an artificial, or synthetic, world of mathematics suitable for doing whatever it is we are doing. For instance, the effective topos is suitable for doing computability. If I am wrong about this particular point, I would like to hear why Synthetic Differential Geometry was originally so called. The word "synthetic" does not refer to there being a completely new thing that is different from what has been done so far. In the above examples there is always a clear connection to the traditional ways, with suitable transfer theorems guaranteeing that the synthetic world is not just a hallucination. In line with the established terminology, such as it may be, Synthetic Homotopy Theory would be homotopy theory developed in (the internal language of) a topos, or other suitable structure, that is particularly suitable for doing homotopy theory. One may put a varying amounts of emphasis on the internal language or the models, according to taste. What I think we are lacking at the moment is a clear way of transfering results in synthetic homotopy theory back to a traditional setup. The explanation which says "interpretet in Kan simplicial sets and apply the geometric realization" does not seem to be good enough, or at least it should be made mathematically precise. Perhaps the we should just forget about topology and use simplicial sets as the natural traditional setup for doing homotopy theory? We even have Synthetic Combinatorics, although its author prefers to adopt terminology from biology and anthropology :-) With kind regards, Andrej