From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 2002:a67:bd07:: with SMTP id y7mr13665414vsq.109.1588867999432; Thu, 07 May 2020 09:13:19 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:ab0:45b3:: with SMTP id u48ls378682uau.1.gmail; Thu, 07 May 2020 09:13:18 -0700 (PDT) X-Received: by 2002:a9f:372e:: with SMTP id z43mr12255670uad.54.1588867997853; Thu, 07 May 2020 09:13:17 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1588867997; cv=none; d=google.com; s=arc-20160816; b=xxK+ySqtqpKSIVswWNknsgRUGN4XD8KKzZT1Bhaiw21UZB6U0A2seXicmxf4KTon2J bNPlNRm3jxLfgRUb5gJaJxQWwmjxgm2oPKExWQx+50kafXi7pWGQRAbfAO3Mg9fj8GKz pu4UZ/YJ6+2UeaY6PWxjd9qiB8WxKONDFuNbAsSAVcLa9U2hJrzjQxmPLcD5f9NKgeUb 5o7ArkcPKWovNe4ClgIBnqgeIFvpm2hI62nuN5bpZgluJJ/n9MBCWhchFHvb9AAqGw3L b3SMdWtt2PjlWmNfuITUAsyfs80GHEDiyrf2aTLHmVnezAMp0z33RFxqnCMTmMv87fYz Oxnw== 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=dBcSc2FJAtDYyo9VaKYjp0ttgAdPEKVT2uDFyVtXKn8=; b=u9wVAfqAr37lHHcoQ8PHCB0//AWpMFEEYIGYPrFlgtQNchZii7oBv54fagfVp2uWG0 DQcVx/NXOkBQvPnVAFEGI93pPoG0kVyim/3mGPyIwmxgsMFZyS8Tg/ZMB+WpAIicGH0F xDY6hTMuQjwjKOLt5d4TTXwZPr43JJm6TXrwhvghL3QLMtNWMIDdjCCWurzNKumBitgC c8S6qIIpn3MKrViVOtYp5mlFRrtjB0cB80lr0mPcmfKKpNjTFOno4ymYXbDAH65mQabZ qt8VfX4px/F0oF8S5lQYi8bLsexNfaDW0DPLspqLvk+FXIiT5mlggVeHp7OhLWMCbQV6 QYxA== 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 (mail6.uqam.ca. [132.208.246.231]) by gmr-mx.google.com with ESMTP id v22si484807vsl.1.2020.05.07.09.13.17 for ; Thu, 07 May 2020 09:13:17 -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: WS1tSyj/JLJpyRPHHMQI0JOnKjSwD0oiz5OTN4IqymPMJ3DcdgnBD3d6WBUTvjsQSxdnVj/9cX eIutZDKoebWAcu3s4ehvLwHSIPzENW+5sWQTSfXbo811D/rQtBtGj5Qw31RlEvI5eDIkYcE+9u YlsFZcAcqpJefdI3fk2tqx0I4mpJxarzFUGOIxjjFsFBhzAnQV1eZ6LHiYK850/sYB029IVhW0 o2ZyFu8SGbW9sd0TyOvN+6e2M5uD6NLu9N/b+t0sP0aH6yoy1Y5akD3qS3CRnM2YXEpGLbRLXe oBw= X-IronPort-AV: E=Sophos;i="5.73,364,1583211600"; d="scan'208";a="10396014" Received: from unknown (HELO Avis.gst.uqam.ca) ([132.208.216.75]) by mail6.uqam.ca with ESMTP; 07 May 2020 12:13:18 -0400 Received: from PLI.gst.uqam.ca ([169.254.3.153]) by Avis.gst.uqam.ca ([169.254.2.247]) with mapi id 14.03.0439.000; Thu, 7 May 2020 12:13:17 -0400 From: =?iso-8859-1?Q?Joyal=2C_Andr=E9?= To: Thomas Streicher , "Thorsten Altenkirch" CC: Michael Shulman , Steve Awodey , "homotopyt...@googlegroups.com" Subject: RE: [HoTT] Identity versus equality Thread-Topic: [HoTT] Identity versus equality Thread-Index: AQHWIrnt2rpL+UtjL0e4oihqoDCB+qibJxGOgACIG4CAAAS1AIAAPFAA//+/ZaSAAMfxgIAANUUAgAAO4LU= Date: Thu, 7 May 2020 16:13:16 +0000 Message-ID: <8C57894C7413F04A98DDF5629FEC90B1652F5334@Pli.gst.uqam.ca> References: <8C57894C7413F04A98DDF5629FEC90B1652F515E@Pli.gst.uqam.ca> <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> In-Reply-To: <20200507100930.GA9390@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.81] Content-Type: text/plain; charset="iso-8859-1" Content-Transfer-Encoding: quoted-printable MIME-Version: 1.0 Thank you all for your comments. Thomas wrote: <> I agree, there is some some kind of (weak) Quillen model structure associat= ed to every model of type theory. All of higher category theory seems to be based on good old set theory. For example, a quasi-category is a simplicial set. The category of sets could be replaced by a topos, but a topos is a categor= y=20 and every category has a set of objects and a set of arrows. At some level, all mathematics is based on some kind of set theory. Is it not obvious? We cannot escape Kantor's paradise! Of course, we could possibly work exclusively with countable sets. The set of natural numbers is the socle on which all mathematics is constru= cted. Still, I would not want to refer constantly to recursion when I do mathemat= ics. There is a hierarchy of mathematical languages, and Peano's arithmetic is a= t the ground level. Modern mathematics is mostly concerned with higher levels of abstraction. Its usefulness is without questions, athough its foundation can be problema= tic. Type theory is the only theory I know which includes two levels in its form= alism.=20 Judgemental equality is at the lower level. It is not inferior, it is more = fundamental. Best, Andr=E9 ________________________________________ From: Thomas Streicher [stre...@mathematik.tu-darmstadt.de] Sent: Thursday, May 07, 2020 6:09 AM To: Thorsten Altenkirch Cc: Joyal, Andr=E9; Michael Shulman; Steve Awodey; homotopyt...@googlegroup= s.com Subject: Re: [HoTT] Identity versus equality In my eyes the reason for the confusion (or rather different views) arises from the different situation we have in syntax and in semantics. In syntax the "real thing" is propositional equality and judgemental equality is just an auxiliary notion. In mathematics it's the well known difference between equality requiring proof (e.g. by induction) and checking equality by mere symbolic computation. The latter is just a technical device and not something conceptually basic. The situation is very different in models (be they simplicial, cubical or whatever). There judgemental equality gets interpreted as equality of morphism and propositional equality gets interpreted as being homotopic. Since the outer level of 2-level type theory is extensional there is no judgemental equality (as in extensional TT). This latter view is the view of people working in higher dimensional category theory as e.g. you, Andr'e when you are not posting on the list but write your beautiful texts on quasicats, Lurie or Cisinski (and quite a few others). In these works people are not afraid of refering to equality of objects, e.g. when defining the infinite dimensional analogue of Grothendieck fibrations. And this for very good reasons since there are important parts of category theory where equality of objects does play a role (typically Grothendieck fibrations). Fibered cats also often don't allow one to speak about equality of objects in the base but it is there. This is very clearly expressed so in the last paragraph of B'enabou's JSL article of fibered cats from 1985. I think this applies equally well to infinity cats mutatis mutandis. This phenomenon is not new. Consider good old topos theory. There are things expressible in the internal logic of a topos and there are things which can't be expressed in it as e.g. well pointedness or every epi splits. The first holds vacuously when (misleadingly) expressed in the internal language of a topos and the second amounts to so called internal AC (which amounts to epis being preserved by arbitrary exponentiation). This doesn't mean at all that internal language = is a bad thing. It just means that that it has its limitations... Analogously, so in infinity category theory. Let us assume for a moment that HoTT were the internal language of infinity toposes (which I consider as problematic). There are many things which can be expressed in the internal language but not everything as e.g. being a Grothendieck fibration or being a mono... I mean these are facts which one has to accept. One might find them deplorable or a good thing but one has to accept them... One of the reasons why I do respect Voevodsky a lot is that although he developed HoTT (or better the "univalent view") he also suggested 2-level type theory when he saw its limitations. I hope you apologize but I can't supress the following analogy coming to my mind. After revolution in Russia and the civil war when economy lay down the Bolsheviks reintroduced a bit of market economy under the name NEP (at least that's the acronym in German) to help up the economy. (To finish the story NEP was abandoned by Stalin which lead to well known catastrophies like the forced collectivization...) Sorry for that but one has to be careful when changing things and think twice before throwing away old things...some of them might be still useful and even indispensible! Thomas