From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 2002:a2e:9cc1:: with SMTP id g1mr638922ljj.261.1588920044672; Thu, 07 May 2020 23:40:44 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a2e:81d6:: with SMTP id s22ls121166ljg.0.gmail; Thu, 07 May 2020 23:40:43 -0700 (PDT) X-Received: by 2002:a2e:990f:: with SMTP id v15mr670748lji.7.1588920043344; Thu, 07 May 2020 23:40:43 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1588920043; cv=none; d=google.com; s=arc-20160816; b=NEDm7wXCBhRQHRPX5ffz0pzPrw7OetCEhPfooJZbF3oKVUESK4AK0Tu1mzZs4Lcmje rgI0vaT6yoMEIV34G45+i3F4sSgZlSNqX25nUcsbbDKo+UqwzMWFUtiiz0Y8Ag9q8ur4 SMWEqQrjw2nJKPdsiCmP+zuAAzdtomYXoVcwPrbQQMBVT7kdzVrgYpV/D5QdkgBjVPW6 t7JiVifD26xQVFYRdJTSbB8Yy3uOwNLLB5se4fvenhinbGlT4f8eWAQO9XAvZ/1LMl63 fILpNgaWjdZm5uwJz0/OPGAxKOmCoWR1MXLYF8go5S0q836MnKIEuLWMJKcqJbd7CWUU Oruw== 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=PwG8CPzJA+lurVle4xyjIx4n5TGadSJd6BwJArncMlA=; b=tJZ0aSV7RStOPnmJCBlWgvVA7oNXrhhVBqcFfiCvlSCsBtaz72RGcSXnfqvbyhRHfH 74qESyepJemQ86Hf1hW4tw0GgnfT/0WdMFTUTrLBig6tCcNJHVIcBAJ2lirpSH/jX4wZ /dwPRWtH8wceA5nrC50mS++nhQZNhVPaIlBZv98fGTaWDvGo6ZN+d5ZB4Ex+SMOzbKE6 igXb74xjunDqQhSJCvi0y8wfFOBIiIx/HQ7lyO2tvoz99JvXLJlub5z28QKH6c/lYw7x xqAD/+HveHcQPC2vro7tVQSKkLDjsdtEZYIq5OQNUgNxSaxcozbNpB2xrJESysJHFShJ n51w== 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 c24si51870lff.2.2020.05.07.23.40.43 for (version=TLS1_2 cipher=ECDHE-ECDSA-AES128-GCM-SHA256 bits=128/128); Thu, 07 May 2020 23:40:43 -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 49JLLc60K3z43qW; Fri, 8 May 2020 08:40:40 +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 0486fJiD022856; Fri, 8 May 2020 08:41:19 +0200 Received: by fb04209.mathematik.tu-darmstadt.de (Postfix, from userid 11003) id 7AF2BC0061; Fri, 8 May 2020 08:40:39 +0200 (CEST) Date: Fri, 8 May 2020 08:40:39 +0200 From: Thomas Streicher To: David Roberts Cc: =?iso-8859-1?Q?Joyal=2C_Andr=E9?= , Thorsten Altenkirch , Michael Shulman , Steve Awodey , "homotopyt...@googlegroups.com" Subject: Re: [HoTT] Identity versus equality Message-ID: <20200508064039.GC21473@mathematik.tu-darmstadt.de> References: <05375057-883F-4487-8919-2579F5771AFC@cmu.edu> <952EF822-FD92-404C-A279-89502238BCDC@nottingham.ac.uk> <8C57894C7413F04A98DDF5629FEC90B1652F526C@Pli.gst.uqam.ca> <67E9DCCA-F9CA-45B7-9AC8-E5A7E94FE9A9@nottingham.ac.uk> <20200507100930.GA9390@mathematik.tu-darmstadt.de> <8C57894C7413F04A98DDF5629FEC90B1652F5334@Pli.gst.uqam.ca> <8C57894C7413F04A98DDF5629FEC90B1652F53A3@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 Robert, in what I said I didn't mean set theory literally. I was rather referring to all kinds of categorical logic where equality is interpreted as (fiberwise) diagonal like (traditional) topos theory in particular. These kinds of gadgets all have the advantage that "Set" is not ruled out as a model. Since the diagonal is hardly ever fibrant HoTT rules out Set as a model. But this is not my main problem. My main problem is that there is at least one area of category theory where one has to speak about equality of objects and these are Grothendieck fibrations. And these are intrinsic for doing topos theory over general base toposes. (That I really like them is, admittedly, also an important reason for me not being ready to give them up! And for reasons of personal and cultural "antagonisms" they are not very popular among the majority of category theorists... Thus, there are many people who would not be too sad about working in a framework not allowing to speak about them.) But I want to emphasize that real masters of infinite dimensional categories do not have the faintest problem speaking about equality when speaking about infinite dimensional versions of Grothendieck fibrations!) Though (traditional) topos theory can be developed over fairly general toposes and this, at least philosophically, is an important aspect one cannot deny that most toposes of interest heavily rely on Set, be they of the Grothendieck kind or be they of the realizability kind! Thomas PS Above I put Set into inverted commas because the logician in me finds it amusing to speak about "the" category of sets which is nothing but an illusion... Even the nowadays not so little number of adherents of the "multiverse" view of set theory would share this view! But even the "universe" view is nothing but an ideology because since Cohen set theory is mainly a business of constructing different models via forcing. Thus, since Set is (sort of) an illusion it is important to do toposes over arbitrary bases for which purpose one needs Grothendieck fibrations which do not make sense without equality of objects. PPS Some people might get the impression I am a "crypto set theorist". Nothing could be more wrong. I am anti-ideological and pluralist and I like "deviating" ideas. But I am interested in calibrating what one needs for which goals. What I am allergic at is ideological positions which want to forbid someone doing certain things because they do not fit to some ideological positions... And one has to accept that not all combinations are possible. Thus pluralist is better to inegrist!