From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 10.25.38.75 with SMTP id m72mr1776463lfm.4.1465159254011; Sun, 05 Jun 2016 13:40:54 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 10.28.15.11 with SMTP id 11ls353028wmp.48.canary; Sun, 05 Jun 2016 13:40:52 -0700 (PDT) X-Received: by 10.28.45.145 with SMTP id t139mr1134223wmt.1.1465159252673; Sun, 05 Jun 2016 13:40:52 -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 s140si744840wme.1.2016.06.05.13.40.52 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Sun, 05 Jun 2016 13:40:52 -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 1b9eqq-0000QF-NA; Sun, 05 Jun 2016 21:40:52 +0100 Received: from host81-147-122-132.range81-147.btcentralplus.com ([81.147.122.132] helo=[192.168.1.112]) by bham.ac.uk (envelope-from ) with esmtpsa (TLSv1.2:DHE-RSA-AES128-SHA:128) (Exim 4.84) id 1b9eqq-0006Be-DI using interface auth-smtp.bham.ac.uk; Sun, 05 Jun 2016 21:40:52 +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> Cc: "HomotopyT...@googlegroups.com" From: Martin Escardo Organization: University of Birmingham Message-ID: <57548E59.9080406@cs.bham.ac.uk> Date: Sun, 5 Jun 2016 21:40:57 +0100 User-Agent: Mozilla/5.0 (X11; Linux x86_64; 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 X-BHAM-AUTH-data: TLSv1.2:DHE-RSA-AES128-SHA:128 via 147.188.128.21:465 (escardom) On 04/06/16 12:43, Michael Shulman wrote: > On Thu, Jun 2, 2016 at 4:29 PM, Martin Escardo wrote: >> The difference with >> HoTT is that in HoTT such distinctions are merely axiomatized. > > Please stop saying this. Obviously I can't claim to personally > "define HoTT" in the same way that Vladimir can "define UF", but the > term "homotopy type theory" as it is used, not just by me but by > plenty of other people, DOES NOT refer only to the type theory > described in the book that adds axioms to MLTT. It INCLUDES cubical > type theory. If you want to refer to the formal type theory used in > the book, some possibilities are "HoTT 1.0" or "Book HoTT". I am happy to stop saying this. I am glad that Vladimir said explicitly what he thinks UF is/should be (and that also he said more than I asked). Perhaps you should say what you think HoTT is, for instance to prevent me from mis-representing it. But also to prevent people from reading the book in an unintended way. What is clear, both with UF and with HoTT, is that they are both (indended to be) a philosophy and also something mathematically precise matching such philosophy. Perhaps each of them also explicitly desire some amount of vagueness, or open-endedness, or generality, e.g. to accommodate cubicaltt. 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. I think I am in a similar process regarding UF/HoTT. What I think happened was that with Brouwer, Heyting, Curry, Howard, de Brujin, Martin-Loef and many others, and with topos theory too, we understood logic rather well, excluding equality. Then Martin-Loef said something new about equality in the form of the identity type. Like with topology in Brouwer's hands to understand logic, homotopy has been used to understand Martin-Loef identity. (Or, if you come from the other side, Martin-Loef identity has been used to formalize homotopy equivalence, but this is a later development (and certainly interesting, as I said in my previous message).) But to say homotopy is the ultimate understanding of identity would be like saying that topology is the ultimate understanding of intuitionistic logic. I do think that topology is a very good and precise understanding of intuitionistic logic, and that homotopy is a very good and precise understanding of identity. However, I wouldn't like to refer to intuitionistic logic as topological logic, or to refer to a type theory with the identity type as homotopy type theory. And the univalence axiom and higher-inductive types make sense on their own before we consider any homotopical interpretation, just as intuitionistic logic makes sense before we consider any topological interpretation. Having said that, yes, I love both the topological and the homotopical interpretations of (mathematics and) logic, and, moreover, I would like to see them properly combined, as we discussed earlier. Best, Martin