From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 10.28.93.20 with SMTP id r20mr1241090wmb.5.1465380842450; Wed, 08 Jun 2016 03:14:02 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 10.25.36.68 with SMTP id k65ls6913lfk.71.gmail; Wed, 08 Jun 2016 03:14:01 -0700 (PDT) X-Received: by 10.46.1.38 with SMTP id 38mr1118657ljb.3.1465380841291; Wed, 08 Jun 2016 03:14:01 -0700 (PDT) Return-Path: Received: from sun61.bham.ac.uk (sun61.bham.ac.uk. [147.188.128.150]) by gmr-mx.google.com with ESMTPS id f142si745383wmf.3.2016.06.08.03.14.01 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Wed, 08 Jun 2016 03:14:01 -0700 (PDT) Received-SPF: pass (google.com: best guess record for domain of m.es...@cs.bham.ac.uk designates 147.188.128.150 as permitted sender) client-ip=147.188.128.150; Authentication-Results: gmr-mx.google.com; spf=pass (google.com: best guess record for domain of m.es...@cs.bham.ac.uk designates 147.188.128.150 as permitted sender) smtp.mailfrom=m.es...@cs.bham.ac.uk Received: from [147.188.128.127] (helo=bham.ac.uk) by sun61.bham.ac.uk with esmtp (Exim 4.84) (envelope-from ) id 1bAaUq-0000Mm-Oz; Wed, 08 Jun 2016 11:14:00 +0100 Received: from mx1.cs.bham.ac.uk ([147.188.192.53]) by bham.ac.uk (envelope-from ) with esmtp (Exim 4.84) id 1bAaUq-0004JT-FC using interface smart1.bham.ac.uk; Wed, 08 Jun 2016 11:14:00 +0100 Received: from dynamic200-118.cs.bham.ac.uk ([147.188.200.118]) by mx1.cs.bham.ac.uk with esmtp (Exim 4.51) id 1bAaUq-0007br-JJ; Wed, 08 Jun 2016 11:14:00 +0100 Subject: Re: [HoTT] What is UF, what is HoTT and what is a univalent type theory? To: Michael Shulman References: <5750A527.4060705@cs.bham.ac.uk> <57548E59.9080406@cs.bham.ac.uk> Cc: "HomotopyT...@googlegroups.com" From: =?UTF-8?B?TWFydMOtbiBIw7Z0emVsIEVzY2FyZMOz?= Organization: University of Birmingham Message-ID: <5757EFE8.3070807@cs.bham.ac.uk> Date: Wed, 8 Jun 2016 11:14:00 +0100 User-Agent: Mozilla/5.0 (X11; Linux i686; rv:38.0) Gecko/20100101 Thunderbird/38.8.0 MIME-Version: 1.0 In-Reply-To: Content-Type: text/plain; charset=utf-8; format=flowed Content-Transfer-Encoding: 7bit X-BHAM-SendViaRouter: yes Many thanks, Mike, for your reply. I am prepared to agree with all your points, in particular: (1) You use geometric logic to explain the gap between topology and intuitionistic logic in a very nice and precise way. In particular, you said "the rules of intuitionistic logic do not encompass a definition of topological space (though one might argue that the rules of *geometric* logic do)". Nice way to put it. (2) You make the point that, since the presence of identity types makes types into infty-groupoids, we get (an incarnation of) homotopy theory. So, in this sense, yes, we have a much more precise match. (But, to play devil's advocate, we do have a precise definition of geometry logic to match up with intuitionistic logic, but are you offering precise definitions of the things to be matched up in (2)? (Existing or to be developed.)) You also make a point that HoTT is not tied to a particular type theory, like Vladimir says UF is not tied to a particular type theory. I agree with this, and I am sorry if in previous messages I may have conveyed the opposite view. Now, for the sake of discussion, suppose a particular incarnation of HoTT like in the book, based on MLTT. I wonder what you think about the question of when MLTT ends and HoTT begins. For instance, much of HoTT/UF works without anything added to MLTT, not even function extensionality, like seeing that types are infty-groupoids, the definition of n-type, the definition of equivalence and more. Is HoTT a way to understand (the identity types of) MLTT? (Which, in this case, is, as Vladimir said, not the originally intended one.) Best, Martin On 08/06/16 09:18, Michael Shulman wrote: > 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 > -- http://www.cs.bham.ac.uk/~mhe