From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 10.28.27.213 with SMTP id b204mr169812wmb.4.1464985045062; Fri, 03 Jun 2016 13:17:25 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 10.46.5.18 with SMTP id 18ls54477ljf.17.gmail; Fri, 03 Jun 2016 13:17:23 -0700 (PDT) X-Received: by 10.25.16.106 with SMTP id f103mr799664lfi.3.1464985043753; Fri, 03 Jun 2016 13:17:23 -0700 (PDT) Return-Path: Received: from sun60.bham.ac.uk (sun60.bham.ac.uk. [147.188.128.137]) by gmr-mx.google.com with ESMTPS id j140si52069wmf.1.2016.06.03.13.17.23 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Fri, 03 Jun 2016 13:17:23 -0700 (PDT) Received-SPF: pass (google.com: best guess record for domain of m.es...@cs.bham.ac.uk designates 147.188.128.137 as permitted sender) client-ip=147.188.128.137; 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.137 as permitted sender) smtp.mailfrom=m.es...@cs.bham.ac.uk Received: from [147.188.128.127] (helo=bham.ac.uk) by sun60.bham.ac.uk with esmtp (Exim 4.84) (envelope-from ) id 1b8vX0-0000PC-Oi; Fri, 03 Jun 2016 21:17:22 +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 1b8vX0-0001xd-En using interface auth-smtp.bham.ac.uk; Fri, 03 Jun 2016 21:17:22 +0100 Subject: Re: [HoTT] Re: What is UF, what is HoTT and what is a univalent type theory? To: Vladimir Voevodsky , Andrew Polonsky References: <5750A527.4060705@cs.bham.ac.uk> Cc: Homotopy Type Theory From: Martin Escardo Organization: University of Birmingham Message-ID: <5751E5D2.6030306@cs.bham.ac.uk> Date: Fri, 3 Jun 2016 21:17:22 +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) Thanks, Vladimir for this. It is good to know where you come from, explicitly, and what your philosophy and program are. I will concentrate in one aspect of your reply, which is probably the one you didn't intend to emphasize: On 03/06/16 13:49, Vladimir Voevodsky wrote: > However the original philosophy of MLTT and the original philosophy of > UF are different and our use of MLTT for UF is in a sense an abuse of > the MLTT as Per himself politely mentioned a number of times. Precisely. It always seemed to me, for a long time, since the last millemium, that the identity type was ad hoc, starting from the fact that there were three alternative approaches to patch it: (1) (Going back to Bishop) Work with setoids. Perhaps this is *the* philosophy ML had in mind. I don't know. However, it is a pity that a formal system supporting this philosophy was created, but the philosophy was not formalised by Martin-Loef. But Martin Hofmann did this (excluding the universe). Is that what Martin-Lof had in mind? (2) Have the reflection rule. Martin-Loef had this for a while. But then how does this relate to (1)? I've never seen an account of this. People just concentrate on undecidability things regarding (2), which I think is a red hearing. (3) Have the K axiom. This is due to Streicher. Then UF has a fourth way to look at this: (4) Certain types do satisfy the K axiom. But there is no reason why all types should satisfy it. What worked as a "revelation" to me what not the univalence axiom (which makes (4) good), but something we can say before we consider the univalence axiom: although there is no reason to suppose that, in MLTT, any two points of Id X x y are themselves Id-related, we have that any two points of Sigma(y:X). Id x y are Id-related. This was known before UF/HoTT, and was considered puzzling for a while. What is interesting is that homotopy explains this very clearly and naturally. It was this that convinced me that the homotopical view of types is correct, once one has identity types. It was not the univalence axiom or higher inductive types. The identity type seemed something at the same time natural and weird from the point of view of the philosophy of the last millenium. Without changing MLTT, but now looking at it from the homotopical point of view, it seems now completely natural to me. Before it felt rather weird. There is more to say, but I prefer this message to have just one point. Martin