From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 10.25.44.205 with SMTP id s196mr1413434lfs.3.1465943464945; Tue, 14 Jun 2016 15:31:04 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 10.46.9.197 with SMTP id 188ls3514ljj.97.gmail; Tue, 14 Jun 2016 15:31:04 -0700 (PDT) X-Received: by 10.25.158.203 with SMTP id h194mr1420641lfe.0.1465943464505; Tue, 14 Jun 2016 15:31:04 -0700 (PDT) Return-Path: Received: from mail-lb0-x234.google.com (mail-lb0-x234.google.com. [2a00:1450:4010:c04::234]) by gmr-mx.google.com with ESMTPS id y20si883555lbl.1.2016.06.14.15.31.04 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Tue, 14 Jun 2016 15:31:04 -0700 (PDT) Received-SPF: pass (google.com: domain of virit...@gmail.com designates 2a00:1450:4010:c04::234 as permitted sender) client-ip=2a00:1450:4010:c04::234; Authentication-Results: gmr-mx.google.com; dkim=pass head...@gmail.com; spf=pass (google.com: domain of virit...@gmail.com designates 2a00:1450:4010:c04::234 as permitted sender) smtp.mailfrom=virit...@gmail.com; dmarc=pass (p=NONE dis=NONE) header.from=gmail.com Received: by mail-lb0-x234.google.com with SMTP id oe3so1236800lbb.1 for ; Tue, 14 Jun 2016 15:31:04 -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 :cc; bh=Dg2ERCk+rqYGR4eBIcgfTujTs3xTJcYc4U6wnhd/Zyg=; b=dwd1kFK7YTC33e/RLeWkoZZrLJ1xyQIP1VZNdYczUUr81yrBwHBagjvO6Bynmim5fA hRKuPEQudODutaG2At7cKjFpKCjYlts5lEwUSz6IH01Yvmatvrc4wxnknBlqbMRvGPjh +RK6bhKIDvTB8C9a3oc9OT7hoeHuvO5G++FJXtNVvdKxGjaU15VdGij7sshHgesERzBO viUKiqt1tBmEG5JAwXDtQK66/bF6lc/uHyGieyonIBwkoTi+mUcSMx5VJMmczH6G2qlk 0OfEM1JNs3OR/T8XptXWK7L6MYe90SloQmG0WLww8Dy4gsmX4msBWxbNsUhJk55bNL5Y JJ9g== X-Gm-Message-State: ALyK8tJr1UmDmp1npKaFpJOjQfyGCdgKiKt9cq9dc2fSB8JfwReH3bxwTWt4/AKe+kokx46y9qoJHRICY9jfqA== X-Received: by 10.25.87.83 with SMTP id l80mr1045339lfb.159.1465943464319; Tue, 14 Jun 2016 15:31:04 -0700 (PDT) MIME-Version: 1.0 Received: by 10.25.19.203 with HTTP; Tue, 14 Jun 2016 15:30:44 -0700 (PDT) In-Reply-To: <576081E8.1080701@cs.bham.ac.uk> References: <5750A527.4060705@cs.bham.ac.uk> <57548E59.9080406@cs.bham.ac.uk> <5757EFE8.3070807@cs.bham.ac.uk> <576081E8.1080701@cs.bham.ac.uk> From: Michael Shulman Date: Tue, 14 Jun 2016 15:30:44 -0700 Message-ID: Subject: Re: [HoTT] What is UF, what is HoTT and what is a univalent type theory? To: Martin Escardo Cc: "HomotopyT...@googlegroups.com" Content-Type: text/plain; charset=UTF-8 Note that the sentence you quoted began with "if MLTT and HoTT refer to specific formal systems". However, as I've been saying, I *don't* think "HoTT" should refer to a specific formal system, and you've just given one good argument as to why. (-: However, I suppose even on the grounds of formal systems one could object. ZF includes Zermelo set theory as a subsystem, but there's no reason to say that ZF only "begins" when we start using the replacement axiom. So maybe it would be better to say that, as formal systems, MLTT ends when we start using univalence/HITs/etc., but since HoTT includes MLTT it begins at the same place. On Tue, Jun 14, 2016 at 3:15 PM, Martin Escardo wrote: > 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.) >