From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 2002:a63:e602:: with SMTP id g2mr3697392pgh.380.1588972011710; Fri, 08 May 2020 14:06:51 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a63:d049:: with SMTP id s9ls1688098pgi.5.gmail; Fri, 08 May 2020 14:06:50 -0700 (PDT) X-Received: by 2002:a63:b214:: with SMTP id x20mr3788019pge.289.1588972010197; Fri, 08 May 2020 14:06:50 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1588972010; cv=none; d=google.com; s=arc-20160816; b=tMdQc8jIy1XJc0mLWv+Yn3w1kVpcnB33AkrMwV8FtZM1YIS9Qcuuh3BFtPPYFTKA3I FqgB9NXSmIsVG3eAmoWAs4s0rG3bWZ5W6b3XoK4QlPpAakMewJrFaYOt0Z8lLFOCMKGW e4hrBTVoivU6BK2mzIK6cSF/EWUhNd+4uGL34M3Pb13nDFW2ByW6xnkz6brAcRViNZOp BfP/1t1S3idCYwEjsgPsO9jM7cqWQt8yC2XarvySHTi79uQvGFGtTYIwKT+rRsw8aBTk NL14zcIjgTYJmNFNRUELbsYftBlklOvyzUIJ54AQNn1C5/zVEKQFjNilp8Kmk66BD7w3 qI0g== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=mime-version:content-transfer-encoding:content-language :accept-language:in-reply-to:references:message-id:date:thread-index :thread-topic:subject:cc:to:from:ironport-sdr; bh=HYWcK9BVzJjdTp9Ml2SSchzTy7gJ1D1J6cV/HXEuiAc=; b=ifJ7XSim0wOVMQSghopAVKEDqCoMJWhjny6NkLoGQbsSQ5M3KBfdhM1tpvEtl30j4v CdEItpYDOvUIOPsrtPRXmZkQ9u48clKpKtfCDLKDSYAWUIvCNa/SLd07YqPSEBLKgiyr clNiBRDzyxAe46s5Pk9cmF735mUAk+cX69rx4ZIcTn6Q8FltBwVGF899QvJMr/qkZoHI gIt9RKKnv3qQX4aVr/Gjb95fKePAR9YfliAzu1LTE/h9FW6YUsbRE4sG5rQrcyCqDlX0 KEw/ZnxCPWpk9CaDrqlOxm2zGyNzhPKFDJJ/HJZMq9SdH1RbkND+Tl/TpF9NtEtq2ZH/ LWsg== ARC-Authentication-Results: i=1; gmr-mx.google.com; spf=pass (google.com: domain of joyal...@uqam.ca designates 132.208.246.231 as permitted sender) smtp.mailfrom=joyal...@uqam.ca Return-Path: Received: from mail6.uqam.ca (mail.uqam.ca. [132.208.246.231]) by gmr-mx.google.com with ESMTP id k13si212961pfd.0.2020.05.08.14.06.49 for ; Fri, 08 May 2020 14:06:50 -0700 (PDT) Received-SPF: pass (google.com: domain of joyal...@uqam.ca designates 132.208.246.231 as permitted sender) client-ip=132.208.246.231; Authentication-Results: gmr-mx.google.com; spf=pass (google.com: domain of joyal...@uqam.ca designates 132.208.246.231 as permitted sender) smtp.mailfrom=joyal...@uqam.ca IronPort-SDR: yqgSbrwcE6Gicjw/7lsNWOxyLO7cA12wyrHL3tyrlXeAJOrVyMruZ6bCviy51w7sStTH4czwzV 5XdOoLiNuIwSrmHRAR98JmF+wBnsOsaBA/ENk+3LDtCA5y4blQDwOnONAjDHnbiFokcMeFQzeX IsiQqYbu/LgQAk2zyEuUdv4zL6d9JzvcnUkol/EbrFZeB+3mrl8IsYIkTISp4jqkviTolGRRa/ NllChLtuVffz6Jp+Y5LdG24W5BdFsHVSNyZvRpiHwTcx0izC3QpyfxXa4SHEuxrV3wYSlZULSj T8k= X-IronPort-AV: E=Sophos;i="5.73,369,1583211600"; d="scan'208";a="10519389" Received: from unknown (HELO Message.gst.uqam.ca) ([132.208.216.70]) by mail6.uqam.ca with ESMTP; 08 May 2020 17:06:49 -0400 Received: from PLI.gst.uqam.ca ([169.254.3.153]) by Message.gst.uqam.ca ([169.254.1.218]) with mapi id 14.03.0439.000; Fri, 8 May 2020 17:06:48 -0400 From: =?iso-8859-1?Q?Joyal=2C_Andr=E9?= To: Thomas Streicher , David Roberts CC: Thorsten Altenkirch , "Michael Shulman" , Steve Awodey , "homotopyt...@googlegroups.com" Subject: RE: [HoTT] Identity versus equality Thread-Topic: [HoTT] Identity versus equality Thread-Index: AQHWIrnt2rpL+UtjL0e4oihqoDCB+qibJxGOgACIG4CAAAS1AIAAPFAA//+/ZaSAAMfxgIAANUUAgAAO4LWAALJlgP//xKOFgABhQICAAHDSgIAAmhfJ Date: Fri, 8 May 2020 21:06:47 +0000 Message-ID: <8C57894C7413F04A98DDF5629FEC90B1652F54CC@Pli.gst.uqam.ca> 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> ,<20200508064039.GC21473@mathematik.tu-darmstadt.de> In-Reply-To: <20200508064039.GC21473@mathematik.tu-darmstadt.de> Accept-Language: en-US, en-CA Content-Language: en-US X-MS-Has-Attach: X-MS-TNEF-Correlator: x-originating-ip: [132.208.216.80] Content-Type: text/plain; charset="iso-8859-1" Content-Transfer-Encoding: quoted-printable MIME-Version: 1.0 Dear Thomas, You are right, the equality of objects in a Grothendieck fibration is judge= mental. Propositional equality of type theory has been studied a lot during the las= t decades. I feel quite confortable with it, with the homotopy interpretation and the = univalence principle, etc. I confess that I am much less at ease with judgmental equality and the synt= ax of type theory. Until now, type theory has failed to prove that pi_4(S^3)=3DC_2. Is it the symptom of a fundamental problem? Is it because the reduction algoritms are not optimal? Or because computers are not powerful enough? What is the abstract theory of terms reduction in type theory? I apologise for my ignorance. Best, Andr=E9 ________________________________________t From: Thomas Streicher [stre...@mathematik.tu-darmstadt.de] Sent: Friday, May 08, 2020 2:40 AM To: David Roberts Cc: Joyal, Andr=E9; Thorsten Altenkirch; Michael Shulman; Steve Awodey; hom= otopyt...@googlegroups.com Subject: Re: [HoTT] Identity versus equality 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!