From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 2002:a5d:4dc9:: with SMTP id f9mr3159925wru.407.1589101800868; Sun, 10 May 2020 02:10:00 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a05:6000:9:: with SMTP id h9ls4723628wrx.9.gmail; Sun, 10 May 2020 02:09:59 -0700 (PDT) X-Received: by 2002:a5d:50ce:: with SMTP id f14mr13282979wrt.251.1589101799654; Sun, 10 May 2020 02:09:59 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1589101799; cv=none; d=google.com; s=arc-20160816; b=cV7fr7xbqwqsC8D+4l610U+U53fuxWSr9xSqqfeohuCIcg9tkKaO69QQfPA8VEO+iJ H6iLqm4hNw6FJmdQLr1eOAUvDi/llv+fTQJw65UVOf2CUZ6W/9aLBxKcn355mUpDlf+j khribjDQWQpaVp08/DR19SeKqlSzgAowx5vGtz1LbnY+7/QiaXx5nIPGtZ7aMGYj9A8O AIu4a3BcYQw8GgZyprNY6Zd8f83KLWNimu5khbW1mfh0KUU/qIHPjT5bWgVcjA44uDI0 R6f5eU1M9PeuWPp/yedrsgoFBAI1qyFXzA76fEwWeRgb7JOnguxuU06cdChWBkcCATWZ yFng== 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=xrK3kEPmJO4gus/4F2ZGj3nZ83hXGt2KQhYZFPjcLc8=; b=iVtDlTvh2qyS7iqxx9S/w6Udnw1WvWPMAv1z+Rcw7fDV6dKRVzJJMT687X/Wtx8SrO lk2a0Bt65EtRi6+iR81hKNB27QvfEgkzpWBJJMzzkE5kYxZvK8BDHIGgdaID/Ea44B3H feydiEdjpco3S9gH3bTUrY38eC+aSKLYL8YOqVKnyQnyFBxi2Urds3gUqWlVr+Ux0flZ MN8a5bwYUoJ96KFPM7zZEsss7zRgskc2P0nQqTy49+sBjyVZ4xKtwa743gLIMO4HrMHS 9EZ75r/vpZCAGnVZ5SpyVRIINSswIsnhmPNjRvtIV2Zh/Ulp93Qr7Y8pbajaTFGb2JVu 1coQ== 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.156.230 as permitted sender) smtp.mailfrom=stre...@mathematik.tu-darmstadt.de Return-Path: Received: from mail-relay230.hrz.tu-darmstadt.de (mail-relay230.hrz.tu-darmstadt.de. [130.83.156.230]) by gmr-mx.google.com with ESMTPS id u16si828343wmd.2.2020.05.10.02.09.59 for (version=TLS1_2 cipher=ECDHE-ECDSA-AES128-GCM-SHA256 bits=128/128); Sun, 10 May 2020 02:09:59 -0700 (PDT) Received-SPF: pass (google.com: best guess record for domain of stre...@mathematik.tu-darmstadt.de designates 130.83.156.230 as permitted sender) client-ip=130.83.156.230; Authentication-Results: gmr-mx.google.com; spf=pass (google.com: best guess record for domain of stre...@mathematik.tu-darmstadt.de designates 130.83.156.230 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-relay230.hrz.tu-darmstadt.de (Postfix) with ESMTPS id 49KdYy3hZ4z43SG; Sun, 10 May 2020 11:09:58 +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 04A9AfNX026873; Sun, 10 May 2020 11:10:41 +0200 Received: by fb04209.mathematik.tu-darmstadt.de (Postfix, from userid 11003) id 3BCBEC0055; Sun, 10 May 2020 11:09:57 +0200 (CEST) Date: Sun, 10 May 2020 11:09:57 +0200 From: Thomas Streicher To: Jon Sterling Cc: =?iso-8859-1?B?IkpveWFsLCBBbmRy6SI=?= , "'Martin Escardo' via Homotopy Type Theory" Subject: Re: [HoTT] Identity versus equality Message-ID: <20200510090957.GA24125@mathematik.tu-darmstadt.de> References: <20200508064039.GC21473@mathematik.tu-darmstadt.de> <8C57894C7413F04A98DDF5629FEC90B1652F54CC@Pli.gst.uqam.ca> <20200509082829.GA8417@mathematik.tu-darmstadt.de> <8C57894C7413F04A98DDF5629FEC90B1652F55C8@Pli.gst.uqam.ca> <20200509184313.GB28841@mathematik.tu-darmstadt.de> <8C57894C7413F04A98DDF5629FEC90B1652F563A@Pli.gst.uqam.ca> <8C57894C7413F04A98DDF5629FEC90B1652F5693@Pli.gst.uqam.ca> MIME-Version: 1.0 Content-Type: text/plain; charset=us-ascii Content-Disposition: inline In-Reply-To: User-Agent: Mutt/1.5.23 (2014-03-12) Dear Andr'e and Jon, I mostly agree with what Jon said. I also think that intensional type theory within an extensional type theory (it is 2 levels and not 3) is an attractive system for cubical type theory. In the simplicial case this is a bit more problematic since the filling conditions for Kan complexes involve classical existential quantification and as shown by Thierry et.al. this is important! That the extensional level is just formulated using J and K is a possibility. It has to be seen in practice how far it goes. Let me finish with a remark on how constructive traditional topos theory is. I don't mean the logic represented by a topos but which logical principles one uses when doing topos theory. Since one wants to develop toposes relative to fairly general base toposes people introduced fibered/indexed reasoning. But the reasoning about fibrations is per se fairly classical and also involves choice for classes typically. So this reasoning is performed on a meta level and not within the logic of the base topos. For the situations when this is partly possible Benabou invented the notion of "definability". This is sometimes swept under the carpet because of some "antilogical" tendencies which were influential at the time of the genesis of topos theory (beautifully described in a little essay by Reyes I recnely found on his home page). I am aware that I am on dangerous grounds now since Andr'e has really experienced and shaped these days (when I started high school). But it coincides with my impression of what is the practice of the working topos theorist... I think the real antagonism is or was that those days (and I am afraid still nowadays) traditional logicians are mainly adherents of a one world view. This has changed recently where even among set theorists there is a "multiverse" and a "universe" fraction and the former is getting larger compared to the past. This is funny in a sense since one of the reasons for a multiverse veiw was independnce results is set theory... Anyway both traditional topos theory and higher dimensional category theory was and is developed within a unrestricted metatheory which could be formalized in ZFC + every set is an element of some Grothendieck universe. It is not impossible that certain aspects and fragments can be developed in weaker systems but there is no guarantee that this will always work. Thomas