From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 2002:a7b:c1c4:: with SMTP id a4mr14710814wmj.86.1588595981773; Mon, 04 May 2020 05:39:41 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a05:6000:8d:: with SMTP id m13ls5515208wrx.4.gmail; Mon, 04 May 2020 05:39:40 -0700 (PDT) X-Received: by 2002:adf:e784:: with SMTP id n4mr11166956wrm.170.1588595980644; Mon, 04 May 2020 05:39:40 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1588595980; cv=none; d=google.com; s=arc-20160816; b=IHA3XYSUHjz21oJGAi7fleosnSvS+VRUuVmBTbfPAq+BCrxV6PcakVRwxpHLXYGYxo IRtjVGwzEHct7H7quzADmmd0+fDzOX1iSHN9MxCz1o2i3RGTZeYkcT6c8LbRbP5cUqAA tmf7x3aTzm5ZDtQrY6/UdXUHpKXXAm3hVvm6GlQBX24/Am64Rp4Y5zK+WapU7wAaIvLo Ecf9TkfK/B2nvdB+qMFGWfUJsmsvtm8joqh18Xx3xq1lfhTboJUQUghkzh0eBoyplT9M eICkDEAyhJHyZTaMbGlhZ5Z/5RiDGXr3coiusG8apBScNtXWAlNkFDx7qLA6g7+uB9VZ XtjA== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=user-agent:in-reply-to:content-disposition:mime-version:references :message-id:subject:cc:to:from:date; bh=O4FnP7nqqzCF1q+X/AeH9pJ8EEiHNOP/XrOjOGLzORY=; b=UnpcPhtvtPlIi/y9VeLC0tbmWg/Id4FwQXxMhHfZI6gznk8XX/ShlGB1qzrdERZX4G GbC1g1mz5jmjl2HJ3Kjv4Z7zXsYzKmRDzJS1u3cscOFBaXNIrDu/wqFfmegEuiO6MpvH rE5KrErG5saeVNlDbj5oOgXMU7JNozwlJsdQd0acxp7xM0y3Zk7cpNBSiosqrk9mRjmJ bh/0zS0l2cobNu14Px5EiIhqyTzkNU253an7Gu2AXZshilAqAzNW4W4aySkwTv9gmuYe IVMBf6J2RncMkluLppY4Mme8kRi/S/Tepi9n52H0xrv9IMv7uOFvMq95ltH+XBm8m0RY 1Frw== ARC-Authentication-Results: i=1; gmr-mx.google.com; spf=pass (google.com: best guess record for domain of stre...@mathematik.tu-darmstadt.de designates 130.83.252.152 as permitted sender) smtp.mailfrom=stre...@mathematik.tu-darmstadt.de Return-Path: Received: from mail-relay152.hrz.tu-darmstadt.de (mail-relay152.hrz.tu-darmstadt.de. [130.83.252.152]) by gmr-mx.google.com with ESMTPS id q17si545181wmg.1.2020.05.04.05.39.40 for (version=TLS1_2 cipher=ECDHE-ECDSA-AES128-GCM-SHA256 bits=128/128); Mon, 04 May 2020 05:39:40 -0700 (PDT) Received-SPF: pass (google.com: best guess record for domain of stre...@mathematik.tu-darmstadt.de designates 130.83.252.152 as permitted sender) client-ip=130.83.252.152; Authentication-Results: gmr-mx.google.com; spf=pass (google.com: best guess record for domain of stre...@mathematik.tu-darmstadt.de designates 130.83.252.152 as permitted sender) smtp.mailfrom=stre...@mathematik.tu-darmstadt.de Received: from fb04281.mathematik.tu-darmstadt.de (fb04281.mathematik.tu-darmstadt.de [130.83.2.21]) (using TLSv1.2 with cipher ECDHE-RSA-AES256-GCM-SHA384 (256/256 bits)) (Client CN "mail.mathematik.tu-darmstadt.de", Issuer "DFN-Verein Global Issuing CA" (verified OK)) by mail-relay152.hrz.tu-darmstadt.de (Postfix) with ESMTPS id 49G2Vg5JqHz43ql; Mon, 4 May 2020 14:39:39 +0200 (CEST) Received: from fb04209.mathematik.tu-darmstadt.de (fb04209.mathematik.tu-darmstadt.de [130.83.2.209]) by fb04281.mathematik.tu-darmstadt.de (8.14.4/8.14.4/Debian-8+deb8u2) with ESMTP id 044CeCPA010312; Mon, 4 May 2020 14:40:12 +0200 Received: by fb04209.mathematik.tu-darmstadt.de (Postfix, from userid 11003) id 14E58C0061; Mon, 4 May 2020 14:39:39 +0200 (CEST) Date: Mon, 4 May 2020 14:39:39 +0200 From: Thomas Streicher To: Thorsten Altenkirch Cc: "homotopyt...@googlegroups.com" Subject: Re: [HoTT] "Identifications" ? Message-ID: <20200504123938.GA15963@mathematik.tu-darmstadt.de> References: <20200504120620.GA14623@mathematik.tu-darmstadt.de> <31C5A7B0-8512-4ABD-8DAA-EF3A1FA0EEFF@nottingham.ac.uk> MIME-Version: 1.0 Content-Type: text/plain; charset=us-ascii Content-Disposition: inline In-Reply-To: <31C5A7B0-8512-4ABD-8DAA-EF3A1FA0EEFF@nottingham.ac.uk> User-Agent: Mutt/1.5.23 (2014-03-12) Hi Thorsten, > But I am not "interpreting HoTT in SSet". I am just working in HoTT. You are doing Metamathematics, I am just talking about Mathematics. > > Sure when you consider models of your theory you can say that certain equalities are just metatheoretic equalities and others are non-trivial equalities. I am not sure what you really mean but I guess you refer to the distinction between what is provable in HoTT and what holds or exists in particular models. Of couse, Nicolai"s vexing example is model dependent (at least in my reconstruction!) But that is the same in set theory. Most of the time you are model independent, i.e. provable in ZFC or actually much weaker systems. But there are quite a few things which heavily depend on the model. Continuum Hypothesis for example but many other things as well. Modern set theory is essentially about independences... And if you consider ZF the notions of finite and Dedekind finite are different. That is in my opinion an example where incompleteness strikes already on a very basic level! Thomas PS But I agree that this is "metamathematical" but so what. Mathematics is not one fixed game but rather pluralist even classically. Even more so constructively where things branch much earlier. As a (categorical) logician one is interested in constructive mathematics precisely because of this excessive pluralism! I never understood why constructive math is used in the singular since it is even false for classical maths. And adding strong principles doesn't mean one gets nonalgorithmic. Adding to HA all true Pi^0_1 sentences doesn't allow you to construct functions on N which are not recursive (as follow from number realizability).