From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 10.25.125.7 with SMTP id y7mr1447033lfc.2.1465947227223; Tue, 14 Jun 2016 16:33:47 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 10.28.26.82 with SMTP id a79ls47519wma.37.gmail; Tue, 14 Jun 2016 16:33:46 -0700 (PDT) X-Received: by 10.28.4.210 with SMTP id 201mr1427555wme.6.1465947226701; Tue, 14 Jun 2016 16:33:46 -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 x203si207760wme.0.2016.06.14.16.33.46 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Tue, 14 Jun 2016 16:33:46 -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 1bCxq6-0007L9-O1; Wed, 15 Jun 2016 00:33:46 +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 1bCxq6-00029s-E9 using interface auth-smtp.bham.ac.uk; Wed, 15 Jun 2016 00:33:46 +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> <576081E8.1080701@cs.bham.ac.uk> Cc: "HomotopyT...@googlegroups.com" From: Martin Escardo Organization: University of Birmingham Message-ID: <5760945A.7050108@cs.bham.ac.uk> Date: Wed, 15 Jun 2016 00:33:46 +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 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