From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 10.28.40.195 with SMTP id o186mr1502741wmo.5.1465959875316; Tue, 14 Jun 2016 20:04:35 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 10.28.90.2 with SMTP id o2ls1035440wmb.44.canary; Tue, 14 Jun 2016 20:04:34 -0700 (PDT) X-Received: by 10.194.20.233 with SMTP id q9mr1505692wje.1.1465959874686; Tue, 14 Jun 2016 20:04:34 -0700 (PDT) Return-Path: Received: from mail-lf0-x22b.google.com (mail-lf0-x22b.google.com. [2a00:1450:4010:c07::22b]) by gmr-mx.google.com with ESMTPS id a14si892667lbq.3.2016.06.14.20.04.34 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Tue, 14 Jun 2016 20:04:34 -0700 (PDT) Received-SPF: pass (google.com: domain of virit...@gmail.com designates 2a00:1450:4010:c07::22b as permitted sender) client-ip=2a00:1450:4010:c07::22b; Authentication-Results: gmr-mx.google.com; dkim=pass head...@gmail.com; spf=pass (google.com: domain of virit...@gmail.com designates 2a00:1450:4010:c07::22b as permitted sender) smtp.mailfrom=virit...@gmail.com; dmarc=pass (p=NONE dis=NONE) header.from=gmail.com Received: by mail-lf0-x22b.google.com with SMTP id l188so1448047lfe.2 for ; Tue, 14 Jun 2016 20:04:34 -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=EhVxMRCaax//cyE+x1x5GxcfoAGE/TwhE/BkcJjAeZg=; b=X7IKlpaabQUwJZOur3HUbExP+U1LChDJV1Ja2if736eS8QvR3cQ4SVJnjYRyS1X08x gk59HExqeVLk6q6f1ZhTK6io1hC3whp02z37X6uoFGg9X6VmWdcnxbp1gpS+9Ks2ahQQ AvDzuWLwyTQmiHF94M6XczDmWWfrMNMTlHCyZxYWtKBuanoe4JQHPWCAYB3Jky4LOGpz 7UhUmkXjC7Zblsj3OyMLbrfC3D5zz7AB7N67tF+vGlwHA7pDjTx1O9yyWfMobG71DkO2 IhaLWi3I25xGTWZpFCDRI6xgsMEFp2yoeaWSGphFGQKDni+qaV1oBUWa9rcT+JmxGsDu LNiw== X-Gm-Message-State: ALyK8tJ+SHdYdhvY06qYGlOq5JRB96J/vpANTHbRnH5yMJ0aQMWmLxydakch2zkk1eWM4Qy6tr1ImLeTnVpjfw== X-Received: by 10.25.30.194 with SMTP id e185mr2996122lfe.202.1465959874446; Tue, 14 Jun 2016 20:04:34 -0700 (PDT) MIME-Version: 1.0 Received: by 10.25.19.203 with HTTP; Tue, 14 Jun 2016 20:04:14 -0700 (PDT) In-Reply-To: <5760945A.7050108@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> <5760945A.7050108@cs.bham.ac.uk> From: Michael Shulman Date: Tue, 14 Jun 2016 20:04:14 -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 The main point I meant to make is that I don't know what you mean by the question "where does MLTT end and HoTT begin?" I think it could mean different things, and have different answers, depending on exactly what one means by "MLTT" and "HoTT" (let alone "begin" and "end"). But I think this discussion has probably passed the point of diminishing returns for a mailing list. (-: I would be happy to continue privately if you like. On Tue, Jun 14, 2016 at 4:33 PM, Martin Escardo wrote: > > > On 14/06/16 23:30, Michael Shulman wrote: >> >> 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. (-: > > > After 50 minutes of reflection, I am not sure how to react to this. Whatever > the formal system, univalent foundations does start by working in a type > theory in which types are omega-groupoids and in which there is a notion of > equivalence which is used to formulate univalence, which is postulated. > > So I am not sure what you are up to here. Perhaps MLTT was wrong for this > (univalence). Fair enough. But then we have cubicaltt, which accomplishes > this and more. > > Anyway, I am not sure what is the point you wanted to make. > > I am happy for you not to commit yourself to a particular type theory, or > any theory, but at some point you have to be sufficiently precise about what > you want to talk about. > >> 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. > > > I guess my point is that MLTT is naturally invariant under equivalence, > before we postulate the univalence axiom. > > In fact, the consistency of the univalence axiom says something about MLTT > without the univalence axiom: namely that it can't distinguish equivalent > types. > > Martin