From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 10.25.196.143 with SMTP id u137mr1402635lff.9.1465396689483; Wed, 08 Jun 2016 07:38:09 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 10.28.175.69 with SMTP id y66ls126114wme.2.gmail; Wed, 08 Jun 2016 07:38:07 -0700 (PDT) X-Received: by 10.28.152.70 with SMTP id a67mr1473817wme.4.1465396687234; Wed, 08 Jun 2016 07:38:07 -0700 (PDT) Return-Path: Received: from mail-lf0-x233.google.com (mail-lf0-x233.google.com. [2a00:1450:4010:c07::233]) by gmr-mx.google.com with ESMTPS id ur4si53248lbc.0.2016.06.08.07.38.07 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Wed, 08 Jun 2016 07:38:07 -0700 (PDT) Received-SPF: pass (google.com: domain of virit...@gmail.com designates 2a00:1450:4010:c07::233 as permitted sender) client-ip=2a00:1450:4010:c07::233; Authentication-Results: gmr-mx.google.com; dkim=pass head...@gmail.com; spf=pass (google.com: domain of virit...@gmail.com designates 2a00:1450:4010:c07::233 as permitted sender) smtp.mailfrom=virit...@gmail.com; dmarc=pass (p=NONE dis=NONE) header.from=gmail.com Received: by mail-lf0-x233.google.com with SMTP id u74so6985855lff.2 for ; Wed, 08 Jun 2016 07:38:07 -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; bh=ZEoElCk7NwpW0iOrb58yaVfEUNbJYZVBhCr9oBm1qbo=; b=uGq4bKcNmSSAqO75f6l6M2yg8lDFnW/+lTAfmCcdpwt+DR52w22S51NvXWfaOH3Tw9 vKwGweny+H1wLZEZAZzMOGEXE+9n2ajmBRzdhIdYA3F1F1Vz8vYwwWh5oDkjjLXiD0mf W3JOBDYwOqSWHjwakA3jpfnQBcj9rRMmygTfHA+Lkpa5J1afdu+dcYjHMZj4pEHCjEDs fi240x5oUuF2opudquw8gWMwQVeP5aJ7b8YAM9QKxqeaNXiHVmLO9RwiZtY3l4TaQ4KQ 7SgpulCtatDYqXRaRJmyOyw6AHTpFwtR5rRr5MqBc3Hsxd4HqAQ8nkg6dxpPqj6cSGWo gI3g== X-Gm-Message-State: ALyK8tLnCpQmNbWDZcBQSXu2ge1OlsDomfofGa/JeyjrkqyqrqHlwoOqVnuvbjF5R9K4Ew+Yy+8QXF1SqPYB5w== X-Received: by 10.25.42.21 with SMTP id q21mr5056065lfq.94.1465396686969; Wed, 08 Jun 2016 07:38:06 -0700 (PDT) MIME-Version: 1.0 Received: by 10.25.23.84 with HTTP; Wed, 8 Jun 2016 07:37:47 -0700 (PDT) In-Reply-To: References: <5750A527.4060705@cs.bham.ac.uk> <57548E59.9080406@cs.bham.ac.uk> From: Michael Shulman Date: Wed, 8 Jun 2016 07:37:47 -0700 Message-ID: Subject: Fwd: [HoTT] What is UF, what is HoTT and what is a univalent type theory? To: "HomotopyT...@googlegroups.com" Content-Type: text/plain; charset=UTF-8 Here is a message that didn't make it through to the list. ---------- Forwarded message ---------- From: Michael Shulman Date: Wed, Jun 8, 2016 at 1:18 AM Subject: Re: [HoTT] What is UF, what is HoTT and what is a univalent type theory? To: Martin Escardo Cc: "HomotopyT...@googlegroups.com" On Sun, Jun 5, 2016 at 1:40 PM, Martin Escardo wrote: > Perhaps you should say what you think HoTT is, for instance to prevent me > from mis-representing it. Personally (all caveats repeated), I prefer to use it for the mathematical subject involving the interaction of homotopy-theoretic and type-theoretic ideas, including models of type theory in classical homotopy theories but also application of homotopy-theoretic ideas to type theory. I don't mean to specify any particular philosophy or motivation for doing such mathematics. > But also to prevent people from reading the book in an unintended way. Yes, it would be nice for the book to make clearer that the particular type theory used therein is only one possible choice, and other possibilities are a field of active research. > To make a parallel (again), I very much like intuitionistic mathematics as > Brouwer initiated it. What we nowadays distil from it is called > intuitionistic logic. > > But with Brouwer it had a heavy amount of topology, which we now consider to > be still very interesting (and in particular I do myself), but we don't any > more consider to be the essence of intuitionistic mathematics. > > ... > > But to say homotopy is the ultimate understanding of identity would be like > saying that topology is the ultimate understanding of intuitionistic logic. This is a very interesting point; I am glad that you brought it up. When you first mentioned it a while ago, my reaction was that "logically it makes sense, but intuitively it feels wrong". But I didn't say that out loud because it didn't seem like a very good argument! (-: After mulling it over for a while, however, I have a couple of real points to make, to explain my intuitive reaction. Firstly, I agree that topology is not the ultimate understanding of intuitionistic logic. But I think one might more plausibly argue that topology is the ultimate understanding of *geometric* logic. That is, the relationship between topology and intuitionistic logic is the same as the relationship between frames and Heyting algebras. Every frame is a Heyting algebra, so topology furnishes models of intuitionistic logic. But frame homomorphisms are different from Heyting algebra homomorphisms, and moreover not every Heyting algebra is complete; so there is more to intuitionistic logic than topology. So this is one concrete way in which I think the connection between homotopy and identity is closer than the connection between topology and intuitionistic logic. Secondly, I *DO* actually believe that homotopy is the ultimate understanding of identity. Why? That is essentially the definition of "homotopy"! Homotopy theory is the study of infty-groupoids, and an infty-groupoid is exactly what you get when you take a vague intuitive notion of "collection" and allow "different witnesses of identity" in a coherent way. The historical origins (and current concrete incarnations) of homotopy theory in topological spaces and simplicial sets are, philosophically, irrelevant; what the homotopy theorist is actually interested in are infty-groupoids, as witnessed by the tide sweeping homotopy theory into (infty,1)-categorical language that talks more directly about its objects of interest. A mathematical expression of this is Brunerie's observation that Martin-Lof's rule for identity types is essentially a definition of infty-groupoid, and that the definition one gets is essentially the very first such definition given by Grothendieck. There is nothing analogous on the other side of your analogy: the rules of intuitionistic logic do not encompass a definition of topological space (though one might argue that the rules of *geometric* logic do). Best, Mike