From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 10.194.20.233 with SMTP id q9mr1415727wje.1.1465942505407; Tue, 14 Jun 2016 15:15:05 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 10.28.63.81 with SMTP id m78ls48283wma.21.gmail; Tue, 14 Jun 2016 15:15:04 -0700 (PDT) X-Received: by 10.28.45.208 with SMTP id t199mr1427980wmt.0.1465942504806; Tue, 14 Jun 2016 15:15:04 -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 x203si200973wme.0.2016.06.14.15.15.04 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Tue, 14 Jun 2016 15:15:04 -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 1bCwbw-0006Px-Np; Tue, 14 Jun 2016 23:15:04 +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 1bCwbw-0004OH-Dw using interface auth-smtp.bham.ac.uk; Tue, 14 Jun 2016 23:15:04 +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> <5757EFE8.3070807@cs.bham.ac.uk> Cc: "HomotopyT...@googlegroups.com" From: Martin Escardo Organization: University of Birmingham Message-ID: <576081E8.1080701@cs.bham.ac.uk> Date: Tue, 14 Jun 2016 23:15:04 +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) Mike, I think we agree a lot. So let me disagree here: On 14/06/16 22:46, Michael Shulman wrote: > As for when MLTT ends and when HoTT begins, if "MLTT" and "HoTT" refer > to specific formal systems, then the answer is that HoTT begins > whenever we use something present in HoTT that is not present in MLTT, > like univalence or HITs. I disagree, because, as I said in the previous messages in this thread, before we have univalence or HIT's, we can: 0. Know that types are omega-groupoids. (And you asserted that too.) 1. Define what an n-type is. 2. Define what an equivalence is. 3. Formulate the univalence axiom without asserting it (which is much subtler than it seems, as you know, because, for example, if in its formulation you use "isomorphism" rather than equivalence, then you get something that is provably false even before we begin looking for a model). 4. Blah blah blah. In particular, the PhD thesis of my student Chuangjie Xu was based on this rationale, without ever invoking univalence or HIT's, even though is had *nothing* to do with homotopy. We just saw that the new ideas about MLTT coming from homotopy were rather useful for what we wanted to talk about (Brouwerian continuity axioms and Kleene-Kreisel functionals). Martin (I still don't know where MLTT ends and HoTT begins.)